From a5b9306e04146169efc70d17df390a3bfd197ff2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Aug 2021 20:35:34 -0700 Subject: [PATCH] fix: deep recursion at `contradiction` --- src/Lean/Meta/Tactic/Contradiction.lean | 11 ++++++++--- tests/lean/run/contradictionLoop.lean | 4 ++++ 2 files changed, 12 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/contradictionLoop.lean diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index 0d9729f986..52bbe7fce8 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -46,16 +46,15 @@ def contradictionCore (mvarId : MVarId) (useDecide : Bool) (searchDepth : Nat) : if let some pFVarId ← findLocalDeclWithType? p then assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) (mkFVar pFVarId) localDecl.toExpr) return true - -- (h : ) - if (← elimEmptyInductive mvarId localDecl.fvarId searchDepth) then - return true -- (h : x ≠ x) if let some (_, lhs, rhs) ← matchNe? localDecl.type then if (← isDefEq lhs rhs) then assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) (← mkEqRefl lhs) localDecl.toExpr) return true + let mut isEq := false -- (h : ctor₁ ... = ctor₂ ...) if let some (_, lhs, rhs) ← matchEq? localDecl.type then + isEq := true if let some lhsCtor ← matchConstructorApp? lhs then if let some rhsCtor ← matchConstructorApp? rhs then if lhsCtor.name != rhsCtor.name then @@ -72,6 +71,12 @@ def contradictionCore (mvarId : MVarId) (useDecide : Bool) (searchDepth : Nat) : return true catch _ => pure () + -- (h : ) + unless isEq do + -- We do not use `elimEmptyInductive` for equality, since `cases h` produces a huge proof + -- when `(h : 10000 = 10001)`. TODO: `cases` add a threshold at `cases` + if (← elimEmptyInductive mvarId localDecl.fvarId searchDepth) then + return true return false def contradiction (mvarId : MVarId) (useDecide : Bool := true) (searchDepth : Nat := 2) : MetaM Unit := diff --git a/tests/lean/run/contradictionLoop.lean b/tests/lean/run/contradictionLoop.lean new file mode 100644 index 0000000000..0810819056 --- /dev/null +++ b/tests/lean/run/contradictionLoop.lean @@ -0,0 +1,4 @@ +theorem ex (h : 10000 = 100001) : False := by + contradiction + +#print ex