feat: make noConfusion even more heterogeneous

This PR makes the noConfusion principles even more heterogeneous, by
allowing not just indices but also parameters to be differ.

This is a breaking change for manual use of `noConfusion` for types with
parameters. Pass suitable `rfl` arguments, and use `eq_of_heq` on the
resulting equalities as needed.

This fixes #11560.

Author: nomeata

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -33,25 +33,27 @@ constructor. In particular, returns
 ```
 fun params x1 x2 x3 x1' x2' x3' => (x1 = x1' → x2 = x2' → x3 = x3' → P)
 ```
-where `x1 x2 x3` and `x1' x2' x3'` are the fields of a constructor application of `ctorName`,
-omitting equalities between propositions and using `HEq` where needed.
+where `x1 x2 x3` and `x1' x2' x3'` are the parameters and  fields of a constructor application of
+`ctorName`, omitting equalities between propositions and using `HEq` where needed.
 -/
 def mkNoConfusionCtorArg (ctorName : Name) (P : Expr) : MetaM Expr := do
   let ctorInfo ← getConstInfoCtor ctorName
   -- We bring the constructor's parameters into scope abstractly, this way
   -- we can check if we need to use HEq. (The concrete fields could allow Eq)
-  forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs t => do
-    forallTelescopeReducing t fun fields1 _ => do
-    forallTelescopeReducing t fun fields2 _ => do
-    withPrimedNames fields2 do
+  forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs1 t1 => do
+  forallTelescopeReducing t1 fun fields1 _ => do
+  forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs2 t2 => do
+  withPrimedNames xs2 do
+  forallTelescopeReducing t2 fun fields2 _ => do
+  withPrimedNames fields2 do
     let mut t := P
     for f1 in fields1.reverse, f2 in fields2.reverse do
       if (← isProof f1) then
         continue
       let name := (← f1.fvarId!.getUserName).appendAfter "_eq"
       let eq ← mkEqHEq f1 f2
       t := mkForall name .default eq t
-    mkLambdaFVars (xs ++ fields1 ++ fields2) t
+    mkLambdaFVars (xs1 ++ fields1 ++ xs2 ++ fields2) t
 
 register_builtin_option backward.linearNoConfusionType : Bool := {
   defValue := true
@@ -89,54 +91,57 @@ def mkNoConfusionType (indName : Name) : MetaM Unit := do
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   let e := mkConst casesOnName (v.succ::us)
   let t ← inferType e
-  let e ← forallBoundedTelescope t info.numParams fun xs t => do
-    let e := mkAppN e xs
-    let PType := mkSort v
-    withLocalDeclD `P PType fun P => do
-      let motive ← forallTelescope (← whnfD t).bindingDomain! fun ys _ =>
-        mkLambdaFVars ys PType
-      let ti ← instantiateForall t #[motive]
-      let e := mkApp e motive
-      forallBoundedTelescope ti (some (info.numIndices + 1)) fun ysx1 t => do -- indices and major
-      forallBoundedTelescope ti (some (info.numIndices + 1)) fun ysx2 _ => do -- indices and major
+  let PType := mkSort v
+  let e ← withLocalDeclD `P PType fun P => do
+    forallBoundedTelescope t info.numParams fun xs1 t1 => do
+    forallBoundedTelescope t info.numParams fun xs2 t2 => do
+    withPrimedNames xs2 do
+      let e := mkAppN e xs1
+      let motive1 ← forallTelescope (← whnfD t1).bindingDomain! fun ys _ => mkLambdaFVars ys PType
+      let t1 ← instantiateForall t1 #[motive1]
+      let e := mkApp e motive1
+      let motive2 ← forallTelescope (← whnfD t2).bindingDomain! fun ys _ => mkLambdaFVars ys PType
+      let t2 ← instantiateForall t2 #[motive2]
+      forallBoundedTelescope t1 (some (info.numIndices + 1)) fun ysx1 t1 => do -- indices and major
+      forallBoundedTelescope t2 (some (info.numIndices + 1)) fun ysx2 _t2 => do -- indices and major
       withPrimedNames ysx2 do
         let e := mkAppN e ysx1
-        let altTypes ← arrowDomainsN info.numCtors t
+        let altTypes ← arrowDomainsN info.numCtors t1
         let alts ← altTypes.mapIdxM fun i altType => do
           forallTelescope altType fun zs1 _ => do
             if useLinearConstruction then
-              let ctorIdxApp := mkAppN (mkConst (mkCtorIdxName indName) us) (xs ++ ysx2)
+              let ctorIdxApp := mkAppN (mkConst (mkCtorIdxName indName) us) (xs2 ++ ysx2)
               let alt ← mkIfNatEq PType (ctorIdxApp) (mkRawNatLit i)
                 («else» := fun _ => pure P) fun h => do
                 let conName := info.ctors[i]!
                 let withName := mkConstructorElimName indName conName
                 let e := mkConst withName (v.succ :: us)
-                let e := mkAppN e (xs ++ #[motive] ++ ysx2 ++ #[h])
+                let e := mkAppN e (xs2 ++ #[motive2] ++ ysx2 ++ #[h])
                 let e := mkApp e <|
                   ← forallTelescopeReducing ((← whnf (← inferType e)).bindingDomain!) fun zs2 _ => do
-                    let k := (← mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
+                    let k := (← mkNoConfusionCtorArg conName P).beta (xs1 ++ zs1 ++ xs2 ++ zs2)
                     let t ← mkArrow k P
                     mkLambdaFVars zs2 t
                 pure e
               mkLambdaFVars zs1 alt
             else
               let conName := info.ctors[i]!
               let alt := mkConst casesOnName (v.succ :: us)
-              let alt := mkAppN alt (xs ++ #[motive] ++ ysx2)
+              let alt := mkAppN alt (xs2 ++ #[motive2] ++ ysx2)
               let t2 ← inferType alt
               let altTypes2 ← arrowDomainsN info.numCtors t2
               let alts2 ← altTypes2.mapIdxM fun j altType2 => do
                 forallTelescope altType2 fun zs2 _ => do
                   if i = j then
-                    let k := (← mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
+                    let k := (← mkNoConfusionCtorArg conName P).beta (xs1 ++ zs1 ++ xs2 ++ zs2)
                     let t ← mkArrow k P
                     mkLambdaFVars zs2 t
                   else
                     mkLambdaFVars zs2 P
               let alt := mkAppN alt alts2
               mkLambdaFVars zs1 alt
         let e := mkAppN e alts
-        mkLambdaFVars (xs ++ #[P] ++ ysx1 ++ ysx2) e
+        mkLambdaFVars (#[P] ++ xs1 ++ ysx1 ++ xs2 ++ ysx2) e
 
   addDecl (.defnDecl (← mkDefinitionValInferringUnsafe
     (name        := declName)
@@ -220,19 +225,19 @@ def mkNoConfusionCoreImp (indName : Name) : MetaM Unit := do
   let casesOnInfo ← getConstVal casesOnName
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   trace[Meta.mkNoConfusion] m!"mkNoConfusionCoreImp for {declName}"
-  let e ← forallBoundedTelescope (← inferType (mkConst noConfusionTypeName (v::us))) (some (info.numParams + 1)) fun xs t => do
-    let params : Array Expr := xs[:info.numParams]
-    let P := xs[info.numParams]!
-    forallBoundedTelescope t (some (info.numIndices + 1)) fun ysx1 _ => do -- indices and major
-    forallBoundedTelescope t (some (info.numIndices + 1)) fun ysx2 _ => do -- indices and major
-    withPrimedNames ysx2 do
-      withImplicitBinderInfos ((ysx1 ++ ysx2).push P) do
-      let target1 := mkAppN (mkConst noConfusionTypeName (v :: us)) (params ++ #[P] ++ ysx1 ++ ysx1)
+  let e ← forallBoundedTelescope (← inferType (mkConst noConfusionTypeName (v::us))) (some 1) fun xs t => do
+    let P := xs[0]!
+    forallBoundedTelescope t (some (info.numParams + info.numIndices + 1)) fun xs1 t => do -- params, indices and major
+    forallBoundedTelescope t (some (info.numParams + info.numIndices + 1)) fun xs2 _ => do -- params, indices and major
+    withImplicitBinderInfos ((xs1 ++ xs2).push P) do
+      let params1 : Array Expr := xs1[:info.numParams]
+      let ysx1    : Array Expr := xs1[info.numParams:]
+      let target1 := mkAppN (mkConst noConfusionTypeName (v :: us)) (#[P] ++ xs1 ++ xs1)
       let motive1 ← mkLambdaFVars ysx1 target1
       let alts ← info.ctors.mapM fun ctor => do
-        let ctorType ← inferType (mkAppN (mkConst ctor us) params)
-        forallTelescopeReducing ctorType fun fs _ => do
-          let kType := (← mkNoConfusionCtorArg ctor P).beta (params ++ fs ++ fs)
+        let ctorType ← inferType (mkAppN (mkConst ctor us) params1)
+        forallTelescopeReducing ctorType fun fs1 _ => do
+          let kType := (← mkNoConfusionCtorArg ctor P).beta (params1 ++ fs1 ++ params1 ++ fs1)
           withLocalDeclD `k kType fun k => do
             let mut e := k
             let eqns ← arrowDomainsN kType.getNumHeadForalls kType
@@ -243,12 +248,12 @@ def mkNoConfusionCoreImp (indName : Name) : MetaM Unit := do
                 e := mkApp e (← mkHEqRefl x)
               else
                 throwError "unexpected equation {eqn} in `mkNoConfusionCtorArg` for {ctor}"
-            mkLambdaFVars (fs ++ #[k]) e
-      let e := mkAppN (mkConst casesOnName (v :: us)) (params ++ #[motive1] ++ ysx1 ++ alts)
-      let target2 := mkAppN (mkConst noConfusionTypeName (v :: us)) (params ++ #[P] ++ ysx1 ++ ysx2)
-      let motive2 ← mkLambdaFVars ysx2 target2
-      let e ← mkEqNDRecTelescope motive2 e ysx1 ysx2
-      mkLambdaFVars (params ++ #[P] ++ ysx1 ++ ysx2) e
+            mkLambdaFVars (fs1 ++ #[k]) e
+      let e := mkAppN (mkConst casesOnName (v :: us)) (params1 ++ #[motive1] ++ ysx1 ++ alts)
+      let target2 := mkAppN (mkConst noConfusionTypeName (v :: us)) (#[P] ++ xs1 ++ xs2)
+      let motive2 ← mkLambdaFVars xs2 target2
+      let e ← mkEqNDRecTelescope motive2 e xs1 xs2
+      mkLambdaFVars (#[P] ++ xs1 ++ xs2) e
 
   addDecl (.defnDecl (← mkDefinitionValInferringUnsafe
     (name        := declName)
@@ -265,8 +270,8 @@ def mkNoConfusionCoreImp (indName : Name) : MetaM Unit := do
 
 /--
 Creates per-constructor no-confusion definitions. These specialize the general noConfusion
-declaration to equalities between two applications of the same constructor, to effectively cache
-the computation of `noConfusionType` for that constructor:
+declaration to (homogeneous!) equalities between two applications of the same constructor, to
+effectively cache the computation of `noConfusionType` for that constructor:
 
 ```
 def L.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
@@ -282,6 +287,14 @@ def Vec.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
   (n = n' → x = x' → xs ≍ xs' → P)
   → P
 ```
+
+These are specialized to equal parameters. The main use of these theorems is `injection` through
+`Meta.mkNoConfusion`, which deals with homogeneous equalities, so no need for the generality.
+
+These still accept a heterogeneous equality between the two constructor applications: if we tried
+to phrase this theroem with a homogeneous equality, this would force those constructor fields that
+appear in indices to be equal, which is too strong: we can have homogenenous equalities between
+two constructor applications with different fields but same indices.
 -/
 def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
   -- Do not do anything unless can_elim_to_type.
@@ -312,11 +325,21 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
           -- When the kernel checks this definition, it will perform the potentially expensive
           -- computation that `noConfusionType h` is equal to `$kType → P`
           let kType ← mkNoConfusionCtorArg ctor P
-          let kType := kType.beta (xs ++ fields1 ++ fields2)
+          let kType := kType.beta (xs ++ fields1 ++ xs ++ fields2)
+          -- TODO: Turn HEq to Eq in kType
           withLocalDeclD `k kType fun k => do
             let mut e := mkConst noConfusionName (v :: us)
-            e := mkAppN e (xs ++ #[P] ++ is1 ++ #[ctor1] ++ is2 ++ #[ctor2])
-            -- eqs may have more Eq rather than HEq than expected by `noConfusion`
+            e := mkAppN e (#[P] ++ xs ++ is1 ++ #[ctor1] ++ xs ++ is2 ++ #[ctor2])
+            -- Pass rfl equalities for parameters
+            for _ in [:xs.size] do
+              let eq ← whnf (← whnfForall (← inferType e)).bindingDomain!
+              if let some (_,i,_,_) := eq.heq? then
+                e := mkApp e (← mkHEqRefl i)
+              else if let some (_,i,_) := eq.eq? then
+                e := mkApp e (← mkEqRefl i)
+              else
+                throwError "mkNoConfusion: unexpected equality `{eq}` as next argument to{inlineExpr (← inferType e)}"
+            -- Equalities for indices. May require going from Eq to HEq
             for eq in eqs do
               let needsHEq := (← whnfForall (← inferType e)).bindingDomain!.isHEq
               if needsHEq && (← inferType eq).isEq then
@@ -336,11 +359,10 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
               (hints       := ReducibilityHints.abbrev)
             ))
             setReducibleAttribute name
-            let arity := ctorInfo.numParams + 1 + 2 * ctorInfo.numFields + indVal.numIndices + 1
+            let arity := ctorInfo.numParams + 1 + 2 * ctorInfo.numFields + eqvs.size
             let fields := kType.getNumHeadForalls
             modifyEnv fun env => markNoConfusion env name (.perCtor arity fields)
 
-
 def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   -- Do not do anything unless can_elim_to_type. TODO: Extract to util
   let .inductInfo indVal ← getConstInfo declName | return

src/Lean/Meta/Injective.lean

@@ -196,22 +196,23 @@ private structure MkHInjTypeResult where
 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 _ => do
-  withImplicitBinderInfos (params ++ args1) do
+  forallTelescope type fun args1 _ =>
+  withImplicitBinderInfos args1 do
+    let params1 := args1[:ctorVal.numParams]
     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 params2 := args2[:ctorVal.numParams]
+      let lhs := mkAppN (mkConst ctorVal.name us) args1
+      let rhs := mkAppN (mkConst ctorVal.name us) 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 ← 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 idxEqs ← mkEqs (params1 ++ idxs1) (params2 ++ idxs2) (skipIfPropOrEq := false)
         let result ← mkArrowN idxEqs result
-        let thmType ← mkForallFVars params (← mkForallFVars args1 (← mkForallFVars args2 result))
+        let thmType ← mkForallFVars args1 (← mkForallFVars args2 result)
         return some { thmType, us, numIndices := idxs1.size }
       else
         return none
@@ -231,10 +232,9 @@ private def failedToGenHInj (ctorVal : ConstructorVal) : MetaM α :=
 private partial def mkHInjectiveTheoremValue? (ctorVal : ConstructorVal) (typeInfo : MkHInjTypeResult) : MetaM (Option Expr) := do
   forallTelescopeReducing typeInfo.thmType fun xs type => do
     let noConfusionName := ctorVal.induct.str "noConfusion"
-    let params := xs[*...ctorVal.numParams]
-    let noConfusion := mkAppN (mkConst noConfusionName (0 :: typeInfo.us)) params
+    let noConfusion := mkConst noConfusionName (0 :: typeInfo.us)
     let noConfusion := mkApp noConfusion type
-    let n := xs.size - typeInfo.numIndices - 1
+    let n := xs.size - ctorVal.numParams - typeInfo.numIndices - 1
     let eqs := xs[n...*].toArray
     let eqExprs ← eqs.mapM fun x => do
       match_expr (← inferType x) with

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

@@ -72,28 +72,25 @@ private def propagateCtorHetero (a b : Expr) : GoalM Unit := do
   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 ()
+  if  params₁.size ≠ params₂.size then return () else
   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₂
+    let proof := mkConst hinjDeclName us₁
+    let proof := mkAppN (mkAppN proof args₁) args₂
     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 := mkConst noConfusionName (0 :: us₁)
     let noConfusion := mkApp noConfusion (← getFalseExpr)
-    let noConfusion := mkApp (mkAppN noConfusion indices₁) a
-    let noConfusion := mkApp (mkAppN noConfusion indices₂) b
+    let noConfusion := mkApp (mkAppN noConfusion (params₁ ++ indices₁)) a
+    let noConfusion := mkApp (mkAppN noConfusion (params₂ ++ indices₂)) b
     let proof := noConfusion
     addNewRawFact proof (← inferType proof) gen (.inj (.decl noConfusionName))
 

tests/lean/run/def15.lean

@@ -4,7 +4,7 @@ def head {α} : (as : List α) → as ≠ [] → α
 | [],    h => absurd rfl h
 | a::as, _ => a
 
-theorem head_cons {α} (a : α) (as : List α) : head (a::as) (fun h => List.noConfusion h) = a :=
+theorem head_cons {α} (a : α) (as : List α) : head (a::as) (fun h => List.noConfusion rfl (heq_of_eq h)) = a :=
 rfl
 
 theorem head_cons' {α} (a : α) (as : List α) (h : a::as ≠ []) : head (a::as) h = a :=

tests/lean/run/issue11560.lean

@@ -0,0 +1,21 @@
+structure Fin' (n : Nat) where
+  mk ::
+  val  : Nat
+  isLt : LT.lt val n
+
+example
+ (a b c d : Nat)
+ (h1 : c.succ < a)
+ (h2 : d.succ < b)
+ (hab : a = b)
+ (hcd : @Fin'.mk a c.succ h1 ≍ @Fin'.mk b d.succ h2) :
+ c = d := Fin'.mk.noConfusion hab hcd (fun h => Nat.succ.noConfusion h fun h' => h')
+
+example
+ (a b c d : Nat)
+ (h1 : c.succ < a)
+ (h2 : d.succ < b)
+ (hab : a = b)
+ (hcd : @Fin'.mk a c.succ h1 ≍ @Fin'.mk b d.succ h2) :
+ c = d := by
+  grind

tests/lean/run/noConfusionCtorInjection.lean

@@ -6,7 +6,8 @@ inductive L (α : Type u) : Type u where
 /--
 info: theorem L.cons.inj.{u} : ∀ {α : Type u} {x : α} {xs : L α} {x_1 : α} {xs_1 : L α},
   L.cons x xs = L.cons x_1 xs_1 → x = x_1 ∧ xs = xs_1 :=
-fun {α} {x} {xs} {x_1} {xs_1} x_2 => L.cons.noConfusion x_2 fun x_eq xs_eq => ⟨x_eq, xs_eq⟩
+fun {α} {x} {xs} {x_1} {xs_1} x_2 =>
+  L.cons.noConfusion (Eq.refl α) (heq_of_eq x_2) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
 -/
 #guard_msgs in
 #print L.cons.inj
@@ -20,7 +21,8 @@ theorem ex1 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
 /--
 info: theorem ex1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
   L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
-fun {α} {x} {xs} {y} {ys} h => L.cons.noConfusion h fun x_eq xs_eq => ⟨x_eq, xs_eq⟩
+fun {α} {x} {xs} {y} {ys} h =>
+  L.cons.noConfusion (Eq.refl α) (heq_of_eq h) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
 -/
 #guard_msgs in #print ex1