From 4f7067fe7fe1c71622bc7fbc044360d4f3366052 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Feb 2022 08:07:23 -0800 Subject: [PATCH] fix: `substEqs` may close input goal closes #1029 --- src/Lean/Meta/Injective.lean | 4 ++-- src/Lean/Meta/Tactic/Cases.lean | 4 ++-- tests/lean/run/1029.lean | 2 ++ 3 files changed, 6 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/1029.lean diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index 6b0a997dff..a0ba276eb9 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -127,8 +127,8 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me let (_, mvarId₂) ← intro1 mvarId₂ solveEqOfCtorEq ctorName mvarId₁ h let mvarId₂ ← casesAnd mvarId₂ - let mvarId₂ ← substEqs mvarId₂ - applyRefl mvarId₂ (injTheoremFailureHeader ctorName) + if let some mvarId₂ ← substEqs mvarId₂ then + applyRefl mvarId₂ (injTheoremFailureHeader ctorName) mkLambdaFVars xs mvar private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index 8afc43bb9c..968bac7522 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -340,11 +340,11 @@ def casesAnd (mvarId : MVarId) : MetaM MVarId := do let mvarIds ← casesRec mvarId fun localDecl => return (← instantiateMVars localDecl.type).isAppOfArity ``And 2 exactlyOne mvarIds -def substEqs (mvarId : MVarId) : MetaM MVarId := do +def substEqs (mvarId : MVarId) : MetaM (Option MVarId) := do let mvarIds ← casesRec mvarId fun localDecl => do let type ← instantiateMVars localDecl.type return type.isEq || type.isHEq - exactlyOne mvarIds + ensureAtMostOne mvarIds structure ByCasesSubgoal where mvarId : MVarId diff --git a/tests/lean/run/1029.lean b/tests/lean/run/1029.lean new file mode 100644 index 0000000000..0b3a6245a9 --- /dev/null +++ b/tests/lean/run/1029.lean @@ -0,0 +1,2 @@ +inductive Foo : Type + | mk : 0 = 1 → Foo → Foo