From b8475299baad3aba36a5cfdb221b8697da93dcb8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 26 Jul 2024 11:32:35 +0200 Subject: [PATCH 1/4] fix: improve proof search in IndPredBelow `MVarId.apply` is clever in the order it returns mvars, by putting those arising from non-dependent arguments first. If we lean on that behavior, this fixes #1672. --- src/Lean/Meta/IndPredBelow.lean | 23 +++++++++++------------ tests/lean/run/1672.lean | 8 ++++++++ 2 files changed, 19 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/1672.lean diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index d9822f1ffa9c..10bad0a76f84 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -232,10 +232,11 @@ def mkBelowDecl (ctx : Context) : MetaM Declaration := do partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do m.withContext do let mTy ← m.getType - if depth = 0 then - trace[Meta.IndPredBelow.search] "searching for {mTy}: ran out of max depth" - return false - else + withTraceNodeBefore `Meta.IndPredBelow.search (do pure m!"searching for {mTy}") do + trace[Meta.IndPredBelow.search] "Search goal:{m}" + if depth = 0 then + trace[Meta.IndPredBelow.search] "ran out of max depth" + return false let lctx ← getLCtx let r ← lctx.anyM fun localDecl => if localDecl.isAuxDecl then @@ -244,11 +245,12 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do commitWhen do let (mvars, _, t) ← forallMetaTelescope localDecl.type if (← isDefEq mTy t) then - trace[Meta.IndPredBelow.search] "searching for {mTy}: trying {mkFVar localDecl.fvarId} : {localDecl.type}" - m.assign (mkAppN localDecl.toExpr mvars) - mvars.allM fun v => - v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1) - else return false + withTraceNodeBefore `Meta.IndPredBelow.search (do pure m!"trying {mkFVar localDecl.fvarId} : {localDecl.type}") do + m.assign (mkAppN localDecl.toExpr mvars) + mvars.allM fun v => + v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1) + else + return false unless r do trace[Meta.IndPredBelow.search] "searching for {mTy} failed" return r @@ -302,9 +304,6 @@ where args.back.withApp fun ctor _ => do let ctorName := ctor.constName!.updatePrefix below.constName! let ctor := mkConst ctorName below.constLevels! - let ctorInfo ← getConstInfoCtor ctorName - let (mvars, _, _) ← forallMetaTelescope ctorInfo.type - let ctor := mkAppN ctor mvars m.apply ctor return mss.foldr List.append [] diff --git a/tests/lean/run/1672.lean b/tests/lean/run/1672.lean new file mode 100644 index 000000000000..654c74c4bd52 --- /dev/null +++ b/tests/lean/run/1672.lean @@ -0,0 +1,8 @@ +set_option trace.Meta.IndPredBelow true in +inductive TransClosure (r : α → α → Prop) : α → α → Prop + | extends : r a b → TransClosure r a b + | trans_left : r a b → TransClosure r b c → TransClosure r a c + +def trans' {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c +| .extends h₁ => .trans_left h₁ +| .trans_left h₁ h₂ => .trans_left h₁ ∘ trans' h₂ From 9264505b02e3ce70dc2f4033c9e63d5caa99f100 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 26 Jul 2024 11:35:15 +0200 Subject: [PATCH 2/4] Add termination_by --- tests/lean/run/1672.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/1672.lean b/tests/lean/run/1672.lean index 654c74c4bd52..b76aafa7f73d 100644 --- a/tests/lean/run/1672.lean +++ b/tests/lean/run/1672.lean @@ -1,4 +1,3 @@ -set_option trace.Meta.IndPredBelow true in inductive TransClosure (r : α → α → Prop) : α → α → Prop | extends : r a b → TransClosure r a b | trans_left : r a b → TransClosure r b c → TransClosure r a c @@ -6,3 +5,4 @@ inductive TransClosure (r : α → α → Prop) : α → α → Prop def trans' {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c | .extends h₁ => .trans_left h₁ | .trans_left h₁ h₂ => .trans_left h₁ ∘ trans' h₂ +termination_by structural t => t From 1224f0cadcc01d9bd365e3576d935e4ad4ff890c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 26 Jul 2024 12:20:21 +0200 Subject: [PATCH 3/4] More termination_by --- tests/lean/run/1674.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/lean/run/1674.lean b/tests/lean/run/1674.lean index 617825978f60..cca5d267f72d 100644 --- a/tests/lean/run/1674.lean +++ b/tests/lean/run/1674.lean @@ -5,3 +5,4 @@ inductive T : Prop where def inc: T → T | T.nil n => T.nil (n+1) | T.fn f => T.fn fun n => inc (f n) +termination_by structural t => t From e725ab92e2311d64d5b0387a5ecfd4e600636573 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 28 Jul 2024 20:26:33 -0300 Subject: [PATCH 4/4] Try reverse, mostly trial and error --- src/Lean/Meta/IndPredBelow.lean | 11 ++++++++--- tests/lean/run/4751.lean | 2 +- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index f67041e71e3d..11ac21bb76cf 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -305,7 +305,10 @@ where args.back.withApp fun ctor _ => do let ctorName := ctor.constName!.updatePrefix below.constName! let ctor := mkConst ctorName below.constLevels! - m.apply ctor + let ms ← m.apply ctor + trace[Meta.IndPredBelow] "new goals {ms}" + pure ms.reverse + return mss.foldr List.append [] introNPRec (m : MVarId) : MetaM MVarId := do @@ -321,12 +324,14 @@ where def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do let type ← mkType let indVal := ctx.typeInfos[idx]! - let name := indVal.name ++ .mkSimple brecOnSuffix + let name := mkBRecOnName indVal.name + let value ← proveBrecOn ctx indVal type + trace[Meta.IndPredBelow] "brecOn value: {value}" return Declaration.thmDecl { name := name levelParams := indVal.levelParams type := type - value := ←proveBrecOn ctx indVal type } + value := value} where mkType : MetaM Expr := forallTelescopeReducing ctx.headers[idx]! fun xs _ => do diff --git a/tests/lean/run/4751.lean b/tests/lean/run/4751.lean index 92f360af5aff..88191e005d05 100644 --- a/tests/lean/run/4751.lean +++ b/tests/lean/run/4751.lean @@ -1,4 +1,4 @@ -inductive F: Prop where +inductive F : Prop where | base | step (fn: Nat → F)