From bffefa61bdcc3ec382ead32057ad91e893841245 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Aug 2021 12:52:50 -0700
Subject: [PATCH] feat: extend `contradiction` for `MatchEqs.lean`

---
 src/Lean/Meta/Match/MatchEqs.lean       |  4 +--
 src/Lean/Meta/Tactic/Contradiction.lean | 41 ++++++++++++++++++++++++-
 2 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index d79b3abca9..5bb6d307fb 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -120,10 +120,10 @@ where
 
   proveLoop (mvarId : MVarId) (depth : Nat) : MetaM Unit := withIncRecDepth do
     let mvarId ← modifyTargetEqLHS mvarId whnfCore
-    trace[Meta.debug] "proveLoop\n{MessageData.ofGoal mvarId}"
+    trace[Meta.debug] "proveLoop [{depth}]\n{MessageData.ofGoal mvarId}"
     (applyRefl mvarId)
     <|>
-    (contradiction mvarId)
+    (contradiction mvarId { genDiseq := true })
     <|>
     (do (← casesOnStuckLHS mvarId).forM (proveLoop . (depth + 1)))
     <|>
diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index f7bc34f5e8..5b273aac6d 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -12,8 +12,14 @@ namespace Lean.Meta
 structure Contradiction.Config where
   useDecide : Bool  := true
   searchDepth : Nat := 2
+  /- Support for hypotheses such as
+     ```
+     h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
+     ```
+     This kind of hypotheses appear when proving conditional equation theorems for match expressions. -/
+  genDiseq : Bool := false
 
-def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (searchDepth : Nat) : MetaM Bool :=
+private def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (searchDepth : Nat) : MetaM Bool :=
   match searchDepth with
   | 0 => return false
   | searchDepth + 1 =>
@@ -40,6 +46,35 @@ def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (searchDepth : Nat) :
         else
           return false
 
+/-- Return true if `e` is of the form `(x : α) → ... → s = t → ... → False` -/
+private def isGenDiseq (e : Expr) : Bool :=
+  match e with
+  | Expr.forallE _ d b _ => (d.isEq || b.hasLooseBVar 0) && isGenDiseq b
+  | _ => e.isConstOf ``False
+
+/--
+  Close goal if `localDecl` is a "generalized disequality". Example:
+  ```
+  h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
+  ```
+  This kind of hypotheses is created when we generate conditional equations for match expressions.
+-/
+private def processGenDiseq (mvarId : MVarId) (localDecl : LocalDecl) : MetaM Bool :=
+  assert! isGenDiseq localDecl.type
+  withNewMCtxDepth do
+    let (args, _, _) ← forallMetaTelescope localDecl.type
+    for arg in args do
+      let argType ← inferType arg
+      if let some (_, lhs, rhs) ← matchEq? argType then
+        unless (← isDefEq lhs rhs) do
+          return false
+        assignExprMVar arg.mvarId! (← mkEqRefl lhs)
+    let falseProof ← instantiateMVars (mkAppN localDecl.toExpr args)
+    if (← hasAssignableMVar falseProof) then
+      return false
+    assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) falseProof)
+    return true
+
 def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM Bool := do
   withMVarContext mvarId do
     checkNotAssigned mvarId `contradiction
@@ -77,6 +112,10 @@ def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM
                 return true
             catch _ =>
               pure ()
+        -- "generalized" diseq
+        if config.genDiseq && isGenDiseq localDecl.type then
+          if (← processGenDiseq mvarId localDecl) then
+            return true
         -- (h : <empty-inductive-type>)
         unless isEq do
           -- We do not use `elimEmptyInductive` for equality, since `cases h` produces a huge proof