feat: heterogeneous contructor injectivity in grind (#11491)

This PR implements heterogeneous contructor injectivity in `grind`.

Example:
```lean
opaque double : Nat → Nat

inductive Parity : Nat -> Type
  | even (n) : Parity (double n)
  | odd  (n) : Parity (Nat.succ (double n))

opaque q : Nat → Nat → Prop
axiom qax : q a b → double a = double b
attribute [grind →] qax

example
  (motive : (x : Nat) → Parity x → Sort u_1)
  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
  (j n : Nat)
  (heq_1 : q j n) -- Implies that `double j = double n`
  (heq_2 : Parity.even n ≍ Parity.even j):
  h_2 n ≍ h_2 j := by
grind
```

Closes #11449

Author: leodemoura

src/Lean/Meta/Injective.lean

@@ -40,7 +40,7 @@ private def mkEqs (args1 args2 : Array Expr) (skipIfPropOrEq : Bool := true) : M
       eqs := eqs.push (← mkEqHEq arg1 arg2)
   return eqs
 
-private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
+private def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam
   let type ← elimOptParam ctorVal.type
   forallBoundedTelescope type ctorVal.numParams fun params type =>
@@ -181,7 +181,7 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
 builtin_initialize
   registerTraceClass `Meta.injective
 
-private def getIndices? (ctorApp : Expr) : MetaM (Option (Array Expr)) := do
+def getCtorAppIndices? (ctorApp : Expr) : MetaM (Option (Array Expr)) := do
   let type ← whnfD (← inferType ctorApp)
   type.withApp fun typeFn typeArgs => do
     let .const declName _ := typeFn | return none
@@ -197,20 +197,20 @@ private structure MkHInjTypeResult where
   us : List Level
   numIndices : Nat
 
-private partial def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeResult) := do
+private def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeResult) := do
   let us := ctorVal.levelParams.map mkLevelParam
   let type ← elimOptParam ctorVal.type
   forallBoundedTelescope type ctorVal.numParams fun params type =>
-  forallTelescope type fun args1 resultType => do
+  forallTelescope type fun args1 _ => do
     let k (args2 : Array Expr) : MetaM (Option MkHInjTypeResult) := do
       let lhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args1
       let rhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args2
       let eq ← mkEqHEq lhs rhs
       let eqs ← mkEqs args1 args2
       if let some andEqs := mkAnd? eqs then
         let result ← mkArrow eq andEqs
-        let some idxs1 ← getIndices? lhs | return none
-        let some idxs2 ← getIndices? rhs | return none
+        let some idxs1 ← getCtorAppIndices? lhs | return none
+        let some idxs2 ← getCtorAppIndices? rhs | return none
         -- **Note**: We dot not skip here because the type of `noConfusion` does not.
         let idxEqs ← mkEqs idxs1 idxs2 (skipIfPropOrEq := false)
         let result ← mkArrows idxEqs result
@@ -254,7 +254,6 @@ private partial def mkHInjectiveTheoremValue? (ctorVal : ConstructorVal) (typeIn
     let mvarId := mvar.mvarId!
     let (_, mvarId) ← mvarId.intros
     splitAndAssumption mvarId ctorVal.name
-    check noConfusion
     let result ← instantiateMVars noConfusion
     mkLambdaFVars xs result
 

src/Lean/Meta/Tactic/Grind/Ctor.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Injective
 import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind
@@ -33,20 +34,13 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) (generation : Na
    reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
-/--
-Given constructors `a` and `b`, propagate equalities if they are the same,
-and close goal if they are different.
--/
-def propagateCtor (a b : Expr) : GoalM Unit := do
-  let aType ← whnfD (← inferType a)
-  let bType ← whnfD (← inferType b)
-  unless (← isDefEqD aType bType) do
-    return ()
+/-- Homogeneous case where constructor applications `a` and `b` have the same type `α`. -/
+private def propagateCtorHomo (α : Expr) (a b : Expr) : GoalM Unit := do
   let ctor₁ := a.getAppFn
   let ctor₂ := b.getAppFn
   if ctor₁ == ctor₂ then
-    let .const ctorName _ := a.getAppFn | return ()
-    let injDeclName := Name.mkStr ctorName "inj"
+    let .const ctorName _ := ctor₁ | return ()
+    let injDeclName := mkInjectiveTheoremNameFor ctorName
     unless (← getEnv).contains injDeclName do return ()
     let info ← getConstInfo injDeclName
     let n := info.type.getForallArity
@@ -62,9 +56,57 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
     let gen := max (← getGeneration a) (← getGeneration b)
     propagateInjEqs injLemmaType injLemma gen
   else
-    let .const declName _ := aType.getAppFn | return ()
+    let .const declName _ := α.getAppFn | return ()
     let noConfusionDeclName := Name.mkStr declName "noConfusion"
     unless (← getEnv).contains noConfusionDeclName do return ()
     closeGoal (← mkNoConfusion (← getFalseExpr) (← mkEqProof a b))
 
+/-- Heterogeneous case where constructor applications `a` and `b` have different types `α` and `β`. -/
+private def propagateCtorHetero (a b : Expr) : GoalM Unit := do
+  a.withApp fun ctor₁ args₁ =>
+  b.withApp fun ctor₂ args₂ => do
+  let .const ctorName₁ us₁ := ctor₁ | return ()
+  let .const ctorName₂ us₂ := ctor₂ | return ()
+  let .ctorInfo ctorVal₁ ← getConstInfo ctorName₁ | return ()
+  let .ctorInfo ctorVal₂ ← getConstInfo ctorName₂ | return ()
+  unless ctorVal₁.induct == ctorVal₂.induct do return ()
+  let params₁ := args₁[*...ctorVal₁.numParams]
+  let params₂ := args₂[*...ctorVal₂.numParams]
+  let fields₁ := args₁[ctorVal₁.numParams...*]
+  let fields₂ := args₂[ctorVal₂.numParams...*]
+  if h : params₁.size ≠ params₂.size then return () else
+  unless (← params₁.size.allM fun i h => isDefEq params₁[i] params₂[i]) do return ()
+  unless us₁.length == us₂.length do return ()
+  unless (← us₁.zip us₂ |>.allM fun (u₁, u₂) => isLevelDefEq u₁ u₂) do return ()
+  let gen := max (← getGeneration a) (← getGeneration b)
+  if ctorName₁ == ctorName₂ then
+    let hinjDeclName := mkHInjectiveTheoremNameFor ctorName₁
+    unless (← getEnv).containsOnBranch hinjDeclName do
+      let _ ← executeReservedNameAction hinjDeclName
+    let proof := mkAppN (mkConst hinjDeclName us₁) params₁
+    let proof := mkAppN (mkAppN proof fields₁) fields₂
+    addNewRawFact proof (← inferType proof) gen (.inj (.decl hinjDeclName))
+  else
+    let some indices₁ ← getCtorAppIndices? a | return ()
+    let some indices₂ ← getCtorAppIndices? b | return ()
+    let noConfusionName := ctorVal₁.induct.str "noConfusion"
+    let noConfusion := mkAppN (mkConst noConfusionName (0 :: us₁)) params₁
+    let noConfusion := mkApp noConfusion (← getFalseExpr)
+    let noConfusion := mkApp (mkAppN noConfusion indices₁) a
+    let noConfusion := mkApp (mkAppN noConfusion indices₂) b
+    let proof := noConfusion
+    addNewRawFact proof (← inferType proof) gen (.inj (.decl noConfusionName))
+
+/--
+Given constructors `a` and `b`, propagate equalities if they are the same,
+and close goal if they are different.
+-/
+def propagateCtor (a b : Expr) : GoalM Unit := do
+  let aType ← whnfD (← inferType a)
+  let bType ← whnfD (← inferType b)
+  if (← isDefEqD aType bType) then
+    propagateCtorHomo aType a b
+  else
+    propagateCtorHetero a b
+
 end Lean.Meta.Grind

tests/lean/run/grind_11449.lean

@@ -0,0 +1,52 @@
+opaque double : Nat → Nat
+def P (n : Nat) : Prop := n >= 0
+theorem pax (n : Nat) : P n := by grind [P]
+def T (n : Nat) : Type := Vector Nat n
+
+inductive Foo' (α β : Type u) : (n : Nat) → P n -> Type u
+  | even (a : α) (n : Nat) (v : T n) (h : P n) : Foo' α β (double n) (pax _)
+  | odd  (b : β) (n : Nat) (v : T n) : Foo' α β (Nat.succ (double n)) (pax _)
+
+example (α β : Type) (a₁ a₂ : α)
+    (n₁ n₂ : Nat)
+    (v₁ : T n₁) (v₂ : T n₂)
+    (h₁ : P n₁) (h₂ : P n₂)
+    (h_1 : double n₁ = double n₂)
+    (h_2 : Foo'.even (β := β) a₁ n₁ v₁ h₁ ≍ Foo'.even (β := β) a₂ n₂ v₂ h₂) :
+    a₁ = a₂ ∧ n₁ = n₂ ∧ v₁ ≍ v₂ ∧ h₁ ≍ h₂ := by
+  grind
+
+example (α β : Type) (a : α) (b : β)
+    (n₁ n₂ : Nat)
+    (v₁ : T n₁) (v₂ : T n₂)
+    (h₁ : P n₁)
+    (h_1 : double n₁ = (double n₂).succ)
+    (h_2 : Foo'.even (β := β) a n₁ v₁ h₁ ≍ Foo'.odd (α := α) b n₂ v₂)
+    : False := by
+  grind
+
+inductive Parity : Nat -> Type
+  | even (n) : Parity (double n)
+  | odd  (n) : Parity (Nat.succ (double n))
+
+example
+  (motive : (x : Nat) → Parity x → Sort u_1)
+  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
+  (j n : Nat)
+  (heq_1 : double n = double j)
+  (heq_2 : Parity.even n ≍ Parity.even j):
+  h_2 n ≍ h_2 j := by
+grind
+
+opaque q : Nat → Nat → Prop
+axiom qax : q a b → double a = double b
+attribute [grind →] qax
+
+example
+  (motive : (x : Nat) → Parity x → Sort u_1)
+  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
+  (j n : Nat)
+  (heq_1 : q j n)
+  (heq_2 : Parity.even n ≍ Parity.even j):
+  h_2 n ≍ h_2 j := by
+grind

tests/lean/run/issue11449.lean

@@ -11,10 +11,7 @@ example
   (heq_1 : double n = double j)
   (heq_2 : Parity.even n ≍ Parity.even j):
   h_2 n ≍ h_2 j := by
-  fail_if_success grind -- does not work yet
-  sorry
-
--- manual proof using heterogenenous noConfusion
+  grind
 
 example
   (motive : (x : Nat) → Parity x → Sort u_1)