From 52ff8403210b6d6f5eec5ccfd3c03149c7ac7a4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Feb 2022 17:23:47 -0800
Subject: [PATCH] feat: support for `HEq` at `injection`

---
 src/Lean/Meta/Tactic/Injection.lean | 67 ++++++++++++++++-------------
 tests/lean/run/injHEq.lean          |  2 +
 2 files changed, 40 insertions(+), 29 deletions(-)
 create mode 100644 tests/lean/run/injHEq.lean

diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index b6310ba5c0..4ff2a5901b 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -28,35 +28,44 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
     checkNotAssigned mvarId `injection
     let decl ← getLocalDecl fvarId
     let type ← whnf decl.type
-    match type.eq? with
-    | none           => throwTacticEx `injection mvarId "equality expected"
-    | some (α, a, b) =>
-      let a ← whnf a
-      let b ← whnf b
-      let target ← getMVarType mvarId
-      let env ← getEnv
-      match a.isConstructorApp? env, b.isConstructorApp? env with
-      | some aCtor, some bCtor =>
-        let val ← mkNoConfusion target (mkFVar fvarId)
-        if aCtor.name != bCtor.name then
-          assignExprMVar mvarId val
-          pure InjectionResultCore.solved
-        else
-          let valType ← inferType val
-          let valType ← whnf valType
-          match valType with
-          | Expr.forallE _ newTarget _ _ =>
-            let newTarget := newTarget.headBeta
-            let tag ← getMVarTag mvarId
-            let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
-            assignExprMVar mvarId (mkApp val newMVar)
-            let mvarId ← tryClear newMVar.mvarId! fvarId
-            /- Recall that `noConfusion` does not include equalities for
-               propositions since they are trivial due to proof irrelevance. -/
-            let numPropFields ← getCtorNumPropFields aCtor
-            return InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields)
-          | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
-      | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"
+    let go (type prf : Expr) : MetaM InjectionResultCore := do
+      match type.eq? with
+      | none           => throwTacticEx `injection mvarId "equality expected"
+      | some (α, a, b) =>
+        let a ← whnf a
+        let b ← whnf b
+        let target ← getMVarType mvarId
+        let env ← getEnv
+        match a.isConstructorApp? env, b.isConstructorApp? env with
+        | some aCtor, some bCtor =>
+          let val ← mkNoConfusion target prf
+          if aCtor.name != bCtor.name then
+            assignExprMVar mvarId val
+            return InjectionResultCore.solved
+          else
+            let valType ← inferType val
+            let valType ← whnf valType
+            match valType with
+            | Expr.forallE _ newTarget _ _ =>
+              let newTarget := newTarget.headBeta
+              let tag ← getMVarTag mvarId
+              let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
+              assignExprMVar mvarId (mkApp val newMVar)
+              let mvarId ← tryClear newMVar.mvarId! fvarId
+              /- Recall that `noConfusion` does not include equalities for
+                 propositions since they are trivial due to proof irrelevance. -/
+              let numPropFields ← getCtorNumPropFields aCtor
+              return InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields)
+            | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
+        | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"
+    let prf := mkFVar fvarId
+    if let some (α, a, β, b) := type.heq? then
+      if (← isDefEq α β) then
+        go (← mkEq a b) (← mkEqOfHEq prf)
+      else
+        go type prf
+    else
+      go type prf
 
 inductive InjectionResult where
   | solved
diff --git a/tests/lean/run/injHEq.lean b/tests/lean/run/injHEq.lean
new file mode 100644
index 0000000000..4bd6bfb20e
--- /dev/null
+++ b/tests/lean/run/injHEq.lean
@@ -0,0 +1,2 @@
+example (h : HEq Nat.zero (Nat.succ Nat.zero)) : False := by
+  injection h