feat: heterogeneous noConfusion (#11474)

This PR generalizes the `noConfusion` constructions to heterogeneous
equalities (assuming propositional equalities between the indices). This
lays ground work for better support for applying injection to
heterogeneous equalities in grind.

The `Meta.mkNoConfusion` app builder shields most of the code from these
changes.

Since the per-constructor noConfusion principles are now more
expressive, `Meta.mkNoConfusion` no longer uses the general one.

In `Init.Prelude` some proofs are more pedestrian because `injection`
now needs a bit more machinery.

This is a breaking change for whoever uses the `noConfusion` principle
manually and explicitly for a type with indices.

Fixes #11450.

Author: nomeata

src/Init/Data/Int/Basic.lean

@@ -278,7 +278,11 @@ set_option bootstrap.genMatcherCode false in
 def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m => isTrue <| NonNeg.mk m
-  | -[_ +1] => isFalse <| fun h => nomatch h
+  | -[i +1] => isFalse <| fun h =>
+    have : ∀ j, (j = -[i +1]) → NonNeg j → False := fun _ hj hnn =>
+      Int.NonNeg.casesOn (motive := fun j _ => j = -[i +1] → False) hnn
+        (fun _ h => Int.noConfusion h) hj
+    this -[i +1] rfl h
 
 /-- Decides whether `a ≤ b`.
 

src/Init/Prelude.lean

@@ -1837,6 +1837,8 @@ def Nat.ble : @& Nat → @& Nat → Bool
   | succ _, zero   => false
   | succ n, succ m => ble n m
 
+attribute [gen_constructor_elims] Bool
+
 /--
 Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
 -/
@@ -1860,9 +1862,14 @@ protected def Nat.lt (n m : Nat) : Prop :=
 instance instLTNat : LT Nat where
   lt := Nat.lt
 
-theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
-  | 0      => nofun
-  | succ _ => nofun
+theorem Nat.not_succ_le_zero (n : Nat) : LE.le (succ n) 0 → False :=
+  -- No injectivity tactic until `attribute [gen_constructor_elims] Nat`
+  have : ∀ m, Eq m 0 → LE.le (succ n) m → False := fun _ hm hle =>
+    Nat.le.casesOn (motive := fun m _ => Eq m 0 → False) hle
+      (fun h => Nat.noConfusion h)
+      (fun _ h => Nat.noConfusion h)
+      hm
+  this 0 rfl
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n
@@ -1999,10 +2006,12 @@ protected theorem Nat.lt_of_not_le {a b : Nat} (h : Not (LE.le a b)) : LT.lt b a
 
 protected theorem Nat.add_pos_right :
     {b : Nat} → (a : Nat) → (hb : LT.lt 0 b) → LT.lt 0 (HAdd.hAdd a b)
+  | zero, _, h => (Nat.not_succ_le_zero _ h).elim
   | succ _, _, _ => Nat.zero_lt_succ _
 
 protected theorem Nat.mul_pos :
     {n m : Nat} → (hn : LT.lt 0 n) → (hm : LT.lt 0 m) → LT.lt 0 (HMul.hMul n m)
+  | _, zero, _, hb => (Nat.not_succ_le_zero _ hb).elim
   | _, succ _, ha, _ => Nat.add_pos_right _ ha
 
 protected theorem Nat.pow_pos {a : Nat} : {n : Nat} → (h : LT.lt 0 a) → LT.lt 0 (HPow.hPow a n)
@@ -2059,6 +2068,8 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
   | a, 0      => a
   | a, succ b => pred (Nat.sub a b)
 
+attribute [gen_constructor_elims] Nat
+
 instance instSubNat : Sub Nat where
   sub := Nat.sub
 
@@ -2216,9 +2227,6 @@ theorem Nat.mod_lt : (x : Nat) →  {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HM
       | .isTrue _ => Nat.modCore_lt hm
       | .isFalse h => Nat.lt_of_not_le h
 
-attribute [gen_constructor_elims] Nat
-attribute [gen_constructor_elims] Bool
-
 /--
 Gets the word size of the current platform. The word size may be 64 or 32 bits.
 

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -666,11 +666,11 @@ where
     let .const declName _ := e.getAppFn | unreachable!
     let typeName := declName.getPrefix
     let .inductInfo inductVal ← getConstInfo typeName | unreachable!
-    let arity := inductVal.numParams + inductVal.numIndices + 1 /- motive -/ + 2 /- lhs/rhs-/ + 1 /- equality -/
+    let arity := inductVal.numParams + 1 /- motive -/ + 3*(inductVal.numIndices + 1) /- lhs/rhs and equalities -/
     etaIfUnderApplied e arity do
       let args := e.getAppArgs
-      let lhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 1]!
-      let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
+      let lhs ← liftMetaM do Meta.whnf args[inductVal.numParams + 1 + inductVal.numIndices]!
+      let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + 1 + inductVal.numIndices + 1 + inductVal.numIndices]!
       let lhs ← liftMetaM lhs.toCtorIfLit
       let rhs ← liftMetaM rhs.toCtorIfLit
       match (← liftMetaM <| Meta.isConstructorApp? lhs), (← liftMetaM <| Meta.isConstructorApp? rhs) with

src/Lean/Meta/AppBuilder.lean

@@ -478,46 +478,54 @@ def mkNoConfusion (target : Expr) (h : Expr) : MetaM Expr := do
     let α ← whnfD α
     matchConstInduct α.getAppFn (fun _ => throwAppBuilderException `noConfusion ("inductive type expected" ++ indentExpr α)) fun indVal us => do
       let u ← getLevel target
-      if let some (ctorA, ys1) ← constructorApp? a then
-       if let some (ctorB, ys2) ← constructorApp? b then
-        -- Special case for different manifest constructors, where we can use `ctorIdx`
+      if let some (ctorA, ys1) ← constructorApp'? a then
+       if let some (ctorB, ys2) ← constructorApp'? b then
+        -- Different constructors: Use use `ctorIdx`
         if ctorA.cidx ≠ ctorB.cidx then
           let ctorIdxName := Name.mkStr indVal.name "ctorIdx"
           if (← hasConst ctorIdxName) && (← hasConst `noConfusion_of_Nat) then
             let ctorIdx := mkAppN (mkConst ctorIdxName us) α.getAppArgs
             let v ← getLevel α
             return mkApp2 (mkConst ``False.elim [u]) target <|
               mkAppN (mkConst `noConfusion_of_Nat [v]) #[α, ctorIdx, a, b, h]
-
-        -- Special case for same constructors, where we can maybe use the per-constructor
-        -- noConfusion definition with its type already manifest
-        if ctorA.cidx = ctorB.cidx then
+          else
+            throwError "mkNoConfusion: Missing {ctorIdxName} or {`noConfusion_of_Nat}"
+        else
+          -- Same constructors: use per-constructor noConfusion
           -- Nullary constructors, the construction is trivial
           if ctorA.numFields = 0 then
             return ← withLocalDeclD `P target fun P => mkLambdaFVars #[P] P
 
           let noConfusionName := ctorA.name.str "noConfusion"
-          if (← hasConst noConfusionName) then
-            let xs := α.getAppArgs[:ctorA.numParams]
-            let noConfusion := mkAppN (mkConst noConfusionName (u :: us)) xs
-            let fields1 : Array Expr := ys1[ctorA.numParams:]
-            let fields2 : Array Expr := ys2[ctorA.numParams:]
-            let mask ← occursInCtorTypeMask ctorA.name
-            assert! mask.size = ctorA.numFields
-            let mut ok := true
-            let mut fields2' := #[]
-            for m in mask, f1 in fields1, f2 in fields2 do
-              if m then
-                unless (← isDefEq f1 f2) do
-                  ok := false
-                  break
-              else
-                fields2' := fields2'.push f2
-            if ok then
-              return mkAppN noConfusion (#[target] ++ fields1 ++ fields2' ++ #[h])
-
-      -- Fall back: Use generic theorem
-      return mkAppN (mkConst (Name.mkStr indVal.name "noConfusion") (u :: us)) (α.getAppArgs ++ #[target, a, b, h])
+          unless (← hasConst noConfusionName) do
+            throwError "mkNoConfusion: Missing {noConfusionName}"
+          let noConfusionNameInfo ← getConstVal noConfusionName
+
+          let xs := α.getAppArgs[:ctorA.numParams]
+          let noConfusion := mkAppN (mkConst noConfusionName (u :: us)) xs
+          let fields1 : Array Expr := ys1[ctorA.numParams:]
+          let fields2 : Array Expr := ys2[ctorA.numParams:]
+          let mut e := mkAppN noConfusion (#[target] ++ fields1 ++ fields2)
+          let arity := noConfusionNameInfo.type.getNumHeadForalls
+          -- Index equalities expected. Can be less than `indVal.numIndices` when this constructor
+          -- has fixed indices.
+          assert! arity ≥ xs.size + fields1.size + fields2.size + 3
+          let numIndEqs := arity - (xs.size + fields1.size + fields2.size + 3) -- 3 for `target`, `h` and the continuation
+          for _ in [:numIndEqs] 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)}"
+          let eq := (← whnfForall (← inferType e)).bindingDomain!
+          if eq.isHEq then
+            e := mkApp e (← mkHEqOfEq h)
+          else
+            e := mkApp e h
+          return e
+      throwError "mkNoConfusion: No manifest constructors in {a} = {b}"
 
 /-- Given a `monad` and `e : α`, makes `pure e`.-/
 def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=

src/Lean/Meta/Basic.lean

@@ -1834,6 +1834,9 @@ private def withNewBinderInfosImp (bs : Array (FVarId × BinderInfo)) (k : MetaM
 def withNewBinderInfos (bs : Array (FVarId × BinderInfo)) (k : n α) : n α :=
   mapMetaM (fun k => withNewBinderInfosImp bs k) k
 
+def withImplicitBinderInfos (bs : Array Expr) (k : n α) : n α :=
+  withNewBinderInfos (bs.map (·.fvarId!, BinderInfo.implicit)) k
+
 /--
  Execute `k` using a local context where any `x` in `xs` that is tagged as
  instance implicit is treated as a regular implicit. -/