use std::collections::BTreeSet;
use super::super::expr::aver_name_to_lean;
use super::super::shared::to_lower_first;
use super::super::tactic_ir::{InductionArm, Tactic};
use super::AutoProof;
use super::shared::law_simp_defs;
use crate::ast::{TypeDef, TypeVariant, VerifyBlock, VerifyLaw};
use crate::codegen::CodegenContext;
mod floor_bound;
mod keystone;
mod multicite;
pub(in crate::codegen::lean) use keystone::{
emit_pool_composition_generic_law, recognize_pool_composition_generic,
};
pub(in crate::codegen::lean) use multicite::{
emit_multicite_composition_law, recognize_multicite_composition,
};
fn simp_done_omega_first(simp: &str) -> Tactic {
Tactic::First(vec![
Tactic::Leaf(format!("{simp}; done")),
Tactic::Leaf(format!("{simp}; omega")),
Tactic::Sorry,
])
}
pub(super) fn lean_nat_lift_support(
law: &VerifyLaw,
ctx: &CodegenContext,
law_uid: &str,
extra_fns: &BTreeSet<String>,
) -> (Vec<String>, Vec<String>, BTreeSet<String>) {
use crate::codegen::proof_recognize::NatArithKind;
let mut support = Vec::new();
let mut simp_extra = Vec::new();
let mut bridged_fns: BTreeSet<String> = BTreeSet::new();
let mut arith = crate::codegen::proof_recognize::collect_nat_arith_ops_in_law(law, ctx);
for op in crate::codegen::proof_recognize::collect_nat_arith_ops_for_names(extra_fns, ctx) {
if !arith.iter().any(|o| o.fn_name == op.fn_name) {
arith.push(op);
}
}
let add_bridge_name = arith
.iter()
.find(|op| op.kind == NatArithKind::Add)
.map(|op| format!("{law_uid}_{}_isNatAdd", aver_name_to_lean(&op.fn_name)));
let mut has_mul = false;
let ordered = arith
.iter()
.filter(|o| o.kind != NatArithKind::Mul)
.chain(arith.iter().filter(|o| o.kind == NatArithKind::Mul));
for op in ordered {
let f = aver_name_to_lean(&op.fn_name);
bridged_fns.insert(f.clone());
match op.kind {
NatArithKind::Add => {
let name = format!("{law_uid}_{f}_isNatAdd");
let body = Tactic::Seq(vec![
Tactic::Leaf("intro a b".to_string()),
Tactic::Induction {
target: "a".to_string(),
arms: vec![
InductionArm {
pattern: "zero".to_string(),
body: simp_done_omega_first(&format!("simp [{f}]")),
},
InductionArm {
pattern: "succ k ih".to_string(),
body: simp_done_omega_first(&format!("simp [{f}, ih]")),
},
],
},
]);
support.push(super::support_theorem(
&format!("theorem {name} : ∀ a b, {f} a b = a + b := by"),
body,
));
simp_extra.push(name);
}
NatArithKind::Sub => {
let name = format!("{law_uid}_{f}_isNatSub");
support.push(format!(
"theorem {name} : ∀ a b, {f} a b = a - b := by\n intro a b\n induction a generalizing b with\n | zero => first | (simp [{f}]; done) | (simp [{f}]; omega) | sorry\n | succ k ih => cases b with\n | zero => first | (simp [{f}]; done) | (simp [{f}]; omega) | sorry\n | succ j => first | (simp [{f}, ih]; done) | (simp [{f}, ih]; omega) | sorry"
));
simp_extra.push(name);
}
NatArithKind::Mul => {
let Some(add_name) = &add_bridge_name else {
continue;
};
let name = format!("{law_uid}_{f}_isNatMul");
let body = Tactic::Seq(vec![
Tactic::Leaf("intro a b".to_string()),
Tactic::Induction {
target: "a".to_string(),
arms: vec![
InductionArm {
pattern: "zero".to_string(),
body: simp_done_omega_first(&format!("simp [{f}]")),
},
InductionArm {
pattern: "succ k ih".to_string(),
body: Tactic::First(vec![
Tactic::Leaf(format!(
"simp only [{f}, {add_name}, ih, Nat.succ_mul, Nat.add_comm]"
)),
Tactic::Sorry,
]),
},
],
},
]);
support.push(super::support_theorem(
&format!("theorem {name} : ∀ a b, {f} a b = a * b := by"),
body,
));
simp_extra.push(name);
has_mul = true;
}
}
}
let mut compare = crate::codegen::proof_recognize::collect_nat_compare_ops_in_law(law, ctx);
for op in crate::codegen::proof_recognize::collect_nat_compare_ops_for_names(extra_fns, ctx) {
if !compare.iter().any(|o| o.fn_name == op.fn_name) {
compare.push(op);
}
}
for op in compare {
let f = aver_name_to_lean(&op.fn_name);
bridged_fns.insert(f.clone());
let name = format!("{law_uid}_{f}_{}", op.kind.bridge_suffix());
let prop = op.kind.prop_op();
let (driver, passenger) = if op.kind.induct_on_second() {
("b", "a")
} else {
("a", "b")
};
support.push(format!(
"theorem {name} : ∀ a b, ({f} a b = true) = (a {prop} b) := by\n intro a b\n induction {driver} generalizing {passenger} with\n | zero => cases {passenger} <;> first | (simp [{f}]) | sorry\n | succ k ih => cases {passenger} <;> first | (simp [{f}, ih]) | sorry"
));
simp_extra.push(name);
}
if has_mul {
for lemma in [
"Nat.mul_add",
"Nat.add_mul",
"Nat.mul_assoc",
"Nat.succ_mul",
"Nat.mul_succ",
"Nat.mul_one",
"Nat.one_mul",
"Nat.mul_zero",
"Nat.zero_mul",
] {
simp_extra.push(lemma.to_string());
}
}
(support, simp_extra, bridged_fns)
}
fn recognize_refl_eq_fn(fd: &crate::ast::FnDef, ctx: &CodegenContext) -> bool {
use crate::ast::{Expr, Literal, Pattern};
if fd.return_type.trim() != "Bool" || fd.params.len() != 2 {
return false;
}
let (p0, t0) = (&fd.params[0].0, fd.params[0].1.trim());
let (p1, t1) = (&fd.params[1].0, fd.params[1].1.trim());
if t0 != t1 || find_sum_type(ctx, t0).is_none() {
return false;
}
let Some(body) = fd.body.tail_expr() else {
return false;
};
let Expr::Match { subject, arms } = &body.node else {
return false;
};
if !matches!(&subject.node, Expr::Ident(n) | Expr::Resolved { name: n, .. } if n == p0) {
return false;
}
let ctor_of = |p: &Pattern| -> Option<String> {
match p {
Pattern::Constructor(name, _) => Some(name.clone()),
_ => None,
}
};
let is_recursive_self = |e: &Expr| -> bool {
match e {
Expr::FnCall(callee, args) => {
super::shared::expr_dotted_name(callee).as_deref() == Some(fd.name.as_str())
&& args.len() == 2
}
Expr::TailCall(tc) => tc.target == fd.name && tc.args.len() == 2,
_ => false,
}
};
arms.iter().all(|outer| {
let Some(octor) = ctor_of(&outer.pattern) else {
return false;
};
let Expr::Match {
subject: inner_subj,
arms: inner_arms,
} = &outer.body.node
else {
return false;
};
if !matches!(&inner_subj.node, Expr::Ident(n) | Expr::Resolved { name: n, .. } if n == p1) {
return false;
}
inner_arms.iter().all(|inner| {
let diagonal = ctor_of(&inner.pattern).as_deref() == Some(octor.as_str());
match &inner.body.node {
Expr::Literal(Literal::Bool(b)) => !diagonal || *b,
e if is_recursive_self(e) => true,
_ => !diagonal,
}
})
})
}
fn lean_refl_support(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
law_uid: &str,
) -> (Vec<String>, Vec<String>) {
let mut support = Vec::new();
let mut names = Vec::new();
for src_name in super::shared::law_simp_source_names(ctx, vb, law) {
let Some(fd) = ctx.fn_def_by_name(&src_name, ctx.active_module_scope().as_deref()) else {
continue;
};
if !recognize_refl_eq_fn(fd, ctx) {
continue;
}
let f = aver_name_to_lean(&src_name);
let name = format!("{law_uid}_{f}_refl");
let body = super::intro_then_first(
&["a".to_string()],
vec![
format!("induction a <;> simp_all [{f}]; done"),
format!("induction a <;> simp_all [{f}]"),
],
);
support.push(super::support_theorem(
&format!("theorem {name} : ∀ a, {f} a a = true := by"),
body,
));
names.push(name);
}
(support, names)
}
fn discovered_lemma_source_fns(ctx: &CodegenContext, names: &[String]) -> BTreeSet<String> {
use std::collections::BTreeMap;
if names.is_empty() {
return BTreeSet::new();
}
let lean_index: BTreeMap<String, String> = ctx
.modules
.iter()
.flat_map(|m| m.fn_defs.iter())
.chain(ctx.fn_defs.iter())
.filter(|fd| crate::codegen::common::is_pure_fn(fd))
.map(|fd| (aver_name_to_lean(&fd.name), fd.name.clone()))
.collect();
ctx.discovered_lemmas
.iter()
.filter(|l| names.contains(&l.name))
.flat_map(|l| crate::codegen::lemma_discovery::mentioned_fns(&l.text, &lean_index))
.collect()
}
fn discovered_simp_entries(ctx: &CodegenContext, names: &[String]) -> Vec<String> {
if names.is_empty() {
return Vec::new();
}
let program_fns: BTreeSet<String> = ctx
.modules
.iter()
.flat_map(|m| m.fn_defs.iter())
.chain(ctx.fn_defs.iter())
.filter(|fd| crate::codegen::common::is_pure_fn(fd))
.map(|fd| aver_name_to_lean(&fd.name))
.collect();
let pinned: Vec<&crate::codegen::lemma_discovery::CommittedLemma> = ctx
.discovered_lemmas
.iter()
.filter(|l| names.contains(&l.name))
.collect();
crate::codegen::lemma_discovery::simp_entries(&pinned, &program_fns)
}
fn discovered_support_lines(
ctx: &CodegenContext,
vb: &VerifyBlock,
law: &VerifyLaw,
names: &[String],
) -> Vec<String> {
if names.is_empty() {
return Vec::new();
}
let Some(fn_id) = ctx
.symbol_table
.fn_id_of(&crate::ir::FnKey::entry(&vb.fn_name))
else {
return Vec::new();
};
let mut out = Vec::new();
for name in names {
let first_user = ctx.proof_ir.law_theorems.iter().find(|t| {
matches!(&t.strategy,
crate::ir::ProofStrategy::SimpOverLemmas(ns) if ns.contains(name))
});
let this_law_is_first =
first_user.is_some_and(|t| t.fn_id == fn_id && t.law_name == law.name);
if this_law_is_first
&& let Some(lemma) = ctx.discovered_lemmas.iter().find(|l| &l.name == name)
{
out.push(lemma.text.clone());
}
}
out
}
fn program_fn_lean_names(ctx: &CodegenContext) -> BTreeSet<String> {
ctx.modules
.iter()
.flat_map(|m| m.fn_defs.iter())
.chain(ctx.fn_defs.iter())
.filter(|fd| crate::codegen::common::is_pure_fn(fd))
.map(|fd| aver_name_to_lean(&fd.name))
.collect()
}
fn qualified_cone_name(fd: &crate::ast::FnDef, ctx: &CodegenContext) -> String {
let bare = aver_name_to_lean(&fd.name);
match ctx
.modules
.iter()
.find(|m| m.fn_defs.iter().any(|d| std::ptr::eq(d, fd)))
{
Some(m) => format!("{}.{}", m.prefix, bare),
None => bare,
}
}
#[allow(clippy::too_many_arguments)]
fn dep_law_admissible(
dep_module: &crate::codegen::ModuleInfo,
dep_prev: &VerifyBlock,
dep_prev_law: &VerifyLaw,
qualified_scope: &BTreeSet<String>,
subject: &str,
dep_index: &std::collections::BTreeMap<String, String>,
ctx: &CodegenContext,
) -> Option<(String, String)> {
let (bare_name, stmt) = ctx.with_module_scope(Some(dep_module.prefix.as_str()), || {
crate::codegen::lean::toplevel::law_as_lemma_statement(dep_prev, dep_prev_law, ctx)
})?;
let name = format!("{}.{}", dep_module.prefix, bare_name);
let text = format!("theorem {name} : {stmt} := by");
let mentions = crate::codegen::lemma_discovery::mentioned_fns(&text, dep_index);
if mentions.is_empty() {
return None;
}
let prev_subject_qualified = format!(
"{}.{}",
dep_module.prefix,
aver_name_to_lean(&dep_prev.fn_name)
);
if mentions.is_subset(qualified_scope)
|| (mentions.contains(subject) && qualified_scope.contains(&prev_subject_qualified))
{
Some((name, text))
} else {
None
}
}
fn cited_closure_dep_laws(
ctx: &CodegenContext,
admitted: &mut std::collections::HashSet<(String, String)>,
) {
use crate::ast::{TopLevel, VerifyKind};
const ENTRY_RANK: usize = usize::MAX;
let order = dep_theorem_emit_order(ctx);
if order.is_empty() {
return;
}
fn cited(vb: &VerifyBlock, law: &VerifyLaw, ctx: &CodegenContext) -> Vec<(String, String)> {
let mut out = Vec::new();
out.extend(super::triangle_sum_cited_deps(vb, law, ctx));
out.extend(super::frac_order_chain_cited_deps(vb, law, ctx));
out.extend(super::frac_monotone_compose_cited_deps(vb, law, ctx));
out.extend(super::monotone_reflect_cited_deps(vb, law, ctx));
out.extend(keystone::keystone_dep_bridge_cites(vb, law, ctx));
out
}
let mut admit =
|scope: Option<&str>, vb: &VerifyBlock, law: &VerifyLaw, consumer_key: (usize, usize)| {
for dep in ctx.with_module_scope(scope, || cited(vb, law, ctx)) {
if topology_admits(order.get(&dep), consumer_key) {
admitted.insert(dep);
}
}
};
for item in &ctx.items {
let TopLevel::Verify(vb) = item else { continue };
let VerifyKind::Law(law) = &vb.kind else {
continue;
};
admit(None, vb, law, (ENTRY_RANK, vb.line));
}
for (mi, module) in ctx.modules.iter().enumerate() {
for vb in &module.verify_laws {
let VerifyKind::Law(law) = &vb.kind else {
continue;
};
admit(Some(module.prefix.as_str()), vb, law, (mi, vb.line));
}
}
}
fn topology_admits(dep_order: Option<&(usize, usize)>, consumer_order: (usize, usize)) -> bool {
dep_order.is_none_or(|dep| *dep < consumer_order)
}
fn dep_theorem_emit_order(
ctx: &CodegenContext,
) -> std::collections::HashMap<(String, String), (usize, usize)> {
use crate::ast::VerifyKind;
use crate::codegen::lean::toplevel::{law_as_lemma_statement, law_theorem_base};
let mut order: std::collections::HashMap<(String, String), (usize, usize)> =
std::collections::HashMap::new();
for (mi, module) in ctx.modules.iter().enumerate() {
ctx.with_module_scope(Some(module.prefix.as_str()), || {
for vb in &module.verify_laws {
let VerifyKind::Law(law) = &vb.kind else {
continue;
};
let key = (mi, vb.line);
let canonical = law_theorem_base(vb, law, ctx);
order
.entry((module.prefix.clone(), canonical))
.or_insert(key);
if let Some((rewrite, _)) = law_as_lemma_statement(vb, law, ctx) {
order.entry((module.prefix.clone(), rewrite)).or_insert(key);
}
}
});
}
order
}
#[cfg(debug_assertions)]
pub(crate) fn dep_theorem_order_keys(
ctx: &CodegenContext,
) -> std::collections::HashSet<(String, String)> {
dep_theorem_emit_order(ctx).into_keys().collect()
}
pub(crate) fn admitted_dep_law_theorems(
ctx: &CodegenContext,
) -> std::collections::HashSet<(String, String)> {
use crate::ast::{TopLevel, VerifyKind};
let mut admitted: std::collections::HashSet<(String, String)> =
std::collections::HashSet::new();
if ctx.modules.is_empty() {
return admitted;
}
let consider = |consumer_scope: Option<&str>,
consumer_vb: &VerifyBlock,
consumer_law: &VerifyLaw,
admitted: &mut std::collections::HashSet<(String, String)>| {
ctx.with_module_scope(consumer_scope, || {
let (qualified_scope, subject) =
consumer_law_qualified_scope(consumer_vb, consumer_law, ctx);
let consumer_idx =
consumer_scope.and_then(|s| ctx.modules.iter().position(|m| m.prefix == s));
for (module_idx, module) in ctx.modules.iter().enumerate() {
if let Some(c) = consumer_idx
&& module_idx >= c
{
continue;
}
let dep_index = dep_membership_index(module, ctx);
for dep_prev in &module.verify_laws {
let VerifyKind::Law(dep_prev_law) = &dep_prev.kind else {
continue;
};
if let Some((name, _text)) = dep_law_admissible(
module,
dep_prev,
dep_prev_law,
&qualified_scope,
&subject,
&dep_index,
ctx,
) {
if let Some(base) = name.strip_prefix(&format!("{}.", module.prefix)) {
admitted.insert((module.prefix.clone(), base.to_string()));
}
}
}
}
});
};
for item in &ctx.items {
let TopLevel::Verify(vb) = item else { continue };
let VerifyKind::Law(law) = &vb.kind else {
continue;
};
consider(None, vb, law, &mut admitted);
}
for module in &ctx.modules {
for vb in &module.verify_laws {
let VerifyKind::Law(law) = &vb.kind else {
continue;
};
consider(Some(module.prefix.as_str()), vb, law, &mut admitted);
}
}
cited_closure_dep_laws(ctx, &mut admitted);
admitted
}
fn dep_membership_index(
module: &crate::codegen::ModuleInfo,
ctx: &CodegenContext,
) -> std::collections::BTreeMap<String, String> {
let mut idx: std::collections::BTreeMap<String, String> = program_fn_lean_names(ctx)
.into_iter()
.map(|l| (l.clone(), l))
.collect();
for fd in &module.fn_defs {
if crate::codegen::common::is_pure_fn(fd) {
let qualified = format!("{}.{}", module.prefix, aver_name_to_lean(&fd.name));
idx.insert(qualified.clone(), qualified);
}
}
idx
}
fn consumer_law_qualified_scope(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> (BTreeSet<String>, String) {
let inputs = crate::codegen::proof_lower::ProofLowerInputs::from_ctx(ctx);
let cone = crate::codegen::proof_lower::LawProofCone::compute(law, &vb.fn_name, &inputs);
let mut scope: BTreeSet<String> = cone
.pure_fns()
.iter()
.map(|fd| qualified_cone_name(fd, ctx))
.collect();
let subject = aver_name_to_lean(&vb.fn_name);
scope.insert(subject.clone());
(scope, subject)
}
fn earlier_law_lemmas(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> Vec<crate::codegen::lemma_discovery::CommittedLemma> {
use crate::ast::{TopLevel, VerifyKind};
let inputs = crate::codegen::proof_lower::ProofLowerInputs::from_ctx(ctx);
let cone = crate::codegen::proof_lower::LawProofCone::compute(law, &vb.fn_name, &inputs);
let mut scope: BTreeSet<String> = cone
.pure_fns()
.iter()
.map(|fd| aver_name_to_lean(&fd.name))
.collect();
let subject = aver_name_to_lean(&vb.fn_name);
scope.insert(subject.clone());
let program_index: std::collections::BTreeMap<String, String> = program_fn_lean_names(ctx)
.into_iter()
.map(|l| (l.clone(), l))
.collect();
let mut out = Vec::new();
for item in &ctx.items {
let TopLevel::Verify(prev) = item else {
continue;
};
if prev.line == vb.line && prev.fn_name == vb.fn_name {
break;
}
let VerifyKind::Law(prev_law) = &prev.kind else {
continue;
};
let Some((name, stmt)) =
crate::codegen::lean::toplevel::law_as_lemma_statement(prev, prev_law, ctx)
else {
continue;
};
let text = format!("theorem {name} : {stmt} := by");
let mentions = crate::codegen::lemma_discovery::mentioned_fns(&text, &program_index);
if mentions.is_empty() {
continue;
}
let prev_subject = aver_name_to_lean(&prev.fn_name);
let lhs_mentions = crate::codegen::lemma_discovery::lemma_lhs_fns(&text, &program_index);
let lhs_rooted = !lhs_mentions.is_empty()
&& lhs_mentions.is_subset(&scope)
&& scope.contains(&prev_subject);
let premise_rooted = prev_law.when.as_ref().is_some_and(|w| {
let mut raw: BTreeSet<String> = BTreeSet::new();
crate::codegen::proof_recognize::collect_called_fns(w, &mut raw);
let pmentions: BTreeSet<String> = raw
.iter()
.map(|n| aver_name_to_lean(n))
.filter(|n| program_index.contains_key(n))
.collect();
!pmentions.is_empty() && pmentions.is_subset(&scope) && scope.contains(&prev_subject)
});
if mentions.is_subset(&scope)
|| (mentions.contains(&subject) && scope.contains(&prev_subject))
|| lhs_rooted
|| premise_rooted
{
out.push(crate::codegen::lemma_discovery::CommittedLemma::reference(
name, text,
));
}
}
let (qualified_scope, qualified_subject) = consumer_law_qualified_scope(vb, law, ctx);
let consumer_module_idx = ctx
.active_module_scope()
.and_then(|s| ctx.modules.iter().position(|m| m.prefix == s));
for (module_idx, module) in ctx.modules.iter().enumerate() {
if let Some(consumer_idx) = consumer_module_idx
&& module_idx >= consumer_idx
{
continue;
}
let dep_index = dep_membership_index(module, ctx);
for prev in &module.verify_laws {
let VerifyKind::Law(prev_law) = &prev.kind else {
continue;
};
if let Some((name, text)) = dep_law_admissible(
module,
prev,
prev_law,
&qualified_scope,
&qualified_subject,
&dep_index,
ctx,
) {
out.push(crate::codegen::lemma_discovery::CommittedLemma::reference(
name, text,
));
}
}
}
out
}
fn law_is_userfn_to_builtin_bridge(law: &VerifyLaw) -> bool {
use crate::ast::Expr;
let dotted =
|e: &crate::ast::Spanned<Expr>| crate::codegen::common::expr_to_dotted_name(&e.node);
let Expr::FnCall(lc, _) = &law.lhs.node else {
return false;
};
let Some(lname) = dotted(lc) else {
return false;
};
if lname.contains('.') {
return false; }
match &law.rhs.node {
Expr::FnCall(rc, _) => dotted(rc).is_some_and(|n| n.contains('.')),
Expr::BinOp(..) => true,
_ => false,
}
}
fn bridge_law_lean_names(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> BTreeSet<String> {
earlier_law_cites(vb, law, ctx)
.into_iter()
.filter(|(_, l)| law_is_userfn_to_builtin_bridge(l))
.map(|(name, _)| name)
.collect()
}
fn earlier_law_cites<'a>(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &'a CodegenContext,
) -> Vec<(String, &'a VerifyLaw)> {
use crate::ast::{TopLevel, VerifyKind};
let inputs = crate::codegen::proof_lower::ProofLowerInputs::from_ctx(ctx);
let cone = crate::codegen::proof_lower::LawProofCone::compute(law, &vb.fn_name, &inputs);
let mut scope: BTreeSet<String> = cone
.pure_fns()
.iter()
.map(|fd| aver_name_to_lean(&fd.name))
.collect();
let subject = aver_name_to_lean(&vb.fn_name);
scope.insert(subject.clone());
let program_index: std::collections::BTreeMap<String, String> = program_fn_lean_names(ctx)
.into_iter()
.map(|l| (l.clone(), l))
.collect();
let mut out = Vec::new();
for item in &ctx.items {
let TopLevel::Verify(prev) = item else {
continue;
};
if prev.line == vb.line && prev.fn_name == vb.fn_name {
break;
}
let VerifyKind::Law(prev_law) = &prev.kind else {
continue;
};
if prev_law.when.is_some() {
continue;
}
if crate::codegen::cite_instantiate::law_rewrites_to_self(prev_law) {
continue;
}
let Some((name, stmt)) =
crate::codegen::lean::toplevel::law_as_lemma_statement(prev, prev_law, ctx)
else {
continue;
};
let text = format!("theorem {name} : {stmt} := by");
let mentions = crate::codegen::lemma_discovery::mentioned_fns(&text, &program_index);
if mentions.is_empty() {
continue;
}
let prev_subject = aver_name_to_lean(&prev.fn_name);
let lhs_mentions = crate::codegen::lemma_discovery::lemma_lhs_fns(&text, &program_index);
let lhs_rooted = !lhs_mentions.is_empty()
&& lhs_mentions.is_subset(&scope)
&& scope.contains(&prev_subject);
if mentions.is_subset(&scope)
|| (mentions.contains(&subject) && scope.contains(&prev_subject))
|| lhs_rooted
{
out.push((name, prev_law.as_ref()));
}
}
out
}
fn render_lean_arg(e: &crate::ast::Spanned<crate::ast::Expr>, ctx: &CodegenContext) -> String {
use crate::ast::Expr;
use crate::codegen::cite_instantiate::{HEAD, TAIL, ident_name};
if let Some(n) = ident_name(e) {
return match n {
HEAD => "head".to_string(),
TAIL => "tail".to_string(),
_ => match peano_role(n, ctx) {
Some(crate::codegen::proof_recognize::PeanoCtor::Zero) => "0".to_string(),
_ => aver_name_to_lean(n),
},
};
}
match &e.node {
Expr::Literal(lit) => render_lean_literal(lit),
Expr::List(items) => format!(
"[{}]",
items
.iter()
.map(|i| render_lean_arg(i, ctx))
.collect::<Vec<_>>()
.join(", ")
),
Expr::FnCall(callee, args) => {
let name =
crate::codegen::common::expr_to_dotted_name(&callee.node).unwrap_or_default();
let rendered: Vec<String> = args.iter().map(|a| render_lean_arg(a, ctx)).collect();
if rendered.len() == 1
&& matches!(
peano_role(&name, ctx),
Some(crate::codegen::proof_recognize::PeanoCtor::Succ)
)
{
return format!("({} + 1)", rendered[0]);
}
if name == "List.concat" && rendered.len() == 2 {
format!("({} ++ {})", rendered[0], rendered[1])
} else {
format!("({} {})", aver_name_to_lean(&name), rendered.join(" "))
}
}
Expr::Constructor(name, inner) => match peano_role(name, ctx) {
Some(crate::codegen::proof_recognize::PeanoCtor::Zero) => "0".to_string(),
Some(crate::codegen::proof_recognize::PeanoCtor::Succ) => match inner {
Some(e) => format!("({} + 1)", render_lean_arg(e, ctx)),
None => "0".to_string(),
},
None => match inner {
None => aver_name_to_lean(name),
Some(e) => format!("({} {})", aver_name_to_lean(name), render_lean_arg(e, ctx)),
},
},
Expr::Attr(inner, field) => format!("{}.{}", render_lean_arg(inner, ctx), field),
_ => String::new(),
}
}
fn peano_role(
dotted: &str,
ctx: &CodegenContext,
) -> Option<crate::codegen::proof_recognize::PeanoCtor> {
let (type_name, ctor) = dotted.rsplit_once('.')?;
crate::codegen::proof_recognize::peano_ctor_role(ctx, type_name, ctor)
}
fn render_lean_literal(lit: &crate::ast::Literal) -> String {
use crate::ast::Literal;
match lit {
Literal::Int(i) if *i < 0 => format!("({})", i),
Literal::Int(i) => format!("{}", i),
Literal::BigInt(s) => s.clone(),
Literal::Bool(b) => if *b { "true" } else { "false" }.to_string(),
Literal::Str(s) => format!("\"{}\"", crate::codegen::common::escape_string_literal(s)),
Literal::Float(f) => {
let s = f.to_string();
if s.contains('.') {
s
} else {
format!("{}.0", s)
}
}
Literal::Unit => "()".to_string(),
}
}
fn b_tight_decomposition_arms(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
ind_aver_name: &str,
law_uid: &str,
) -> Option<(String, String, Vec<String>)> {
let cites = earlier_law_cites(vb, law, ctx);
if cites.is_empty() {
return None;
}
let cited: Vec<&VerifyLaw> = cites.iter().map(|(_, l)| *l).collect();
let insts =
crate::codegen::cite_instantiate::compute_instantiations(law, ind_aver_name, &cited, ctx);
if insts.is_empty() {
return None;
}
let mut cited_fns: BTreeSet<String> = BTreeSet::new();
for c in &cited {
crate::codegen::proof_recognize::collect_called_fns(&c.lhs, &mut cited_fns);
crate::codegen::proof_recognize::collect_called_fns(&c.rhs, &mut cited_fns);
}
let (bridge_support, bridges, bridged_fns) =
lean_nat_lift_support(law, ctx, law_uid, &cited_fns);
let defs: Vec<String> = law_simp_defs(ctx, vb, law)
.into_iter()
.filter(|n| !bridged_fns.contains(n.trim_start_matches("_root_.")))
.collect();
let cited_names: Vec<String> = cites.iter().map(|(n, _)| n.clone()).collect();
let mut have_parts: Vec<String> = Vec::new();
let mut keys: Vec<String> = Vec::new();
let mut seen: BTreeSet<String> = BTreeSet::new();
for inst in &insts {
let call = format!(
"{} {}",
cites[inst.law_index].0,
inst.args
.iter()
.map(|a| render_lean_arg(a, ctx))
.collect::<Vec<_>>()
.join(" ")
);
if !seen.insert(call.clone()) {
continue;
}
let key = format!("key{}", keys.len());
have_parts.push(format!("have {key} := {call}"));
keys.push(key);
}
if keys.is_empty() {
return None;
}
let mut cons_set = defs.clone();
cons_set.push("ih".to_string());
cons_set.extend(keys.iter().cloned());
cons_set.extend(bridges.iter().cloned());
let s = cons_set.join(", ");
let arith = if bridges.is_empty() {
String::new()
} else {
format!(
" | (simp_all [{s}] <;> omega) | (simp [{s}] <;> omega) | (simp_all [{s}]; congr 1 <;> omega) | (simp [{s}]; congr 1 <;> omega)"
)
};
let cons = format!(
"{}; first | (simp_all [{s}]; done) | (simp [{s}]; done){arith}",
have_parts.join("; ")
);
let mut nil_set = defs;
nil_set.extend(cited_names);
nil_set.extend(bridges.iter().cloned());
let n = nil_set.join(", ");
let nil_omega = if bridges.is_empty() {
String::new()
} else {
format!(" | (simp [{n}] <;> omega) | (simp_all [{n}] <;> omega)")
};
let nil = format!("first | (simp [{n}]; done) | (simp_all [{n}]; done){nil_omega}");
Some((nil, cons, bridge_support))
}
fn fastpath_simp_entries(
ctx: &CodegenContext,
committed_names: &[String],
siblings: &[crate::codegen::lemma_discovery::CommittedLemma],
) -> Vec<String> {
let mut program_fns = program_fn_lean_names(ctx);
for module in &ctx.modules {
for fd in &module.fn_defs {
if crate::codegen::common::is_pure_fn(fd) {
program_fns.insert(format!("{}.{}", module.prefix, aver_name_to_lean(&fd.name)));
}
}
}
let mut pool: Vec<&crate::codegen::lemma_discovery::CommittedLemma> = ctx
.discovered_lemmas
.iter()
.filter(|l| committed_names.contains(&l.name))
.collect();
pool.extend(siblings.iter());
if pool.is_empty() {
return Vec::new();
}
crate::codegen::lemma_discovery::simp_entries(&pool, &program_fns)
}
fn feedback_source_fns(
ctx: &CodegenContext,
committed_names: &[String],
siblings: &[crate::codegen::lemma_discovery::CommittedLemma],
) -> BTreeSet<String> {
let lean_to_source: std::collections::BTreeMap<String, String> = ctx
.modules
.iter()
.flat_map(|m| m.fn_defs.iter())
.chain(ctx.fn_defs.iter())
.filter(|fd| crate::codegen::common::is_pure_fn(fd))
.map(|fd| (aver_name_to_lean(&fd.name), fd.name.clone()))
.collect();
let mut out = discovered_lemma_source_fns(ctx, committed_names);
for s in siblings {
out.extend(crate::codegen::lemma_discovery::mentioned_fns(
&s.text,
&lean_to_source,
));
}
out
}
enum VariantKind {
Leaf,
DirectRec,
IndirectRec,
}
fn classify_variant(variant: &TypeVariant, type_name: &str) -> VariantKind {
let mut has_indirect = false;
for field in &variant.fields {
if field.trim() == type_name {
return VariantKind::DirectRec;
}
if field_type_contains_indirect(field, type_name) {
has_indirect = true;
}
}
if has_indirect {
VariantKind::IndirectRec
} else {
VariantKind::Leaf
}
}
fn field_type_contains_indirect(field_type: &str, type_name: &str) -> bool {
if field_type.trim() == type_name {
return false;
}
field_type.contains(&format!("<{}", type_name))
|| field_type.contains(&format!("{}>", type_name))
|| field_type.contains(&format!(", {}", type_name))
|| field_type.contains(&format!("{},", type_name))
}
fn find_sum_type<'a>(
ctx: &'a CodegenContext,
name: &str,
) -> Option<(&'a String, &'a Vec<TypeVariant>)> {
ctx.modules
.iter()
.flat_map(|m| m.type_defs.iter())
.chain(ctx.type_defs.iter())
.find_map(|td| match td {
TypeDef::Sum {
name: n, variants, ..
} if n == name => Some((n, variants)),
_ => None,
})
}
fn is_recursive_sum(type_name: &str, variants: &[TypeVariant]) -> bool {
variants
.iter()
.any(|variant| variants_fields_contain_type(&variant.fields, type_name))
}
fn variants_fields_contain_type(fields: &[String], type_name: &str) -> bool {
fields.iter().any(|field| {
field.trim() == type_name
|| field.contains(&format!("<{}", type_name))
|| field.contains(&format!("{}>", type_name))
|| field.contains(&format!(", {}", type_name))
|| field.contains(&format!("{},", type_name))
})
}
fn find_induction_target<'a>(
law: &'a VerifyLaw,
ctx: &CodegenContext,
) -> Option<(usize, &'a str, &'a str)> {
for (index, given) in law.givens.iter().enumerate() {
if let Some((_, variants)) = find_sum_type(ctx, &given.type_name)
&& is_recursive_sum(&given.type_name, variants)
{
return Some((index, &given.name, &given.type_name));
}
}
None
}
fn has_indirect_variants(variants: &[TypeVariant], type_name: &str) -> bool {
variants.iter().any(|variant| {
matches!(
classify_variant(variant, type_name),
VariantKind::IndirectRec
)
})
}
fn premise_intro_names(law: &VerifyLaw, intro_names: &[String]) -> Vec<String> {
let mut names = Vec::new();
if law.when.is_some() {
names.extend(intro_names.iter().map(|name| format!("h_{name}")));
names.push("h_when".to_string());
}
names
}
fn is_linear_nat_arg(expr: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
use crate::ast::{Expr, Literal};
match &expr.node {
Expr::Ident(_) | Expr::Resolved { .. } => true,
Expr::Literal(Literal::Int(_)) => true,
Expr::FnCall(callee, args) => match super::shared::expr_dotted_name(callee) {
Some(name) => match name.rsplit('.').next().unwrap_or(name.as_str()) {
"S" => args.len() == 1 && is_linear_nat_arg(&args[0]),
"Z" => args.is_empty(),
_ => false,
},
None => false,
},
_ => false,
}
}
fn is_peano_compare_call(
expr: &crate::ast::Spanned<crate::ast::Expr>,
ctx: &CodegenContext,
) -> bool {
use crate::ast::Expr;
let Expr::FnCall(callee, args) = &expr.node else {
return false;
};
if args.len() != 2 {
return false;
}
let Some(name) = super::shared::expr_dotted_name(callee) else {
return false;
};
let mut names = BTreeSet::new();
names.insert(name);
if crate::codegen::proof_recognize::collect_nat_compare_ops_for_names(&names, ctx).is_empty() {
return false;
}
is_linear_nat_arg(&args[0]) && is_linear_nat_arg(&args[1])
}
fn negated_compare_inner(
expr: &crate::ast::Spanned<crate::ast::Expr>,
) -> Option<&crate::ast::Spanned<crate::ast::Expr>> {
use crate::ast::Expr;
let Expr::FnCall(callee, args) = &expr.node else {
return None;
};
if super::shared::expr_dotted_name(callee).as_deref() != Some("Bool.not") || args.len() != 1 {
return None;
}
Some(&args[0])
}
fn conditional_comparison_bridge_shape(law: &VerifyLaw, ctx: &CodegenContext) -> bool {
use crate::ast::{Expr, Literal};
let Some(when) = &law.when else {
return false;
};
if !matches!(&law.rhs.node, Expr::Literal(Literal::Bool(true))) {
return false;
}
if !is_peano_compare_call(&law.lhs, ctx) {
return false;
}
match negated_compare_inner(when) {
Some(inner) => is_peano_compare_call(inner, ctx),
None => is_peano_compare_call(when, ctx),
}
}
pub(in crate::codegen::lean) fn recognize_conditional_comparison_bridge(
law: &VerifyLaw,
ctx: &CodegenContext,
) -> bool {
conditional_comparison_bridge_shape(law, ctx)
}
pub(in crate::codegen::lean) fn emit_conditional_comparison_bridge_law(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
) -> Option<AutoProof> {
if !conditional_comparison_bridge_shape(law, ctx) {
return None;
}
let law_uid = format!(
"{}_{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name)
);
let mut extra: BTreeSet<String> = BTreeSet::new();
if let Some(when) = &law.when {
crate::codegen::proof_recognize::collect_called_fns(when, &mut extra);
}
let (bridge_support, bridge_names, _bridged) =
lean_nat_lift_support(law, ctx, &law_uid, &extra);
let has_compare_bridge = bridge_names
.iter()
.any(|n| n.ends_with("_isNatLe") || n.ends_with("_isNatLt") || n.ends_with("_isNatEq"));
if !has_compare_bridge {
return None;
}
let bridges = bridge_names.join(", ");
let intro = format!(" intro {} h_when", intro_names.join(" "));
let mut support = bridge_support;
let close = if let Some(inner) = law.when.as_ref().and_then(negated_compare_inner) {
let mut premise_fns: BTreeSet<String> = BTreeSet::new();
crate::codegen::proof_recognize::collect_called_fns(inner, &mut premise_fns);
let false_bridges: Vec<String> = crate::codegen::proof_recognize::collect_nat_compare_ops_for_names(
&premise_fns, ctx,
)
.into_iter()
.map(|op| {
let f = aver_name_to_lean(&op.fn_name);
let name = format!("{law_uid}_{f}_{}False", op.kind.bridge_suffix());
let false_prop = op.kind.false_prop();
let (driver, passenger) = if op.kind.induct_on_second() {
("b", "a")
} else {
("a", "b")
};
support.push(format!(
"theorem {name} : ∀ a b, ({f} a b = false) = ({false_prop}) := by\n intro a b\n induction {driver} generalizing {passenger} with\n | zero => cases {passenger} <;> first | (simp [{f}]) | (simp [{f}]; omega) | sorry\n | succ k ih => cases {passenger} <;> first | (simp [{f}, ih]) | (simp [{f}, ih]; omega) | sorry"
));
name
})
.collect();
let false_set = false_bridges.join(", ");
format!(
" first | (simp only [{bridges}] at ⊢; simp only [Bool.not_eq_true', {false_set}, {bridges}] at h_when; omega) | sorry"
)
} else {
format!(" first | (simp only [{bridges}] at h_when ⊢ <;> omega) | sorry")
};
Some(AutoProof {
support_lines: support,
body: Tactic::raw(vec![intro, close]),
replaces_theorem: false,
})
}
pub(in crate::codegen::lean) fn recognize_validated_wrapper(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> bool {
if law.when.is_none() {
return false;
}
let crate::ast::Expr::FnCall(callee, _) = &law.lhs.node else {
return false;
};
if super::shared::expr_dotted_name(callee).as_deref() != Some(vb.fn_name.as_str()) {
return false;
}
let rhs_is_result_ok = match &law.rhs.node {
crate::ast::Expr::FnCall(callee, args) => {
!args.is_empty()
&& super::shared::expr_dotted_name(callee).as_deref() == Some("Result.Ok")
}
crate::ast::Expr::Constructor(ctor, Some(_)) => ctor == "Result.Ok",
_ => false,
};
if !rhs_is_result_ok {
return false;
}
let Some(subject_fd) = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())
else {
return false;
};
matches!(
subject_fd.body.tail_expr().map(|e| &e.node),
Some(crate::ast::Expr::Match { .. })
)
}
fn collect_wrapper_guard_predicates(
expr: &crate::ast::Spanned<crate::ast::Expr>,
out: &mut BTreeSet<String>,
) {
if let crate::ast::Expr::Match { subject, arms } = &expr.node {
if let crate::ast::Expr::FnCall(callee, args) = &subject.node
&& super::shared::expr_dotted_name(callee).as_deref() == Some("Bool.not")
&& let Some(inner) = args.first()
&& let crate::ast::Expr::FnCall(gcallee, _) = &inner.node
&& let Some(g) = super::shared::expr_dotted_name(gcallee)
{
out.insert(g);
}
for arm in arms {
collect_wrapper_guard_predicates(&arm.body, out);
}
}
}
fn collect_called_dotted(expr: &crate::ast::Spanned<crate::ast::Expr>, out: &mut BTreeSet<String>) {
match &expr.node {
crate::ast::Expr::FnCall(f, args) => {
if let Some(name) = super::shared::expr_dotted_name(f) {
out.insert(name);
}
collect_called_dotted(f, out);
for a in args {
collect_called_dotted(a, out);
}
}
crate::ast::Expr::BinOp(_, l, r) => {
collect_called_dotted(l, out);
collect_called_dotted(r, out);
}
crate::ast::Expr::Attr(obj, _) => collect_called_dotted(obj, out),
crate::ast::Expr::Neg(inner) => collect_called_dotted(inner, out),
_ => {}
}
}
pub(in crate::codegen::lean) fn emit_validated_wrapper_law(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
) -> Option<AutoProof> {
if !recognize_validated_wrapper(vb, law, ctx) {
return None;
}
let subject_fd = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())?;
let subject = aver_name_to_lean(&vb.fn_name);
let intro = format!(" intro {} h_when", intro_names.join(" "));
let mut guards: BTreeSet<String> = BTreeSet::new();
if let Some(tail) = subject_fd.body.tail_expr() {
collect_wrapper_guard_predicates(tail, &mut guards);
}
let mut premise_fns: BTreeSet<String> = BTreeSet::new();
if let Some(when) = &law.when {
collect_called_dotted(when, &mut premise_fns);
}
guards.retain(|g| !premise_fns.contains(g));
let mut unfold = vec![format!("_root_.{subject}")];
unfold.extend(
guards
.iter()
.map(|g| format!("_root_.{}", aver_name_to_lean(g))),
);
let unfold_set = unfold.join(", ");
let arm = format!(
" | (simp only [{unfold_set}]; simp_all [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq] <;> (first | rfl | omega))"
);
let floor = if super::super::tactic_ir::speculative::probing() {
let id = format!("{}.{}", vb.fn_name, law.name);
super::super::tactic_ir::speculative::record_probed(&id);
format!(" | (trace \"AVERSPEC_SORRY:{id}\"; sorry)")
} else {
" | sorry".to_string()
};
Some(AutoProof {
support_lines: Vec::new(),
body: Tactic::raw(vec![intro, " first".to_string(), arm, floor]),
replaces_theorem: false,
})
}
pub(in crate::codegen::lean) fn recognize_conditional_inductive_generic(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> bool {
if law.when.is_none() {
return false;
}
if !matches!(&law.lhs.node, crate::ast::Expr::FnCall(..)) {
return false;
}
let Some(target_idx) = find_list_induction_target(law) else {
return false;
};
let other_lists = law
.givens
.iter()
.enumerate()
.filter(|(i, g)| *i != target_idx && g.type_name.trim().starts_with("List<"))
.count();
if other_lists > 1 {
return false;
}
let single_list = other_lists == 0;
if recognize_conditional_comparison_bridge(law, ctx) {
return false;
}
if single_list && law_recurses_on_cogiven(law, ctx, target_idx) {
return false;
}
let id = format!("{}.{}", vb.fn_name, law.name);
super::super::tactic_ir::speculative::admits(&id, other_lists == 1)
}
pub(in crate::codegen::lean) fn emit_conditional_inductive_generic_law(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
) -> Option<AutoProof> {
if !recognize_conditional_inductive_generic(vb, law, ctx) {
return None;
}
let target_idx = find_list_induction_target(law)?;
let target = intro_names.get(target_idx)?.clone();
let defs = law_simp_defs(ctx, vb, law)
.into_iter()
.collect::<Vec<_>>()
.join(", ");
let pool_names: Vec<String> = earlier_law_lemmas(vb, law, ctx)
.iter()
.map(|l| l.name.clone())
.collect();
let defs_pool = if pool_names.is_empty() {
defs.clone()
} else {
format!("{defs}, {}", pool_names.join(", "))
};
let with_append =
format!("{defs_pool}, List.cons_append, List.nil_append, List.singleton_append");
let bridge_uid = format!(
"{}_{}_L{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name),
vb.line
);
let mut bridge_extra: BTreeSet<String> = BTreeSet::new();
if let Some(when) = &law.when {
crate::codegen::proof_recognize::collect_called_fns(when, &mut bridge_extra);
}
let (bridge_support, bridge_names, _bridged) =
lean_nat_lift_support(law, ctx, &bridge_uid, &bridge_extra);
let cmp_bridges: Vec<String> = bridge_names
.into_iter()
.filter(|n| n.ends_with("_isNatLe") || n.ends_with("_isNatLt") || n.ends_with("_isNatEq"))
.collect();
let norm = "(try simp only [Bool.not_eq_true, Bool.not_eq_false] at h_when)".to_string();
let bridge_rung: Option<String> = if cmp_bridges.is_empty() {
None
} else {
let defs_pool_br = format!("{defs_pool}, {}", cmp_bridges.join(", "));
let bridges_csv = cmp_bridges.join(", ");
Some(format!(
" | (simp only [{with_append}, {bridges_csv}] at h_when ⊢ <;> (split <;> simp_all [{defs_pool_br}]) <;> (try omega) <;> done)"
))
};
let others: Vec<String> = law
.givens
.iter()
.enumerate()
.filter(|(i, g)| *i != target_idx && g.type_name.trim().starts_with("List<"))
.map(|(_, g)| aver_name_to_lean(&g.name))
.collect();
let case_other = if others.len() == 1 {
format!("cases {} <;> ", others[0])
} else {
String::new()
};
let before: Vec<String> = intro_names.iter().take(target_idx + 1).cloned().collect();
let after: Vec<String> = intro_names.iter().skip(target_idx + 1).cloned().collect();
let arm_intro = if after.is_empty() {
"intro h_when".to_string()
} else {
format!("intro {} h_when", after.join(" "))
};
let floor = if super::super::tactic_ir::speculative::probing() {
let id = format!("{}.{}", vb.fn_name, law.name);
super::super::tactic_ir::speculative::record_probed(&id);
format!(" | (trace \"AVERSPEC_SORRY:{id}\"; sorry)")
} else {
" | sorry".to_string()
};
let subject = aver_name_to_lean(&vb.fn_name);
let subject_split_rung = format!(
" | (simp only [{subject}] <;> (split <;> simp_all [{defs_pool}, h_when]) <;> done)"
);
let is_wrapper = matches!(
&law.lhs.node,
crate::ast::Expr::FnCall(callee, _)
if super::shared::expr_dotted_name(callee).as_deref().is_some_and(|o| o != vb.fn_name)
);
let law_uid = format!(
"{}_{}_L{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name),
vb.line
);
let and_intro = format!("{law_uid}_andTrue");
let not_false = format!("{law_uid}_notTrueOfFalse");
let not_ne = format!("{law_uid}_notTrueOfNe");
let (adapters, wrapper_rung): (Vec<String>, Option<String>) = if is_wrapper {
let adapters = vec![
format!(
"private theorem {and_intro} {{a b : Bool}} (ha : a = true) (hb : b = true) : (a && b) = true := by\n cases ha; cases hb; rfl"
),
format!(
"private theorem {not_false} {{a : Bool}} (h : a = false) : (!a) = true := by\n cases h; rfl"
),
format!(
"private theorem {not_ne} {{a : Bool}} (h : ¬(a = true)) : (!a) = true := by\n cases a <;> simp_all"
),
];
let pool_suffix = if pool_names.is_empty() {
String::new()
} else {
format!(", {}", pool_names.join(", "))
};
let sbe =
format!("(maxDepth := 12) only [*, {and_intro}, {not_false}, {not_ne}{pool_suffix}]");
let mut solve_alts: Vec<String> = Vec::new();
for name in &pool_names {
solve_alts.push(format!("(apply {name} <;> solve_by_elim {sbe} <;> done)"));
}
solve_alts.push(format!("(solve_by_elim {sbe} <;> done)"));
let rung = format!(
" | (simp only [{subject}] <;> split <;> (first | {}))",
solve_alts.join(" | ")
);
(adapters, Some(rung))
} else {
(Vec::new(), None)
};
let mut body = vec![format!(" intro {}", before.join(" "))];
body.extend([
format!(" induction {target} with"),
" | nil =>".to_string(),
format!(" {arm_intro}"),
format!(" {norm}"),
" first".to_string(),
format!(" | ({case_other}simp_all [{with_append}] <;> done)"),
format!(" | (simp_all [{defs_pool}] <;> done)"),
format!(" | (simp only [{subject}] <;> simp_all [{defs_pool}, h_when] <;> done)"),
]);
if let Some(rung) = &bridge_rung {
body.push(rung.clone());
}
body.push(floor.clone());
body.extend([
" | cons hd tl ih =>".to_string(),
format!(" {arm_intro}"),
format!(" {norm}"),
" first".to_string(),
format!(" | ({case_other}simp_all [{with_append}] <;> done)"),
format!(
" | ({case_other}simp only [{with_append}] at h_when ⊢ <;> (split <;> simp_all [{defs_pool}]) <;> done)"
),
format!(" | (simp only [{with_append}] <;> simp_all [{defs_pool}, h_when] <;> done)"),
format!(" | (split <;> simp_all [{defs_pool}, h_when] <;> done)"),
format!(" | (simp_all [{defs_pool}, h_when] <;> done)"),
format!(" | (cases hd <;> simp_all [{defs_pool}, h_when] <;> done)"),
subject_split_rung,
]);
if let Some(rung) = bridge_rung {
body.push(rung);
}
if let Some(rung) = wrapper_rung {
body.push(rung);
}
body.push(floor);
let mut support = bridge_support;
support.extend(adapters);
Some(AutoProof {
support_lines: support,
body: Tactic::raw(body),
replaces_theorem: false,
})
}
#[allow(clippy::too_many_arguments)]
pub(super) fn emit_structural_induction_law(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
_theorem_base: &str,
_quant_params: &str,
_theorem_prop: &str,
discovered: &[String],
) -> Option<AutoProof> {
if law.when.is_some() {
return None;
}
let verified_recurses_on_list = ctx
.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())
.is_some_and(|fd| {
crate::codegen::recursion::detect::single_list_structural_param_index(fd).is_some()
});
let list_target = find_list_induction_target(law);
let sum_target = find_induction_target(law, ctx);
if verified_recurses_on_list && let Some(target_idx) = list_target {
return emit_list_induction(vb, law, ctx, intro_names, target_idx, discovered);
}
if let Some(proof) = emit_both_args_peeling_law(vb, law, ctx, intro_names) {
return Some(proof);
}
if let Some((target_idx, _target_name, type_name)) = sum_target {
let (_, variants) = find_sum_type(ctx, type_name)?;
if has_indirect_variants(variants, type_name) {
return None;
}
return emit_simple_induction(
vb,
law,
ctx,
intro_names,
target_idx,
type_name,
variants,
discovered,
);
}
if let Some(target_idx) = list_target {
return emit_list_induction(vb, law, ctx, intro_names, target_idx, discovered);
}
None
}
fn find_list_induction_target(law: &VerifyLaw) -> Option<usize> {
law.givens
.iter()
.position(|given| given.type_name.trim().starts_with("List<"))
}
fn law_recurses_on_cogiven(law: &VerifyLaw, ctx: &CodegenContext, target_idx: usize) -> bool {
use crate::ast::Expr;
let cogivens: BTreeSet<&str> = law
.givens
.iter()
.enumerate()
.filter(|(i, _)| *i != target_idx)
.map(|(_, g)| g.name.as_str())
.collect();
let target: &str = law.givens[target_idx].name.as_str();
fn is_ident(expr: &crate::ast::Spanned<Expr>, name: &str) -> bool {
matches!(&expr.node, Expr::Ident(n) | Expr::Resolved { name: n, .. } if n == name)
}
fn scan(
expr: &crate::ast::Spanned<Expr>,
cogivens: &BTreeSet<&str>,
target: &str,
ctx: &CodegenContext,
) -> bool {
match &expr.node {
Expr::FnCall(callee, args) => {
if let Some(name) = super::shared::expr_dotted_name(callee)
&& let Some(fd) =
ctx.fn_def_by_name(&name, ctx.active_module_scope().as_deref())
{
let takes_target = args.iter().any(|a| is_ident(a, target));
if takes_target {
for (i, arg) in args.iter().enumerate() {
let arg_is_cogiven = matches!(
&arg.node,
Expr::Ident(n) | Expr::Resolved { name: n, .. } if cogivens.contains(n.as_str())
);
if arg_is_cogiven
&& crate::codegen::recursion::detect::param_decremented_in_recursion(
fd, i,
)
{
return true;
}
}
}
}
args.iter().any(|a| scan(a, cogivens, target, ctx))
|| scan(callee, cogivens, target, ctx)
}
Expr::Attr(e, _) | Expr::Neg(e) | Expr::ErrorProp(e) => scan(e, cogivens, target, ctx),
Expr::BinOp(_, l, r) => {
scan(l, cogivens, target, ctx) || scan(r, cogivens, target, ctx)
}
Expr::Constructor(_, payload) => payload
.as_ref()
.is_some_and(|e| scan(e, cogivens, target, ctx)),
Expr::List(es) | Expr::Tuple(es) => es.iter().any(|e| scan(e, cogivens, target, ctx)),
Expr::Match { subject, arms } => {
scan(subject, cogivens, target, ctx)
|| arms
.iter()
.any(|arm| scan(&arm.body, cogivens, target, ctx))
}
_ => false,
}
}
[Some(&law.lhs), Some(&law.rhs), law.when.as_ref()]
.into_iter()
.flatten()
.any(|e| scan(e, &cogivens, target, ctx))
}
enum MapFoldQuery {
Get,
Has,
}
struct MapFoldHomomorphism {
query: MapFoldQuery,
key_lean: String,
}
fn call_dotted_name(expr: &crate::ast::Spanned<crate::ast::Expr>) -> Option<String> {
use crate::ast::Expr;
match &expr.node {
Expr::FnCall(callee, _) => super::shared::expr_dotted_name(callee),
_ => None,
}
}
fn map_query_over_fold(
expr: &crate::ast::Spanned<crate::ast::Expr>,
fold_fn: &str,
list_given: &str,
given_names: &[String],
) -> Option<String> {
use crate::ast::Expr;
let Expr::FnCall(_, args) = &expr.node else {
return None;
};
if args.len() != 2 {
return None;
}
let Expr::FnCall(map_callee, map_args) = &args[0].node else {
return None;
};
if super::shared::expr_dotted_name(map_callee).as_deref() != Some(fold_fn) {
return None;
}
if map_args.len() != 1
|| !matches!(&map_args[0].node, Expr::Ident(n) | Expr::Resolved { name: n, .. } if n == list_given)
{
return None;
}
let key = match &args[1].node {
Expr::Ident(n) | Expr::Resolved { name: n, .. } => n.clone(),
_ => return None,
};
if key == list_given || !given_names.iter().any(|g| g == &key) {
return None;
}
Some(key)
}
fn recognize_map_fold_homomorphism(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
target_idx: usize,
) -> Option<MapFoldHomomorphism> {
use crate::ast::Expr;
let fd = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())?;
crate::codegen::recursion::detect::single_list_structural_param_index(fd)?;
if !fold_step_updates_map(fd, ctx) {
return None;
}
let list_given = &law.givens.get(target_idx)?.name;
let given_names: Vec<String> = law.givens.iter().map(|g| g.name.clone()).collect();
let recognize_side = |side: &crate::ast::Spanned<Expr>| -> Option<(MapFoldQuery, String)> {
match call_dotted_name(side).as_deref() {
Some("Option.withDefault") | Some("Map.getD") => {
let Expr::FnCall(_, args) = &side.node else {
return None;
};
let inner = args.first()?;
if call_dotted_name(inner).as_deref() != Some("Map.get") {
return None;
}
let key = map_query_over_fold(inner, &vb.fn_name, list_given, &given_names)?;
Some((MapFoldQuery::Get, key))
}
Some("Map.get") => {
let key = map_query_over_fold(side, &vb.fn_name, list_given, &given_names)?;
Some((MapFoldQuery::Get, key))
}
Some("Map.has") => {
let key = map_query_over_fold(side, &vb.fn_name, list_given, &given_names)?;
Some((MapFoldQuery::Has, key))
}
_ => None,
}
};
let (query, key) = recognize_side(&law.lhs).or_else(|| recognize_side(&law.rhs))?;
let key_lean = intro_names
.get(given_names.iter().position(|g| g == &key)?)?
.clone();
Some(MapFoldHomomorphism { query, key_lean })
}
fn fold_step_updates_map(fd: &crate::ast::FnDef, ctx: &CodegenContext) -> bool {
fn expr_calls_map_set(expr: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
use crate::ast::Expr;
match &expr.node {
Expr::FnCall(callee, args) => {
super::shared::expr_dotted_name(callee).as_deref() == Some("Map.set")
|| args.iter().any(expr_calls_map_set)
|| expr_calls_map_set(callee)
}
Expr::Attr(base, _) => expr_calls_map_set(base),
Expr::BinOp(_, l, r) => expr_calls_map_set(l) || expr_calls_map_set(r),
Expr::Neg(inner) | Expr::ErrorProp(inner) => expr_calls_map_set(inner),
Expr::Match { subject, arms } => {
expr_calls_map_set(subject) || arms.iter().any(|a| expr_calls_map_set(&a.body))
}
Expr::Constructor(_, inner) => inner.as_deref().is_some_and(expr_calls_map_set),
Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => {
items.iter().any(expr_calls_map_set)
}
_ => false,
}
}
fn body_calls_map_set(fd: &crate::ast::FnDef) -> bool {
fd.body.stmts().iter().any(|s| match s {
crate::ast::Stmt::Expr(e) | crate::ast::Stmt::Binding(_, _, e) => expr_calls_map_set(e),
})
}
fn collect_called_fns(
expr: &crate::ast::Spanned<crate::ast::Expr>,
out: &mut BTreeSet<String>,
) {
use crate::ast::Expr;
if let Expr::FnCall(callee, args) = &expr.node {
if let Some(n) = super::shared::expr_dotted_name(callee) {
out.insert(n);
}
args.iter().for_each(|a| collect_called_fns(a, out));
}
match &expr.node {
Expr::FnCall(callee, _) => collect_called_fns(callee, out),
Expr::Attr(base, _) => collect_called_fns(base, out),
Expr::BinOp(_, l, r) => {
collect_called_fns(l, out);
collect_called_fns(r, out);
}
Expr::Neg(i) | Expr::ErrorProp(i) => collect_called_fns(i, out),
Expr::Match { subject, arms } => {
collect_called_fns(subject, out);
arms.iter().for_each(|a| collect_called_fns(&a.body, out));
}
Expr::Constructor(_, Some(i)) => collect_called_fns(i, out),
Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => {
items.iter().for_each(|i| collect_called_fns(i, out));
}
_ => {}
}
}
if body_calls_map_set(fd) {
return true;
}
let mut callees = BTreeSet::new();
for s in fd.body.stmts() {
match s {
crate::ast::Stmt::Expr(e) | crate::ast::Stmt::Binding(_, _, e) => {
collect_called_fns(e, &mut callees)
}
}
}
callees.iter().any(|name| {
ctx.fn_def_by_name(name, ctx.active_module_scope().as_deref())
.is_some_and(body_calls_map_set)
})
}
fn emit_map_fold_homomorphism(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
target_idx: usize,
plan: &MapFoldHomomorphism,
) -> AutoProof {
let simp_list = law_simp_defs(ctx, vb, law)
.into_iter()
.collect::<Vec<_>>()
.join(", ");
let target_lean = &intro_names[target_idx];
let key = &plan.key_lean;
let fold_lean = aver_name_to_lean(&vb.fn_name);
let map_lemmas = match plan.query {
MapFoldQuery::Get => "AverMap.get_set_self, AverMap.get_set_ne, beq_iff_eq",
MapFoldQuery::Has => "AverMap.has_set, beq_iff_eq",
};
let close = match plan.query {
MapFoldQuery::Get => " <;> omega",
MapFoldQuery::Has => "",
};
let nil_simp = format!("{simp_list}, AverMap.get, AverMap.has");
let rung_close = match plan.query {
MapFoldQuery::Get => format!("simp_all [{map_lemmas}, hkey, hget]{close}"),
MapFoldQuery::Has => format!("simp_all [{map_lemmas}, hkey, hget]; try rfl; done"),
};
let cons_arm = format!(
"| cons head tail ih => simp only [{simp_list}, List.contains_cons] at * <;> by_cases hkey : head = {key} <;> cases hget : AverMap.get ({fold_lean} tail) head <;> first | ({rung_close}) | (simp_all [{map_lemmas}, hkey, hget]; done) | sorry"
);
let proof_lines = vec![
format!(" intro {}", intro_names.join(" ")),
format!(" induction {target_lean} with"),
format!(" | nil => first | (simp [{nil_simp}]) | sorry"),
format!(" {cons_arm}"),
];
AutoProof {
support_lines: Vec::new(),
body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
replaces_theorem: false,
}
}
pub(super) struct FunInductionTarget {
pub(super) fn_lean: String,
pub(super) args: Vec<String>,
}
fn fn_body_has_match(fd: &crate::ast::FnDef) -> bool {
fn expr_has_match(expr: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
use crate::ast::Expr;
match &expr.node {
Expr::Match { .. } => true,
Expr::FnCall(callee, args) => expr_has_match(callee) || args.iter().any(expr_has_match),
Expr::Attr(base, _) | Expr::Neg(base) | Expr::ErrorProp(base) => expr_has_match(base),
Expr::BinOp(_, l, r) => expr_has_match(l) || expr_has_match(r),
Expr::Constructor(_, Some(inner)) => expr_has_match(inner),
Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => {
items.iter().any(expr_has_match)
}
_ => false,
}
}
fd.body.stmts().iter().any(|s| match s {
crate::ast::Stmt::Expr(e) | crate::ast::Stmt::Binding(_, _, e) => expr_has_match(e),
})
}
pub(super) fn find_fun_induction_targets(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
) -> Vec<FunInductionTarget> {
let given_to_intro = |name: &str| -> Option<String> {
law.givens
.iter()
.position(|g| g.name == name)
.and_then(|i| intro_names.get(i).cloned())
};
let recursive_names = crate::codegen::lean::recursive_pure_fn_names(ctx);
let induct_fns: std::collections::HashSet<String> = ctx
.modules
.iter()
.flat_map(|m| m.fn_defs.iter())
.chain(ctx.fn_defs.iter())
.filter(|fd| {
crate::codegen::common::is_pure_fn(fd)
&& recursive_names.contains(&fd.name)
&& fn_body_has_match(fd)
})
.map(|fd| fd.name.clone())
.collect();
let mut candidates: Vec<FunInductionTarget> = Vec::new();
fn walk(
expr: &crate::ast::Spanned<crate::ast::Expr>,
recursive: &std::collections::HashSet<String>,
given_to_intro: &dyn Fn(&str) -> Option<String>,
out: &mut Vec<FunInductionTarget>,
) {
use crate::ast::Expr;
if let Expr::FnCall(callee, args) = &expr.node
&& let Some(name) = super::shared::expr_dotted_name(callee)
&& recursive.contains(&name)
{
let mut arg_leans = Vec::with_capacity(args.len());
let mut all_free = !args.is_empty();
for a in args {
let leaf = match &a.node {
Expr::Ident(n) | Expr::Resolved { name: n, .. } => given_to_intro(n),
_ => None,
};
match leaf {
Some(l) => arg_leans.push(l),
None => {
all_free = false;
break;
}
}
}
if all_free {
out.push(FunInductionTarget {
fn_lean: aver_name_to_lean(&name),
args: arg_leans,
});
}
}
match &expr.node {
Expr::FnCall(callee, args) => {
walk(callee, recursive, given_to_intro, out);
args.iter()
.for_each(|a| walk(a, recursive, given_to_intro, out));
}
Expr::Attr(base, _) | Expr::Neg(base) | Expr::ErrorProp(base) => {
walk(base, recursive, given_to_intro, out)
}
Expr::BinOp(_, l, r) => {
walk(l, recursive, given_to_intro, out);
walk(r, recursive, given_to_intro, out);
}
Expr::Match { subject, arms } => {
walk(subject, recursive, given_to_intro, out);
arms.iter()
.for_each(|a| walk(&a.body, recursive, given_to_intro, out));
}
Expr::Constructor(_, Some(inner)) => walk(inner, recursive, given_to_intro, out),
Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => items
.iter()
.for_each(|i| walk(i, recursive, given_to_intro, out)),
_ => {}
}
}
walk(&law.lhs, &induct_fns, &given_to_intro, &mut candidates);
walk(&law.rhs, &induct_fns, &given_to_intro, &mut candidates);
let subject_lean = aver_name_to_lean(&vb.fn_name);
candidates.sort_by_key(|c| c.fn_lean != subject_lean);
let mut seen: BTreeSet<(String, Vec<String>)> = BTreeSet::new();
candidates.retain(|c| seen.insert((c.fn_lean.clone(), c.args.clone())));
candidates
}
fn wrap_with_fun_induction_rung(
intro_line: String,
body_lines: Vec<String>,
targets: &[FunInductionTarget],
simp_defs: &str,
) -> Vec<String> {
let defs = if simp_defs.is_empty() {
String::new()
} else {
format!("[{simp_defs}]")
};
let closer = format!(
"first | (simp_all {defs}; done) | (simp_all {defs}; omega) | (simp_all {defs} <;> omega) | (simp_all {defs} <;> (repeat' split) <;> omega)"
);
let mut out = vec![intro_line, " first".to_string()];
for t in targets {
out.push(format!(
" | (fun_induction {} {} <;> ({}))",
t.fn_lean,
t.args.join(" "),
closer
));
}
out.push(" | (".to_string());
for line in &body_lines {
out.push(format!(" {line}"));
}
if let Some(last) = out.last_mut() {
last.push(')');
}
out
}
struct NilHelper {
text: String,
name: String,
}
fn take_drop_nil_helper(
fd: &crate::ast::FnDef,
law_uid: &str,
ctx: &CodegenContext,
) -> Option<NilHelper> {
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, single_list_structural_param_index,
};
let list_idx = single_list_structural_param_index(fd)?;
let nat_idx = fd.params.iter().enumerate().position(|(i, (_, ty))| {
i != list_idx
&& (ty.trim() == "Nat"
|| crate::codegen::proof_recognize::peano_type_named(ctx, ty.trim()).is_some())
&& param_decremented_in_recursion(fd, i)
})?;
let f = aver_name_to_lean(&fd.name);
let name = format!("{law_uid}_{f}_nil");
let driver = "n_d";
let args: Vec<String> = (0..fd.params.len())
.map(|i| {
if i == list_idx {
"[]".to_string()
} else if i == nat_idx {
driver.to_string()
} else {
format!("p_{i}")
}
})
.collect();
let binders: Vec<String> = (0..fd.params.len())
.filter(|i| *i != list_idx)
.map(|i| {
if i == nat_idx {
driver.to_string()
} else {
format!("p_{i}")
}
})
.collect();
let binders = binders.join(" ");
let body = super::intro_then_first(
std::slice::from_ref(&binders),
vec![format!("cases {driver} <;> simp [{f}]")],
);
let text = super::support_theorem(
&format!(
"theorem {name} : ∀ {binders}, {f} {args} = [] := by",
args = args.join(" ")
),
body,
);
Some(NilHelper { text, name })
}
fn zip_nil_helper(
fd: &crate::ast::FnDef,
law_uid: &str,
ctx: &CodegenContext,
) -> Option<NilHelper> {
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, single_list_structural_param_index,
};
let first_list = single_list_structural_param_index(fd)?;
let has_decremented_nat = fd.params.iter().enumerate().any(|(i, (_, ty))| {
i != first_list
&& (ty.trim() == "Nat"
|| crate::codegen::proof_recognize::peano_type_named(ctx, ty.trim()).is_some())
&& param_decremented_in_recursion(fd, i)
});
if has_decremented_nat {
return None;
}
let second_list = fd.params.iter().enumerate().position(|(i, (_, ty))| {
i != first_list && (ty.trim_start().starts_with("List<") || ty.trim() == "List")
})?;
let f = aver_name_to_lean(&fd.name);
let name = format!("{law_uid}_{f}_nil");
let driver = "xs_d";
let args: Vec<String> = (0..fd.params.len())
.map(|i| {
if i == second_list {
"[]".to_string()
} else if i == first_list {
driver.to_string()
} else {
format!("p_{i}")
}
})
.collect();
let binders: Vec<String> = (0..fd.params.len())
.filter(|i| *i != second_list)
.map(|i| {
if i == first_list {
driver.to_string()
} else {
format!("p_{i}")
}
})
.collect();
let binders = binders.join(" ");
let body = super::intro_then_first(
std::slice::from_ref(&binders),
vec![format!("cases {driver} <;> simp [{f}]")],
);
let text = super::support_theorem(
&format!(
"theorem {name} : ∀ {binders}, {f} {args} = [] := by",
args = args.join(" ")
),
body,
);
Some(NilHelper { text, name })
}
fn given_ident_name(expr: &crate::ast::Spanned<crate::ast::Expr>) -> Option<&str> {
use crate::ast::Expr;
match &expr.node {
Expr::Ident(n) | Expr::Resolved { name: n, .. } => Some(n.as_str()),
_ => None,
}
}
struct CountComposition {
inner_count: String,
list_given: String,
}
fn recognize_count_composition(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
) -> Option<CountComposition> {
use crate::ast::Expr;
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, single_list_structural_param_index,
};
if law.when.is_some() {
return None;
}
let fd = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())?;
let list_idx = single_list_structural_param_index(fd)?;
if !fd.params.iter().enumerate().any(|(i, (_, ty))| {
i != list_idx
&& (ty.trim() == "Nat"
|| crate::codegen::proof_recognize::peano_type_named(ctx, ty.trim()).is_some())
&& param_decremented_in_recursion(fd, i)
}) {
return None;
}
let add_fns: BTreeSet<String> =
crate::codegen::proof_recognize::collect_nat_arith_ops_in_law(law, ctx)
.into_iter()
.filter(|op| op.kind == crate::codegen::proof_recognize::NatArithKind::Add)
.map(|op| op.fn_name)
.collect();
if add_fns.is_empty() {
return None;
}
let composed = |side: &crate::ast::Spanned<Expr>| -> Option<(String, String, String)> {
let Expr::FnCall(callee, args) = &side.node else {
return None;
};
if super::shared::expr_dotted_name(callee).as_deref() != Some(vb.fn_name.as_str())
|| args.len() != 2
{
return None;
}
let Expr::FnCall(op_callee, op_args) = &args[0].node else {
return None;
};
let op_name = super::shared::expr_dotted_name(op_callee)?;
if !add_fns.contains(&op_name) || op_args.len() != 2 {
return None;
}
let a = given_ident_name(&op_args[0])?.to_string();
let b = given_ident_name(&op_args[1])?.to_string();
let c = given_ident_name(&args[1])?.to_string();
Some((a, b, c))
};
let nested = |side: &crate::ast::Spanned<Expr>| -> Option<(String, String, String)> {
let Expr::FnCall(callee, args) = &side.node else {
return None;
};
if super::shared::expr_dotted_name(callee).as_deref() != Some(vb.fn_name.as_str())
|| args.len() != 2
{
return None;
}
let a = given_ident_name(&args[0])?.to_string();
let Expr::FnCall(inner_callee, inner_args) = &args[1].node else {
return None;
};
if super::shared::expr_dotted_name(inner_callee).as_deref() != Some(vb.fn_name.as_str())
|| inner_args.len() != 2
{
return None;
}
let b = given_ident_name(&inner_args[0])?.to_string();
let c = given_ident_name(&inner_args[1])?.to_string();
Some((a, b, c))
};
let (composed_side, nested_side) = composed(&law.lhs)
.map(|c| (c, nested(&law.rhs)))
.or_else(|| composed(&law.rhs).map(|c| (c, nested(&law.lhs))))?;
let (ca, cb, cc) = composed_side;
let (na, nb, nc) = nested_side?;
if ca != na || cb != nb || cc != nc {
return None;
}
let given_type = |name: &str| {
law.givens
.iter()
.find(|g| g.name == name)
.map(|g| g.type_name.trim().to_string())
};
let is_nat = |name: &str| -> bool {
given_type(name).is_some_and(|ty| {
ty == "Nat" || crate::codegen::proof_recognize::peano_type_named(ctx, &ty).is_some()
})
};
let is_list = |name: &str| -> bool {
given_type(name).is_some_and(|ty| ty.starts_with("List<") || ty == "List")
};
if ca == cb || !is_nat(&ca) || !is_nat(&cb) || !is_list(&cc) {
return None;
}
Some(CountComposition {
inner_count: cb,
list_given: cc,
})
}
fn emit_count_composition_rung(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
law_uid: &str,
) -> Option<(Vec<String>, Vec<String>)> {
let plan = recognize_count_composition(vb, law, ctx)?;
let driver = law
.givens
.iter()
.position(|g| g.name == plan.inner_count)
.and_then(|i| intro_names.get(i).cloned())?;
let list_intro = law
.givens
.iter()
.position(|g| g.name == plan.list_given)
.and_then(|i| intro_names.get(i).cloned())?;
let (arith_support, arith_bridges, _bridged) =
lean_nat_lift_support(law, ctx, law_uid, &BTreeSet::new());
let add_bridge = arith_bridges
.iter()
.find(|n| n.ends_with("_isNatAdd"))
.cloned()?;
let mut support: Vec<String> = arith_support;
let mut nil_simp: Vec<String> = Vec::new();
if let Some(fd) = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())
&& let Some(h) = take_drop_nil_helper(fd, law_uid, ctx)
{
nil_simp.push(h.name.clone());
support.push(h.text);
}
let mut base_set: BTreeSet<String> = law_simp_defs(ctx, vb, law);
base_set.insert(add_bridge.clone());
base_set.extend(nil_simp.iter().cloned());
let base = base_set.iter().cloned().collect::<Vec<_>>().join(", ");
let mut unfold_set: BTreeSet<String> = law_simp_defs(ctx, vb, law);
unfold_set.insert(add_bridge.clone());
unfold_set.insert("Nat.add_succ".to_string());
let unfold = unfold_set.iter().cloned().collect::<Vec<_>>().join(", ");
let mut cons_set = base_set.clone();
cons_set.insert("ih".to_string());
let cons = cons_set.iter().cloned().collect::<Vec<_>>().join(", ");
let rung = vec![
" | (".to_string(),
format!(" induction {driver} generalizing {list_intro} with"),
format!(" | zero => cases {list_intro} <;> simp_all [{base}]"),
format!(
" | succ k ih => cases {list_intro} <;> simp only [{unfold}] at * <;> simp_all [{cons}])"
),
];
Some((support, rung))
}
fn emit_synchronous_multivar_induction(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
law_uid: &str,
) -> Option<(Vec<String>, Vec<String>)> {
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, single_list_structural_param_index,
};
let subject = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())?;
let list_idx = single_list_structural_param_index(subject)?;
let nat_param = subject
.params
.iter()
.enumerate()
.find_map(|(i, (pname, ty))| {
(i != list_idx
&& (ty.trim() == "Nat"
|| crate::codegen::proof_recognize::peano_type_named(ctx, ty.trim()).is_some())
&& param_decremented_in_recursion(subject, i))
.then_some(pname)
})?;
let driver_given_idx = law.givens.iter().position(|g| &g.name == nat_param)?;
let driver = intro_names.get(driver_given_idx)?.clone();
let mut other_intros: Vec<String> = Vec::new();
let mut cases_intros: Vec<String> = Vec::new();
for (i, g) in law.givens.iter().enumerate() {
if i == driver_given_idx {
continue;
}
let Some(intro) = intro_names.get(i) else {
continue;
};
other_intros.push(intro.clone());
let ty = g.type_name.trim();
let is_nat =
ty == "Nat" || crate::codegen::proof_recognize::peano_type_named(ctx, ty).is_some();
let is_list = ty.starts_with("List<") || ty == "List";
if is_nat || is_list {
cases_intros.push(intro.clone());
}
}
let mut support: Vec<String> = Vec::new();
let mut helper_names: Vec<String> = Vec::new();
for src_name in super::shared::law_simp_source_names(ctx, vb, law) {
let Some(fd) = ctx.fn_def_by_name(&src_name, ctx.active_module_scope().as_deref()) else {
continue;
};
let helper =
take_drop_nil_helper(fd, law_uid, ctx).or_else(|| zip_nil_helper(fd, law_uid, ctx));
if let Some(h) = helper {
support.push(h.text);
helper_names.push(h.name);
}
}
let mut simp_set: BTreeSet<String> = law_simp_defs(ctx, vb, law);
simp_set.extend(helper_names.iter().cloned());
simp_set.insert("List.cons_append".to_string());
simp_set.insert("List.nil_append".to_string());
let simp = simp_set.into_iter().collect::<Vec<_>>().join(", ");
let arm = if cases_intros.is_empty() {
format!("simp_all [{simp}]")
} else {
format!(
"cases {} <;> simp_all [{simp}]",
cases_intros.join(" <;> cases ")
)
};
let generalizing = if other_intros.is_empty() {
String::new()
} else {
format!(" generalizing {}", other_intros.join(" "))
};
let rung = vec![
" | (".to_string(),
format!(" induction {driver}{generalizing} with"),
format!(" | zero => {arm}"),
format!(" | succ k ih => {arm})"),
];
Some((support, rung))
}
fn emit_list_induction(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
target_idx: usize,
discovered: &[String],
) -> Option<AutoProof> {
if discovered.is_empty()
&& let Some(plan) = recognize_map_fold_homomorphism(vb, law, ctx, intro_names, target_idx)
{
return Some(emit_map_fold_homomorphism(
vb,
law,
ctx,
intro_names,
target_idx,
&plan,
));
}
let mut simp_defs: BTreeSet<String> = law_simp_defs(ctx, vb, law);
let law_uid = format!(
"{}_{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name)
);
let discovered_simp = discovered_simp_entries(ctx, discovered);
let siblings = earlier_law_lemmas(vb, law, ctx);
let fast_simp = fastpath_simp_entries(ctx, discovered, &siblings);
let simp_list_plain = simp_defs.iter().cloned().collect::<Vec<_>>().join(", ");
simp_defs.extend(discovered_simp.iter().cloned());
let simp_list = simp_defs.into_iter().collect::<Vec<_>>().join(", ");
let target_lean = &intro_names[target_idx];
let second_list: Option<String> = law
.givens
.iter()
.enumerate()
.find(|(i, g)| *i != target_idx && g.type_name.trim_start().starts_with("List"))
.and_then(|(i, _)| intro_names.get(i).cloned());
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, param_threaded_in_recursion,
single_list_structural_param_index,
};
let gen_given: Option<(String, bool)> = ctx
.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())
.and_then(|fd| {
let lidx = single_list_structural_param_index(fd)?;
let given_intro = |fn_param: &str| -> Option<String> {
law.givens
.iter()
.position(|g| g.name == fn_param)
.map(|gi| intro_names[gi].clone())
};
if let Some((_, (pname, _))) = fd.params.iter().enumerate().find(|(i, (_, ty))| {
*i != lidx
&& (ty.trim() == "Nat"
|| crate::codegen::proof_recognize::peano_type_named(ctx, ty.trim())
.is_some())
&& param_decremented_in_recursion(fd, *i)
}) {
return given_intro(pname).map(|n| (n, true));
}
if let Some((_, (pname, _))) = fd
.params
.iter()
.enumerate()
.find(|(i, _)| *i != lidx && param_threaded_in_recursion(fd, *i))
{
return given_intro(pname).map(|n| (n, false));
}
None
});
let split_set = if simp_list.is_empty() {
"List.cons_append, List.singleton_append, List.nil_append".to_string()
} else {
format!("{simp_list}, List.cons_append, List.singleton_append, List.nil_append")
};
let split_set_plain = if simp_list_plain.is_empty() {
"List.cons_append, List.singleton_append, List.nil_append".to_string()
} else {
format!("{simp_list_plain}, List.cons_append, List.singleton_append, List.nil_append")
};
let mk_arms = |arm_simp: &str,
arm_split: &str,
bridges: Option<&str>,
cases_extra: Option<&str>,
with_sorry: bool|
-> (String, String) {
let nil_bridge = bridges
.map(|b| format!(" | (simp [{arm_simp}]; simp only [{b}] <;> omega)"))
.unwrap_or_default();
let cons_bridge = bridges
.map(|b| format!(" | (simp_all [{arm_simp}]; simp only [{b}] <;> omega)"))
.unwrap_or_default();
let split_bridge = bridges
.map(|b| format!(" <;> (try simp only [{b}])"))
.unwrap_or_default();
let cases_extra_branch = cases_extra
.map(|s| format!(" | (cases tail <;> simp_all [{s}] <;> omega)"))
.unwrap_or_default();
let split_extra_branch = cases_extra
.map(|s| format!(" | (simp only [{s}]; split <;> simp_all [{s}] <;> omega)"))
.unwrap_or_default();
let second_cases_nil = second_list
.as_deref()
.map(|sl| format!(" | (cases {sl} <;> simp_all [{arm_simp}] <;> omega)"))
.unwrap_or_default();
let second_cases_cons = second_list
.as_deref()
.map(|sl| {
format!(
" | (cases {sl} <;> simp_all [{arm_simp}] <;> omega) | (cases tail <;> cases {sl} <;> simp_all [{arm_simp}] <;> omega)"
)
})
.unwrap_or_default();
let congr_nil =
format!(" | (simp [{arm_simp}]; congr 1 <;> simp_all [{arm_simp}] <;> omega)");
let congr_cons =
format!(" | (simp_all [{arm_simp}]; congr 1 <;> simp_all [{arm_simp}] <;> omega)");
let tail = if with_sorry { " | sorry" } else { "" };
(
format!(
"| nil => first | (simp [{arm_simp}]; done) | (simp [{arm_simp}]; omega){nil_bridge} | (simp only [{arm_split}]; split <;> simp_all [{arm_simp}]{split_bridge} <;> omega){second_cases_nil}{congr_nil}{tail}"
),
format!(
"| cons head tail ih => first | (simp_all [{arm_simp}]; done) | (simp_all [{arm_simp}]; omega){cons_bridge} | (simp only [{arm_split}]; split <;> simp_all [{arm_simp}]{split_bridge} <;> omega) | (cases tail <;> simp_all [{arm_simp}] <;> omega){cases_extra_branch}{split_extra_branch}{second_cases_cons}{congr_cons}{tail}"
),
)
};
let mut proof_lines = vec![format!(" intro {}", intro_names.join(" "))];
let mut support_lines = Vec::new();
if let Some((gv, needs_cases)) = gen_given.as_ref().filter(|_| fast_simp.is_empty()) {
let mul_ac_set = if simp_list.is_empty() {
"Int.mul_assoc, Int.mul_comm, Int.mul_left_comm, Int.mul_one, Int.one_mul".to_string()
} else {
format!(
"{simp_list}, Int.mul_assoc, Int.mul_comm, Int.mul_left_comm, Int.mul_one, Int.one_mul"
)
};
let ladder = |s: &str| -> String {
format!(
"first | ({s} [{d}]; done) | ({s} [{d}]; omega) | ({s} [{ac}]; done) | (simp only [{sp}]; split <;> simp_all [{d}] <;> omega) | sorry",
d = simp_list,
sp = split_set,
ac = mul_ac_set
)
};
let wrap = |arm: &str| -> String {
if *needs_cases {
format!("cases {gv} <;> ({arm})")
} else {
arm.to_string()
}
};
proof_lines.push(format!(
" induction {} generalizing {} with",
target_lean, gv
));
proof_lines.push(format!(" | nil => {}", wrap(&ladder("simp"))));
proof_lines.push(format!(
" | cons head tail ih => {}",
wrap(&ladder("simp_all"))
));
} else if fast_simp.is_empty() && gen_given.is_none() {
let (arith_support, arith_bridges, bridged_fns) =
lean_nat_lift_support(law, ctx, &law_uid, &BTreeSet::new());
let cases_extra = if arith_bridges.is_empty() {
None
} else {
support_lines.extend(arith_support);
let set: BTreeSet<String> = simp_list
.split(", ")
.map(String::from)
.chain(arith_bridges.iter().cloned())
.filter(|n| !n.is_empty() && !bridged_fns.contains(n))
.collect();
Some(set.into_iter().collect::<Vec<_>>().join(", "))
};
let (nil_arm, cons_arm) =
mk_arms(&simp_list, &split_set, None, cases_extra.as_deref(), true);
proof_lines.push(format!(" induction {} with", target_lean));
proof_lines.push(format!(" {nil_arm}"));
proof_lines.push(format!(" {cons_arm}"));
} else {
let lemma_fns = feedback_source_fns(ctx, discovered, &siblings);
let (arith_support, arith_bridges, bridged_fns) =
lean_nat_lift_support(law, ctx, &law_uid, &lemma_fns);
const COMMUTE_NORMALIZERS: &[&str] = &[
"Nat.add_comm",
"Nat.mul_comm",
"Int.add_comm",
"Int.mul_comm",
];
let mut fast_lemmas: Vec<String> = fast_simp.clone();
fast_lemmas.extend(arith_bridges.iter().cloned());
if !fast_simp.is_empty() {
fast_lemmas.extend(COMMUTE_NORMALIZERS.iter().map(|s| s.to_string()));
}
let fast_unfolds: BTreeSet<String> = law_simp_defs(ctx, vb, law)
.into_iter()
.chain(fast_simp.iter().cloned())
.chain(arith_bridges.iter().cloned())
.chain(
COMMUTE_NORMALIZERS
.iter()
.filter(|_| !fast_simp.is_empty())
.map(|s| s.to_string()),
)
.filter(|n| !bridged_fns.contains(n))
.collect();
let bridge_set = if arith_bridges.is_empty() {
None
} else {
Some(arith_bridges.join(", "))
};
let arm_forward_siblings: Vec<String> = fast_simp
.iter()
.filter(|e| !e.starts_with("← ") && !discovered_simp.contains(*e))
.cloned()
.collect();
proof_lines.push(" first".to_string());
if !discovered_simp.is_empty() {
let (nil_plain, cons_plain) = mk_arms(
&simp_list_plain,
&split_set_plain,
bridge_set.as_deref(),
None,
false,
);
proof_lines.push(format!(" | (induction {} with", target_lean));
proof_lines.push(format!(" {nil_plain}"));
proof_lines.push(format!(" {cons_plain})"));
}
if !fast_simp.is_empty() {
proof_lines.push(format!(" | (simp only [{}]; done)", fast_simp.join(", ")));
}
{
let bridge_names = bridge_law_lean_names(vb, law, ctx);
let strip = |e: &String| e.trim_start_matches("← ").to_string();
let non_bridge: Vec<String> = fast_simp
.iter()
.filter(|e| !bridge_names.contains(&strip(e)))
.cloned()
.collect();
let bridge: Vec<String> = fast_simp
.iter()
.filter(|e| bridge_names.contains(&strip(e)))
.cloned()
.collect();
if !non_bridge.is_empty() && !bridge.is_empty() {
proof_lines.push(format!(
" | (simp only [{}] <;> (try simp only [{}]) <;> (try simp only [List.append_assoc, List.cons_append, List.nil_append, List.singleton_append]) <;> done)",
non_bridge.join(", "),
bridge.join(", ")
));
}
}
proof_lines.push(format!(
" | (simp only [{}] <;> omega)",
fast_lemmas.join(", ")
));
let fast_lemmas_set: BTreeSet<String> = fast_lemmas.iter().cloned().collect();
if fast_unfolds != fast_lemmas_set {
proof_lines.push(format!(
" | (simp only [{}] <;> omega)",
fast_unfolds.into_iter().collect::<Vec<_>>().join(", ")
));
}
if let Some((gv, needs_cases)) = gen_given.as_ref() {
let gen_simp = {
let mut v: Vec<String> = simp_list.split(", ").map(String::from).collect();
v.extend(arm_forward_siblings.iter().cloned());
v.retain(|s| !s.is_empty());
v.join(", ")
};
let gen_split = if gen_simp.is_empty() {
"List.cons_append".to_string()
} else {
format!("{gen_simp}, List.cons_append")
};
let ladder = |s: &str| -> String {
let bridge_arm = bridge_set
.as_deref()
.map(|b| format!(" | ({s} [{gen_simp}]; simp only [{b}] <;> omega)"))
.unwrap_or_default();
let split_bridge = bridge_set
.as_deref()
.map(|b| format!(" <;> (try simp only [{b}])"))
.unwrap_or_default();
format!(
"first | ({s} [{gen_simp}]; done) | ({s} [{gen_simp}]; omega){bridge_arm} | (simp only [{gen_split}]; split <;> simp_all [{gen_simp}]{split_bridge} <;> omega) | sorry"
)
};
let wrap = |arm: &str| -> String {
if *needs_cases {
format!("cases {gv} <;> ({arm})")
} else {
arm.to_string()
}
};
proof_lines.push(format!(
" | (induction {} generalizing {} with",
target_lean, gv
));
proof_lines.push(format!(" | nil => {}", wrap(&ladder("simp"))));
proof_lines.push(format!(
" | cons head tail ih => {})",
wrap(&ladder("simp_all"))
));
} else if arm_forward_siblings.is_empty() {
let (nil_arm, cons_arm) =
mk_arms(&simp_list, &split_set, bridge_set.as_deref(), None, true);
proof_lines.push(format!(" | (induction {} with", target_lean));
proof_lines.push(format!(" {nil_arm}"));
proof_lines.push(format!(" {cons_arm})"));
} else {
let (nil_a, cons_a) =
mk_arms(&simp_list, &split_set, bridge_set.as_deref(), None, false);
proof_lines.push(format!(" | (induction {} with", target_lean));
proof_lines.push(format!(" {nil_a}"));
proof_lines.push(format!(" {cons_a})"));
let simp_b = {
let mut v: Vec<String> = simp_list.split(", ").map(String::from).collect();
v.extend(arm_forward_siblings.iter().cloned());
v.retain(|s| !s.is_empty());
v.join(", ")
};
let split_b = if simp_b.is_empty() {
"List.cons_append".to_string()
} else {
format!("{simp_b}, List.cons_append")
};
let (nil_b, cons_b) = mk_arms(&simp_b, &split_b, bridge_set.as_deref(), None, true);
proof_lines.push(format!(" | (induction {} with", target_lean));
proof_lines.push(format!(" {nil_b}"));
proof_lines.push(format!(" {cons_b})"));
}
support_lines.extend(discovered_support_lines(ctx, vb, law, discovered));
support_lines.extend(arith_support);
}
if discovered.is_empty() && fast_simp.is_empty() {
let targets = find_fun_induction_targets(vb, law, ctx, intro_names);
if !targets.is_empty() {
let (refl_support, refl_names) = lean_refl_support(vb, law, ctx, &law_uid);
let refl_simp_list = if refl_names.is_empty() {
simp_list.clone()
} else if simp_list.is_empty() {
refl_names.join(", ")
} else {
format!("{simp_list}, {}", refl_names.join(", "))
};
support_lines.extend(refl_support);
let intro_line = proof_lines.remove(0);
proof_lines =
wrap_with_fun_induction_rung(intro_line, proof_lines, &targets, &refl_simp_list);
}
let splice_leading_rung = |proof_lines: &mut Vec<String>, rung: Vec<String>| {
let intro_line = proof_lines.remove(0);
if proof_lines.first().map(String::as_str) == Some(" first") {
let mut wrapped = vec![intro_line, " first".to_string()];
wrapped.extend(rung);
wrapped.extend(proof_lines.drain(1..));
*proof_lines = wrapped;
} else {
let mut wrapped = vec![intro_line, " first".to_string()];
wrapped.extend(rung);
wrapped.push(" | (".to_string());
for line in proof_lines.iter() {
wrapped.push(format!(" {line}"));
}
if let Some(last) = wrapped.last_mut() {
last.push(')');
}
*proof_lines = wrapped;
}
};
if let Some((multivar_support, rung)) =
emit_synchronous_multivar_induction(vb, law, ctx, intro_names, &law_uid)
{
support_lines.extend(multivar_support);
splice_leading_rung(&mut proof_lines, rung);
}
if let Some((compose_support, rung)) =
emit_count_composition_rung(vb, law, ctx, intro_names, &law_uid)
{
support_lines.extend(compose_support);
splice_leading_rung(&mut proof_lines, rung);
}
}
if law.when.is_none()
&& gen_given.is_none()
&& let Some((nil_body, cons_body, bridge_support)) =
b_tight_decomposition_arms(vb, law, ctx, &law.givens[target_idx].name, &law_uid)
{
support_lines.extend(bridge_support);
let rung = vec![
format!(" | (induction {target_lean} with"),
format!(" | nil => {nil_body}"),
format!(" | cons head tail ih => {cons_body})"),
];
let intro_line = proof_lines.remove(0);
if proof_lines.first().map(String::as_str) == Some(" first") {
let mut wrapped = vec![intro_line, " first".to_string()];
wrapped.extend(rung);
wrapped.extend(proof_lines.drain(1..));
proof_lines = wrapped;
} else {
let mut wrapped = vec![intro_line, " first".to_string()];
wrapped.extend(rung);
wrapped.push(" | (".to_string());
for line in &proof_lines {
wrapped.push(format!(" {line}"));
}
if let Some(last) = wrapped.last_mut() {
last.push(')');
}
proof_lines = wrapped;
}
}
{
let mut seen: BTreeSet<String> = BTreeSet::new();
support_lines.retain(|line| seen.insert(line.clone()));
}
Some(AutoProof {
support_lines,
body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
replaces_theorem: false,
})
}
fn both_args_peeling_comm_theorem(fn_lean: &str, law_uid: &str) -> (String, String) {
let name = format!("{law_uid}_{fn_lean}_comm");
let ladder = format!(
"first | (cases b <;> simp_all [{fn_lean}]; done) | (cases b <;> simp_all [{fn_lean}]; omega) | sorry"
);
let text = format!(
"theorem {name} : ∀ (a b : Nat), {fn_lean} a b = {fn_lean} b a := by\n intro a b\n induction a generalizing b with\n | zero => {ladder}\n | succ k ih => {ladder}"
);
(text, name)
}
fn consumed_comm_lemmas(
ctx: &CodegenContext,
vb: &VerifyBlock,
law: &VerifyLaw,
law_uid: &str,
) -> (Vec<String>, Vec<String>) {
let mut support = Vec::new();
let mut names = Vec::new();
for src_name in super::shared::law_simp_source_names(ctx, vb, law) {
if src_name == vb.fn_name {
continue;
}
let Some(fd) = ctx.fn_def_by_name(&src_name, ctx.active_module_scope().as_deref()) else {
continue;
};
if crate::codegen::proof_recognize::both_args_peeling_is_commutative(fd, ctx).is_none() {
continue;
}
let fn_lean = aver_name_to_lean(&src_name);
let (text, name) = both_args_peeling_comm_theorem(&fn_lean, law_uid);
support.push(text);
names.push(name);
}
(support, names)
}
fn emit_both_args_peeling_law(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
) -> Option<AutoProof> {
if law.givens.len() != 2 && law.givens.len() != 3 {
return None;
}
let fd = ctx.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())?;
if !crate::codegen::recursion::detect::recurses_decrementing_both_args(fd) {
return None;
}
let param_type = fd.params.first()?.1.trim().to_string();
crate::codegen::proof_recognize::peano_type_named(ctx, ¶m_type)?;
if law.givens.iter().any(|g| g.type_name.trim() != param_type) {
return None;
}
if intro_names.len() != law.givens.len() {
return None;
}
let given_names: Vec<String> = law.givens.iter().map(|g| g.name.clone()).collect();
let is_comm_assoc =
crate::codegen::proof_recognize::recognize_binary_law_shape(law, &vb.fn_name, &given_names)
.is_some();
let law_uid = format!(
"{}_{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name)
);
let (bridge_support, bridge_names, _bridged) =
lean_nat_lift_support(law, ctx, &law_uid, &BTreeSet::new());
let has_compare_bridge = bridge_names
.iter()
.any(|n| n.ends_with("_isNatLe") || n.ends_with("_isNatLt") || n.ends_with("_isNatEq"));
let relational = !is_comm_assoc && law.givens.len() == 2 && has_compare_bridge;
if !is_comm_assoc && !relational {
return None;
}
let simp_list = law_simp_defs(ctx, vb, law)
.into_iter()
.collect::<Vec<_>>()
.join(", ");
let induct_on = &intro_names[0];
let rest = &intro_names[1..];
let generalizing = rest.join(" ");
let cases_prefix = rest
.iter()
.map(|g| format!("cases {g} <;> "))
.collect::<String>();
let bridge_rung = if relational {
let all_simp = if bridge_names.is_empty() {
simp_list.clone()
} else {
format!("{simp_list}, {}", bridge_names.join(", "))
};
format!(" | ({cases_prefix}simp_all [{all_simp}] <;> omega)")
} else {
String::new()
};
let ladder = format!(
"first | ({cases_prefix}simp_all [{simp_list}]; done) | ({cases_prefix}simp_all [{simp_list}]; omega){bridge_rung} | sorry"
);
let proof_lines = vec![
format!(" intro {}", intro_names.join(" ")),
format!(" induction {induct_on} generalizing {generalizing} with"),
format!(" | zero => {ladder}"),
format!(" | succ k ih => {ladder}"),
];
Some(AutoProof {
support_lines: if relational {
bridge_support
} else {
Vec::new()
},
body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
replaces_theorem: false,
})
}
#[allow(clippy::too_many_arguments)]
fn emit_simple_induction(
vb: &VerifyBlock,
law: &VerifyLaw,
ctx: &CodegenContext,
intro_names: &[String],
target_idx: usize,
type_name: &str,
variants: &[TypeVariant],
discovered: &[String],
) -> Option<AutoProof> {
let mut simp_defs: BTreeSet<String> = law_simp_defs(ctx, vb, law);
let discovered_simp = discovered_simp_entries(ctx, discovered);
let siblings = earlier_law_lemmas(vb, law, ctx);
let fast_simp = fastpath_simp_entries(ctx, discovered, &siblings);
simp_defs.extend(discovered_simp.iter().cloned());
let simp_list = simp_defs.into_iter().collect::<Vec<_>>().join(", ");
let target_lean = &intro_names[target_idx];
let premise_names = premise_intro_names(law, intro_names);
let law_uid = format!(
"{}_{}",
aver_name_to_lean(&vb.fn_name),
aver_name_to_lean(&law.name)
);
let lemma_fns = feedback_source_fns(ctx, discovered, &siblings);
let (arith_support, arith_bridges, bridged_fns) =
lean_nat_lift_support(law, ctx, &law_uid, &lemma_fns);
let mut intro_parts = intro_names.to_vec();
intro_parts.extend(premise_names.iter().cloned());
let peano = crate::codegen::proof_recognize::peano_type_named(ctx, type_name);
let arm_bridge = if !arith_bridges.is_empty() {
Some(arith_bridges.join(", "))
} else {
None
};
let (comm_support, comm_lemma_names) = consumed_comm_lemmas(ctx, vb, law, &law_uid);
let comm_arm: Option<(String, String)> = if comm_lemma_names.is_empty() {
None
} else {
let commd_fns: BTreeSet<String> = comm_lemma_names
.iter()
.filter_map(|n| n.strip_suffix("_comm"))
.filter_map(|s| s.strip_prefix(&format!("{law_uid}_")))
.map(str::to_string)
.collect();
let mut comm_set: Vec<String> = law_simp_defs(ctx, vb, law)
.into_iter()
.filter(|d| !commd_fns.contains(d))
.collect();
comm_set.extend(comm_lemma_names.iter().cloned());
let set = comm_set.join(", ");
Some((
format!(" | (simp [{set}]; done)"),
format!(" | (simp_all [{set}]; done)"),
))
};
let mul_ac_arm: Option<(String, String)> = if arith_bridges.iter().any(|b| b == "Nat.mul_assoc")
{
let bridge_thms = arith_bridges.iter().filter(|b| b.starts_with(&law_uid));
let mut acset: Vec<String> = law_simp_defs(ctx, vb, law)
.into_iter()
.filter(|d| !bridged_fns.contains(d.trim_start_matches("_root_.")))
.collect();
acset.extend(bridge_thms.cloned());
for lemma in [
"Nat.mul_assoc",
"Nat.mul_comm",
"Nat.mul_left_comm",
"Nat.mul_one",
"Nat.one_mul",
] {
acset.push(lemma.to_string());
}
let set = acset.join(", ");
Some((
format!(" | (simp [{set}]; done)"),
format!(" | (simp_all [{set}]; done)"),
))
} else {
None
};
let sibling_set = if fast_simp.is_empty() {
None
} else if simp_list.is_empty() {
Some(fast_simp.join(", "))
} else {
Some(format!("{simp_list}, {}", fast_simp.join(", ")))
};
let sibling_leaf = sibling_set
.as_deref()
.map(|s| format!(" | (simp [{s}]; done)"))
.unwrap_or_default();
let sibling_rec = sibling_set
.as_deref()
.map(|s| format!(" | (simp_all [{s}]; done)"))
.unwrap_or_default();
let mut arm_lines: Vec<String> = Vec::new();
for variant in variants {
let lean_variant = match &peano {
Some(p) if variant.name == p.base_ctor => "zero".to_string(),
Some(p) if variant.name == p.succ_ctor => "succ".to_string(),
_ => to_lower_first(&variant.name),
};
let field_binders: Vec<String> = (0..variant.fields.len())
.map(|index| format!("f{}", index))
.collect();
match classify_variant(variant, type_name) {
VariantKind::Leaf => {
let binders = if field_binders.is_empty() {
String::new()
} else {
format!(" {}", field_binders.join(" "))
};
let bridge = arm_bridge
.as_deref()
.map(|b| format!(" | (simp [{d}]; simp only [{b}] <;> omega)", d = simp_list))
.unwrap_or_default();
let comm = comm_arm
.as_ref()
.map(|(leaf, _)| leaf.as_str())
.unwrap_or_default();
let mul_ac = mul_ac_arm
.as_ref()
.map(|(leaf, _)| leaf.as_str())
.unwrap_or_default();
arm_lines.push(format!(
"| {v}{b} => first | (simp [{d}]; done) | (simp [{d}]; omega){bridge}{comm}{mul_ac}{sibling} | sorry",
v = lean_variant,
b = binders,
d = simp_list,
sibling = sibling_leaf
));
}
VariantKind::DirectRec => {
let ih_names: Vec<String> = variant
.fields
.iter()
.enumerate()
.filter(|(_, field)| field.trim() == type_name)
.map(|(index, _)| format!("ih{}", index))
.collect();
let bridge = arm_bridge
.as_deref()
.map(|b| {
format!(
" | (simp_all [{d}]; simp only [{b}] <;> omega)",
d = simp_list
)
})
.unwrap_or_default();
let comm = comm_arm
.as_ref()
.map(|(_, rec)| rec.as_str())
.unwrap_or_default();
let mul_ac = mul_ac_arm
.as_ref()
.map(|(_, rec)| rec.as_str())
.unwrap_or_default();
arm_lines.push(format!(
"| {v} {b} {ih} => first | (simp_all [{d}]; done) | (simp_all [{d}]; omega){bridge}{comm}{mul_ac}{sibling} | sorry",
v = lean_variant,
b = field_binders.join(" "),
ih = ih_names.join(" "),
d = simp_list,
sibling = sibling_rec
));
}
VariantKind::IndirectRec => return None,
}
}
use crate::codegen::recursion::detect::{
param_decremented_in_recursion, param_threaded_in_recursion,
};
let acc_generalize: Option<(String, String)> = ctx
.fn_def_by_name(&vb.fn_name, ctx.active_module_scope().as_deref())
.and_then(|fd| {
let driver_idx =
(0..fd.params.len()).find(|&i| param_decremented_in_recursion(fd, i))?;
let acc_idx = (0..fd.params.len())
.find(|&i| i != driver_idx && param_threaded_in_recursion(fd, i))?;
let driver_given = law
.givens
.iter()
.position(|g| g.name == fd.params[driver_idx].0)?;
if law.givens[driver_given].type_name.trim() != type_name {
return None;
}
let acc_intro = law
.givens
.iter()
.position(|g| g.name == fd.params[acc_idx].0)
.map(|gi| intro_names[gi].clone())?;
Some((intro_names[driver_given].clone(), acc_intro))
});
let (effective_target, gen_clause) = match &acc_generalize {
Some((driver, acc)) => (driver.clone(), format!(" generalizing {acc}")),
None => (target_lean.clone(), String::new()),
};
let mut proof_lines = vec![format!(" intro {}", intro_parts.join(" "))];
if arith_bridges.is_empty() && fast_simp.is_empty() {
proof_lines.push(format!(
" induction {}{} with",
effective_target, gen_clause
));
proof_lines.extend(arm_lines.into_iter().map(|a| format!(" {a}")));
} else {
const COMMUTE_NORMALIZERS: &[&str] = &[
"Nat.add_comm",
"Nat.mul_comm",
"Int.add_comm",
"Int.mul_comm",
];
let mut fast_lemmas: Vec<String> = fast_simp.clone();
fast_lemmas.extend(arith_bridges.iter().cloned());
if !fast_simp.is_empty() {
fast_lemmas.extend(COMMUTE_NORMALIZERS.iter().map(|s| s.to_string()));
}
proof_lines.push(" first".to_string());
if !fast_simp.is_empty() {
proof_lines.push(format!(" | (simp only [{}]; done)", fast_simp.join(", ")));
}
proof_lines.push(format!(
" | (simp only [{}] <;> omega)",
fast_lemmas.join(", ")
));
if !fast_simp.is_empty() {
let fast_unfolds: BTreeSet<String> = law_simp_defs(ctx, vb, law)
.into_iter()
.chain(fast_simp.iter().cloned())
.chain(arith_bridges.iter().cloned())
.chain(COMMUTE_NORMALIZERS.iter().map(|s| s.to_string()))
.filter(|n| !bridged_fns.contains(n))
.collect();
let fast_lemmas_set: BTreeSet<String> = fast_lemmas.iter().cloned().collect();
if fast_unfolds != fast_lemmas_set {
proof_lines.push(format!(
" | (simp only [{}] <;> omega)",
fast_unfolds.into_iter().collect::<Vec<_>>().join(", ")
));
}
}
proof_lines.push(format!(
" | (induction {}{} with",
effective_target, gen_clause
));
let last = arm_lines.len().saturating_sub(1);
for (idx, arm) in arm_lines.into_iter().enumerate() {
if idx == last {
proof_lines.push(format!(" {arm})"));
} else {
proof_lines.push(format!(" {arm}"));
}
}
}
let mut support_lines = discovered_support_lines(ctx, vb, law, discovered);
support_lines.extend(arith_support);
support_lines.extend(comm_support);
Some(AutoProof {
support_lines,
body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
replaces_theorem: false,
})
}
pub fn residual_probe_body(thm_lines: &[&str], probe_name: &str) -> Option<String> {
residual_probe_body_dump(thm_lines, probe_name, None)
}
pub fn residual_probe_body_dump(
thm_lines: &[&str],
probe_name: &str,
dump_label: Option<&str>,
) -> Option<String> {
let stmt_line = thm_lines.first()?;
let after_kw = stmt_line.trim_start().strip_prefix("theorem ")?;
let name_end = after_kw.find(char::is_whitespace)?;
let rest = &after_kw[name_end..]; if !rest.trim_end().ends_with(":= by") {
return None;
}
let mut intro_line: Option<&str> = None;
let mut induction_line: Option<&str> = None;
let mut arm_lines: Vec<&str> = Vec::new();
let mut simp_defs: BTreeSet<String> = BTreeSet::new();
for line in &thm_lines[1..] {
let t = line.trim_start();
if t.starts_with("intro ") && intro_line.is_none() {
intro_line = Some(line);
} else if (t.starts_with("induction ") && t.ends_with(" with")) && induction_line.is_none()
{
induction_line = Some(line);
} else if t.starts_with("| ") && induction_line.is_some() {
arm_lines.push(line);
}
collect_simp_idents(line, &mut simp_defs);
}
let induction_line = induction_line?;
if arm_lines.is_empty() {
return None;
}
simp_defs.insert("List.cons_append".to_string());
let simp_set = simp_defs.iter().cloned().collect::<Vec<_>>().join(", ");
let strip = format!("(try simp only [{simp_set}])");
let arm_tail = match dump_label {
Some(label) => {
let dump_set = simp_defs
.iter()
.filter(|n| !is_nat_bridge_lemma(n))
.cloned()
.collect::<Vec<_>>()
.join(", ");
let s = format!("(try simp only [{dump_set}])");
format!(
" {s} <;> (try split) <;> (try split) <;> {s}; \
all_goals (try aver_dump_goal \"{label}\")"
)
}
None => format!(" {strip}"),
};
let mut out = vec![format!("theorem {probe_name}{rest}")];
if let Some(intro) = intro_line {
out.push(format!(" {}", intro.trim_start()));
}
out.push(format!(" {}", induction_line.trim_start()));
for arm in arm_lines {
let arm = arm.trim();
if let Some(arrow) = arm.find("=>") {
let head = arm[..arrow + 2].trim_end();
out.push(format!(" {head}{arm_tail}"));
} else {
out.push(format!(" {arm}{arm_tail}"));
}
}
Some(out.join("\n"))
}
fn is_nat_bridge_lemma(name: &str) -> bool {
name.ends_with("_isNatLe") || name.ends_with("_isNatLt") || name.ends_with("_isNatEq")
}
fn collect_simp_idents(line: &str, set: &mut BTreeSet<String>) {
let mut rest = line;
while let Some(open) = rest.find('[') {
let after = &rest[open + 1..];
let Some(close) = after.find(']') else { break };
let inner = &after[..close];
for tok in inner.split(',') {
let tok = tok.trim();
if tok.is_empty() || tok.starts_with("← ") || tok == "List.cons_append" {
continue;
}
if tok
.chars()
.all(|c| c.is_alphanumeric() || c == '_' || c == '.' || c == '\'')
{
set.insert(tok.to_string());
}
}
rest = &after[close + 1..];
}
}
#[cfg(test)]
mod topology_tests {
use super::topology_admits;
#[test]
fn cited_dep_admissible_only_when_emitted_before_consumer() {
const ENTRY: usize = usize::MAX;
assert!(topology_admits(Some(&(0, 40)), (ENTRY, 10)));
assert!(topology_admits(Some(&(2, 15)), (2, 80)));
assert!(topology_admits(Some(&(1, 9999)), (3, 5)));
assert!(topology_admits(None, (2, 30)));
assert!(!topology_admits(Some(&(2, 90)), (2, 30)));
assert!(!topology_admits(Some(&(4, 1)), (3, 500)));
assert!(!topology_admits(Some(&(2, 30)), (2, 30)));
}
}