feat: contradiction catches empty inductive types

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

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 : <empty-inductive-type>)
+        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

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
 

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