From 2fd0b8c663d2c8879213665bbf712cc98d3a85fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Mar 2021 21:48:43 -0700 Subject: [PATCH] feat: `contradiction` catches empty inductive types --- src/Lean/Meta/Tactic/Cases.lean | 2 +- src/Lean/Meta/Tactic/Contradiction.lean | 41 ++++++++++++++++++++----- src/Lean/Meta/Tactic/Subst.lean | 12 ++++---- tests/lean/run/contradiction1.lean | 25 +++++++++++++++ 4 files changed, 66 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/contradiction1.lean diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index b3d9c0ca56..78b6b0a243 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -281,7 +281,7 @@ private def inductionCasesOn (mvarId : MVarId) (majorFVarId : FVarId) (givenName let casesOn := mkCasesOnName ctx.inductiveVal.name let ctors := ctx.inductiveVal.ctors.toArray let s ← induction mvarId majorFVarId casesOn givenNames - pure $ toCasesSubgoals s ctors majorFVarId us params + return toCasesSubgoals s ctors majorFVarId us params def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) := withMVarContext mvarId do diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index d0243951b4..eb6c9f2e52 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -3,12 +3,40 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Lean.Meta.Tactic.Assumption import Lean.Meta.MatchUtil +import Lean.Meta.Tactic.Assumption +import Lean.Meta.Tactic.Cases namespace Lean.Meta -def contradictionCore (mvarId : MVarId) (useDecide : Bool) : MetaM Bool := do +def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (searchDepth : Nat) : MetaM Bool := + match searchDepth with + | 0 => return false + | searchDepth + 1 => + withMVarContext mvarId do + let localDecl ← getLocalDecl fvarId + let type ← whnfD localDecl.type + matchConstInduct type.getAppFn (fun _ => pure false) fun info _ => do + if info.ctors.length == 0 || info.numIndices > 0 then + -- We only consider inductives with no constructors and indexed families + commitWhen do + let subgoals ← try cases mvarId fvarId catch _ => return false + for subgoal in subgoals do + -- If one of the fields is uninhabited, then we are done + let mut found := false + for field in subgoal.fields do + let field := subgoal.subst.apply field + if field.isFVar then + if (← elimEmptyInductive subgoal.mvarId field.fvarId! searchDepth) then + found := true + break + unless found == true do -- TODO: check why we need true here + return false + return true + else + return false + +def contradictionCore (mvarId : MVarId) (useDecide : Bool) (searchDepth : Nat) : MetaM Bool := do withMVarContext mvarId do checkNotAssigned mvarId `contradiction for localDecl in (← getLCtx) do @@ -18,9 +46,8 @@ def contradictionCore (mvarId : MVarId) (useDecide : Bool) : MetaM Bool := do if let some pFVarId ← findLocalDeclWithType? p then assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) (mkFVar pFVarId) localDecl.toExpr) return true - -- (h : False) - if (← matchFalse localDecl.type) then - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) localDecl.toExpr) + -- (h : ) + if (← elimEmptyInductive mvarId localDecl.fvarId searchDepth) then return true -- (h : x ≠ x) if let some (_, lhs, rhs) ← matchNe? localDecl.type then @@ -47,8 +74,8 @@ def contradictionCore (mvarId : MVarId) (useDecide : Bool) : MetaM Bool := do pure () return false -def contradiction (mvarId : MVarId ) (useDecide : Bool := true) : MetaM Unit := - unless (← contradictionCore mvarId useDecide) do +def contradiction (mvarId : MVarId ) (useDecide : Bool := true) (searchDepth : Nat := 2): MetaM Unit := + unless (← contradictionCore mvarId useDecide searchDepth) do throwTacticEx `contradiction mvarId "" end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index a371ac3898..1ea91d40aa 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -14,7 +14,7 @@ import Lean.Meta.Tactic.FVarSubst namespace Lean.Meta -def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) (clearH := true) : MetaM (FVarSubst × MVarId) := +def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) (clearH := true) (tryToSkip := false) : MetaM (FVarSubst × MVarId) := withMVarContext mvarId do let tag ← getMVarTag mvarId checkNotAssigned mvarId `subst @@ -44,7 +44,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let h := mkFVar hFVarId /- Set skip to true if there is no local variable nor the target depend on the equality -/ let skip ← - if vars.size != 2 then + if !tryToSkip || vars.size != 2 then pure false else let mvarType ← getMVarType mvarId @@ -128,20 +128,20 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := let mvarId ← assert mvarId hLocalDecl.userName newType (mkFVar hFVarId) let (hFVarId', mvarId) ← intro1P mvarId let mvarId ← clear mvarId hFVarId - return (← substCore mvarId hFVarId' symm).2 + return (← substCore mvarId hFVarId' (symm := symm) (tryToSkip := true)).2 let rhs' ← whnf rhs if rhs'.isFVar then if rhs != rhs' then substReduced (← mkEq lhs rhs') true else - return (← substCore mvarId hFVarId true).2 + return (← substCore mvarId hFVarId (symm := true) (tryToSkip := true)).2 else do let lhs' ← whnf lhs if lhs'.isFVar then if lhs != lhs' then substReduced (← mkEq lhs' rhs) false else - return (← substCore mvarId hFVarId).2 + return (← substCore mvarId hFVarId (symm := false) (tryToSkip := true)).2 else do throwTacticEx `subst mvarId m!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr hLocalDecl.type}" | none => @@ -163,7 +163,7 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := return none | _ => return none | throwTacticEx `subst mvarId m!"did not find equation for eliminating '{mkFVar hFVarId}'" - return (← substCore mvarId fvarId symm).2 + return (← substCore mvarId fvarId (symm := symm) (tryToSkip := true)).2 builtin_initialize registerTraceClass `Meta.Tactic.subst diff --git a/tests/lean/run/contradiction1.lean b/tests/lean/run/contradiction1.lean new file mode 100644 index 0000000000..46ec227dbd --- /dev/null +++ b/tests/lean/run/contradiction1.lean @@ -0,0 +1,25 @@ +inductive MyFin : Nat → Type + | z : MyFin (n+1) + | s : MyFin n → MyFin (n+1) + +theorem ex1 (x : MyFin 0) : False := by + contradiction + +inductive Color +| Red +| Black +open Color + +inductive rbnode : Nat → Color → Type where + | Leaf : rbnode 1 Black + | R {h} + (left : rbnode h Black) + (value : Int) + (right : rbnode h Black) : rbnode h Red + | B {h cl cr} + (left : rbnode h cl) + (value : Int) + (right : rbnode h cr) : rbnode (h+1) Black + +theorem ex2 (x : rbnode 0 Color.Red) : False := by + contradiction