chore: resurrect #8978, #8992, #8973 from bad merge (#9641)

This PR resurrects the changes from #8978, #8992, #8973 which were
accidentally removed by #8996.

Fixes #8962.

---------

Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>

src/Init/Core.lean

@@ -1573,6 +1573,7 @@ gen_injective_theorems% MProd
 gen_injective_theorems% NonScalar
 gen_injective_theorems% Option
 gen_injective_theorems% PLift
+gen_injective_theorems% PULift
 gen_injective_theorems% PNonScalar
 gen_injective_theorems% PProd
 gen_injective_theorems% Prod

src/Init/Prelude.lean

@@ -889,6 +889,27 @@ theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl
 instance [Inhabited α] : Inhabited (ULift α) where
   default := ULift.up default
 
+/--
+Lifts a type or proposition to a higher universe level.
+
+`PULift α` wraps a value of type `α`. It is a generalization of
+`PLift` that allows lifting values who's type may live in `Sort s`.
+It also subsumes `PLift`.
+-/
+-- The universe variable `r` is written first so that `ULift.{r} α` can be used
+-- when `s` can be inferred from the type of `α`.
+structure PULift.{r, s} (α : Sort s) : Sort (max s r 1) where
+  /-- Wraps a value to increase its type's universe level. -/
+  up ::
+  /-- Extracts a wrapped value from a universe-lifted type. -/
+  down : α
+
+/-- Bijection between `α` and `PULift.{v} α` -/
+theorem PULift.up_down {α : Sort u} (b : PULift.{v} α) : Eq (up (down b)) b := rfl
+
+/-- Bijection between `α` and `PULift.{v} α` -/
+theorem PULift.down_up {α : Sort u} (a : α) : Eq (down (up.{v} a)) a := rfl
+
 /--
 Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
 with a proof that the `Bool` is `true` if and only if `p` is true.

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -168,11 +168,12 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
     -- A recursive call
     if let some hmono ← solveMonoCall α inst_α e then
       trace[Elab.Tactic.monotonicity] "Found recursive call {e}:{indentExpr hmono}"
-      unless ← goal.checkedAssign hmono do
+      let hmonoType ← inferType hmono
+      unless ← isDefEq hmonoType type do
         trace[Elab.Tactic.monotonicity] "Failed to assign {hmono} : {← inferType hmono} to goal"
         failK f #[]
+      goal.assign hmono
       return []
-
     let monoThms ← withLocalDeclD `f f.bindingDomain! fun f =>
       -- The discrimination tree does not like open terms
       findMonoThms (e.instantiate1 f)

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -14,10 +14,6 @@ public import Lean.Meta.Constructions.NoConfusionLinear
 public section
 
 
-register_builtin_option backwards.linearNoConfusionType : Bool := {
-  defValue := true
-  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
-}
 
 namespace Lean
 
@@ -32,11 +28,7 @@ def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   let recInfo ← getConstInfo (mkRecName declName)
   unless recInfo.levelParams.length > indVal.levelParams.length do return
 
-  let useLinear ←
-    if backwards.linearNoConfusionType.get (← getOptions) then
-      NoConfusionLinear.deps.allM (hasConst · (skipRealize := true))
-    else
-      pure false
+  let useLinear ← NoConfusionLinear.canUse
 
   if useLinear then
     NoConfusionLinear.mkWithCtorType declName

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -41,14 +41,24 @@ namespace Lean.NoConfusionLinear
 
 open Meta
 
+
+register_builtin_option backwards.linearNoConfusionType : Bool := {
+  defValue := true
+  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
+}
+
 /--
 List of constants that the linear `noConfusionType` construction depends on.
 -/
-def deps : Array Lean.Name :=
-  #[ ``Nat.lt, ``cond, ``Nat, ``PUnit, ``Eq, ``Not, ``dite, ``Nat.decEq, ``Nat.blt ]
+private def deps : Array Lean.Name :=
+  #[ ``cond, ``ULift, ``Eq.ndrec, ``Not, ``dite, ``Nat.decEq, ``Nat.blt ]
 
-def mkNatLookupTable (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
-  let type ← inferType default
+def canUse : MetaM Bool := do
+  unless backwards.linearNoConfusionType.get (← getOptions) do return false
+  unless (← NoConfusionLinear.deps.allM (hasConst · (skipRealize := true))) do return false
+  return true
+
+def mkNatLookupTable (n : Expr) (type : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
   let u ← getLevel type
   let rec go (start stop : Nat) (hstart : start < stop := by omega) (hstop : stop ≤ es.size := by omega) : MetaM Expr := do
     if h : start + 1 = stop then
@@ -63,6 +73,55 @@ def mkNatLookupTable (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr
   else
     go 0 es.size
 
+-- Right-associates the top-most `max`s to work around #5695 for prettier code
+private def reassocMax (l : Level) : Level :=
+  let lvls := maxArgs l #[]
+  let last := lvls.back!
+  lvls.pop.foldr mkLevelMax last
+where
+  maxArgs (l : Level) (lvls : Array Level) : Array Level :=
+  match l with
+  | .max l1 l2 => maxArgs l2 (maxArgs l1 lvls)
+  | _ => lvls.push l
+
+/--
+Takes the max of the levels of the given expressions.
+-/
+def maxLevels (es : Array Expr) (default : Expr) : MetaM Level := do
+  let mut maxLevel ← getLevel default
+  for e in es do
+    let l ← getLevel e
+    maxLevel := mkLevelMax' maxLevel l
+  return reassocMax maxLevel.normalize
+
+private def mkPULift (r : Level) (t : Expr) : MetaM Expr := do
+  let s ← getLevel t
+  return mkApp (mkConst `PULift [r,s]) t
+
+private def withMkPULiftUp (t : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
+  let t  ← whnf t
+  if t.isAppOfArity `PULift 1 then
+    let t' := t.appArg!
+    let e ← k t'
+    return mkApp2 (mkConst `PULift.up (t.appFn!.constLevels!)) t' e
+  else
+    throwError "withMkPULiftUp: expected PULift type, got {t}"
+
+private def mkPULiftDown (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  if t.isAppOfArity `PULift 1 then
+    let t' := t.appArg!
+    return mkApp2 (mkConst `PULift.down t.appFn!.constLevels!) t' e
+  else
+    throwError "mkULiftDown: expected ULift type, got {t}"
+
+def mkNatLookupTableLifting (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
+  let u ← maxLevels es default
+  let default ← mkPULift u default
+  let u' := reassocMax (mkLevelMax' u 1).normalize
+  let es ← es.mapM (mkPULift u)
+  mkNatLookupTable n (.sort u') es default
+
 def mkWithCtorTypeName (indName : Name) : Name :=
   Name.str indName "noConfusionType" |>.str "withCtorType"
 
@@ -79,18 +138,15 @@ def mkWithCtorType (indName : Name) : MetaM Unit := do
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   let indTyCon := mkConst indName us
   let indTyKind ← inferType indTyCon
-  let indLevel ← getLevel indTyKind
-  let e ← forallBoundedTelescope indTyKind info.numParams fun xs  _ => do
+  let e ← forallBoundedTelescope indTyKind info.numParams fun xs _ => do
     withLocalDeclD `P (mkSort v.succ) fun P => do
     withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
-      let default ← mkArrow (mkConst ``PUnit [indLevel]) P
       let es ← info.ctors.toArray.mapM fun ctorName => do
         let ctor := mkAppN (mkConst ctorName us) xs
         let ctorType ← inferType ctor
-        let argType ← forallTelescope ctorType fun ys _ =>
+        forallTelescope ctorType fun ys _ =>
           mkForallFVars ys P
-        mkArrow (mkConst ``PUnit [indLevel]) argType
-      let e ← mkNatLookupTable ctorIdx es default
+      let e ← mkNatLookupTableLifting ctorIdx es P
       mkLambdaFVars ((xs.push P).push ctorIdx) e
 
   let declName := mkWithCtorTypeName indName
@@ -113,7 +169,6 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   let indTyCon := mkConst indName us
   let indTyKind ← inferType indTyCon
-  let indLevel ← getLevel indTyKind
   let e ← forallBoundedTelescope indTyKind info.numParams fun xs t => do
     withLocalDeclD `P (mkSort v.succ) fun P => do
     withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
@@ -138,7 +193,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
               let heq := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) ctorIdx (mkRawNatLit i)
               let «then» ← withLocalDeclD `h heq fun h => do
                 let e ← mkEqNDRec (motive := withCtorTypeNameApp) k h
-                let e := mkApp e (mkConst ``PUnit.unit [indLevel])
+                let e ← mkPULiftDown e
                 let e := mkAppN e zs
                 -- ``Eq.ndrec
                 mkLambdaFVars #[h] e
@@ -195,15 +250,16 @@ def mkNoConfusionTypeLinear (indName : Name) : MetaM Unit := do
                 let alt := mkAppN alt xs
                 let alt := mkApp alt PType
                 let alt := mkApp alt (mkRawNatLit i)
-                let k ← forallTelescopeReducing (← inferType alt).bindingDomain! fun zs2 _ => do
-                  let eqs ← (Array.zip zs1 zs2[1...*]).filterMapM fun (z1,z2) => do
-                    if (← isProof z1) then
-                      return none
-                    else
-                      return some (← mkEqHEq z1 z2)
-                  let k ← mkArrowN eqs P
-                  let k ← mkArrow k P
-                  mkLambdaFVars zs2 k
+                let k ← withMkPULiftUp (← inferType alt).bindingDomain! fun t =>
+                  forallTelescopeReducing t fun zs2 _ => do
+                    let eqs ← (Array.zip zs1 zs2).filterMapM fun (z1,z2) => do
+                      if (← isProof z1) then
+                        return none
+                      else
+                        return some (← mkEqHEq z1 z2)
+                    let k ← mkArrowN eqs P
+                    let k ← mkArrow k P
+                    mkLambdaFVars zs2 k
                 let alt := mkApp alt k
                 let alt := mkApp alt P
                 let alt := mkAppN alt ys

tests/lean/run/8894.lean

@@ -0,0 +1,50 @@
+open Lean.Order
+
+def A : Type := Prop
+def B : Type := Prop
+
+instance : Lean.Order.PartialOrder A where
+  rel := sorry
+  rel_refl := sorry
+  rel_trans := sorry
+  rel_antisymm := sorry
+
+instance : Lean.Order.PartialOrder B where
+  rel := sorry
+  rel_refl := sorry
+  rel_trans := sorry
+  rel_antisymm := sorry
+
+instance : Lean.Order.CCPO A where
+  csup := sorry
+  csup_spec := sorry
+
+instance : Lean.Order.CCPO B where
+  csup := sorry
+  csup_spec := sorry
+
+/--
+error: Could not prove 'tick' to be monotone in its recursive calls:
+  Cannot eliminate recursive call in
+    tock (n + 1)
+-/
+#guard_msgs in
+mutual
+  def tick (n : Nat): A :=
+    tock (n + 1)
+  partial_fixpoint
+
+  def tock (n : Nat) : B :=
+    tick (n + 1)
+  partial_fixpoint
+end
+
+mutual
+  def tick2 (n : Nat): A :=
+    tock2 (n + 1)
+  partial_fixpoint
+
+  def tock2 (n : Nat) : A :=
+    tick2 (n + 1)
+  partial_fixpoint
+end

tests/lean/run/ind_whnf.lean

@@ -4,7 +4,7 @@ inductive Expr : id Type
 
 partial def Expr.fold (f : Nat → α → α) : Expr → α → α
   | var n,    a => f n a
-  | app s as, a => as.foldl (init := a) fun a e => fold f e a
+  | app _ as, a => as.foldl (init := a) fun a e => fold f e a
 
 def Expr.isVar : Expr → Bool
   | var _ => true

tests/lean/run/issue8962.lean

@@ -0,0 +1,40 @@
+-- This triggered a bug in the linear-size `noConfusionType` construction
+-- which confused the kernel when producing the `noConfusion` lemma.
+
+-- set_option debug.skipKernelTC true
+set_option pp.universes true
+
+-- Works
+
+inductive S where
+| a {α : Sort u} {β : Type v} (f : α → β)
+| b
+
+/--
+info: @[reducible] protected def S.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 → Nat → Type (max u u_1 (v + 1)) :=
+fun P ctorIdx =>
+  bif Nat.blt ctorIdx 1 then
+    PULift.{max (u + 1) (u_1 + 1) (v + 2), max (max (u + 1) (u_1 + 1)) (v + 2)}
+      ({α : Sort u} → {β : Type v} → (α → β) → P)
+  else PULift.{max (u + 1) (u_1 + 1) (v + 2), u_1 + 1} P
+-/
+#guard_msgs in
+#print S.noConfusionType.withCtorType
+
+-- Didn't work
+
+inductive T where
+| a {α : Sort u} {β : Sort v} (f : α → β)
+| b
+
+/--
+info: @[reducible] protected def T.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 →
+  Nat → Sort (max (u + 1) (u_1 + 1) (v + 1) (imax u v)) :=
+fun P ctorIdx =>
+  bif Nat.blt ctorIdx 1 then
+    PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), max (max (max (u + 1) (u_1 + 1)) (v + 1)) (imax u v)}
+      ({α : Sort u} → {β : Sort v} → (α → β) → P)
+  else PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), u_1 + 1} P
+-/
+#guard_msgs in
+#print T.noConfusionType.withCtorType

tests/lean/run/linearNoConfusion.lean

@@ -12,53 +12,60 @@ inductive Vec.{u} (α : Type) : Nat → Type u where
   | nil : Vec α 0
   | cons {n} : α → Vec α n → Vec α (n + 1)
 
+
 @[reducible] protected def Vec.noConfusionType.withCtorType'.{u_1, u} :
-    Type → Type u_1 → Nat → Type (max (u + 1) u_1) := fun α P ctorIdx =>
-  bif Nat.blt ctorIdx 1
-  then PUnit.{u + 2} → P
-  else PUnit.{u + 2} → {n : Nat} → α → Vec.{u} α n → P
+  Type → Type u_1 → Nat → Type (max u u_1) :=
+fun α P ctorIdx =>
+  bif Nat.blt ctorIdx 1 then PULift.{max (u+1) (u_1+1)} P
+  else PULift.{max (u+1) (u_1+1)} ({n : Nat} → α → Vec.{u} α n → P)
 
 /--
-info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max (u + 1) u_1) :=
-fun α P ctorIdx => bif ctorIdx.blt 1 then PUnit → P else PUnit → {n : Nat} → α → Vec α n → P
+info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max u u_1) :=
+fun α P ctorIdx =>
+  bif Nat.blt ctorIdx 1 then PULift.{max (u + 1) (u_1 + 1), u_1 + 1} P
+  else PULift.{max (u + 1) (u_1 + 1), max (u + 1) (u_1 + 1)} ({n : Nat} → α → Vec.{u} α n → P)
 -/
 #guard_msgs in
+set_option pp.universes true in
 #print Vec.noConfusionType.withCtorType
 
 example : @Vec.noConfusionType.withCtorType.{u_1,u} = @Vec.noConfusionType.withCtorType'.{u_1,u} := rfl
 
+
 @[reducible] protected noncomputable def Vec.noConfusionType.withCtor'.{u_1, u} : (α : Type) →
   (P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType' α P ctorIdx → P → (a : Nat) → Vec.{u} α a → P :=
 fun _α _P ctorIdx k k' _a x =>
   Vec.casesOn x
-    (if h : ctorIdx = 0 then Eq.ndrec k h PUnit.unit else k')
-    (fun a a_1 => if h : ctorIdx = 1 then Eq.ndrec k h PUnit.unit a a_1 else k')
+    (if h : ctorIdx = 0 then (Eq.ndrec k h).down else k')
+    (fun a a_1 => if h : ctorIdx = 1 then (Eq.ndrec k h).down a a_1 else k')
 
 /--
 info: @[reducible] protected def Vec.noConfusionType.withCtor.{u_1, u} : (α : Type) →
   (P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType α P ctorIdx → P → (a : Nat) → Vec α a → P :=
 fun α P ctorIdx k k' a x =>
-  Vec.casesOn x (if h : ctorIdx = 0 then (h ▸ k) PUnit.unit else k') fun {n} a a_1 =>
-    if h : ctorIdx = 1 then (h ▸ k) PUnit.unit a a_1 else k'
+  Vec.casesOn x (if h : ctorIdx = 0 then (h ▸ k).down else k') fun {n} a a_1 =>
+    if h : ctorIdx = 1 then (h ▸ k).down a a_1 else k'
 -/
 #guard_msgs in
 #print Vec.noConfusionType.withCtor
 
 example : @Vec.noConfusionType.withCtor.{u_1,u} = @Vec.noConfusionType.withCtor'.{u_1,u} := rfl
 
+
 @[reducible] protected def Vec.noConfusionType'.{u_1, u} : {α : Type} →
   {a : Nat} → Sort u_1 → Vec.{u} α a → Vec α a → Sort u_1 :=
 fun {α} {a} P x1 x2 =>
   Vec.casesOn x1
-    (Vec.noConfusionType.withCtor' α (Sort u_1) 0 (fun _x => P → P) P a x2)
-    (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 (fun _x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2)
+    (Vec.noConfusionType.withCtor' α (Sort u_1) 0 ⟨P → P⟩ P a x2)
+    (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 ⟨fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P⟩ P a x2)
 
 /--
 info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} →
   {a : Nat} → Sort u_1 → Vec α a → Vec α a → Sort u_1 :=
 fun {α} {a} P x1 x2 =>
-  Vec.casesOn x1 (Vec.noConfusionType.withCtor α (Sort u_1) 0 (fun x => P → P) P a x2) fun {n} a_1 a_2 =>
-    Vec.noConfusionType.withCtor α (Sort u_1) 1 (fun x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2
+  Vec.casesOn x1 (Vec.noConfusionType.withCtor α (Sort u_1) 0 { down := P → P } P a x2) fun {n} a_1 a_2 =>
+    Vec.noConfusionType.withCtor α (Sort u_1) 1 { down := fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P } P
+      a x2
 -/
 #guard_msgs in
 #print Vec.noConfusionType
@@ -84,3 +91,9 @@ run_meta do
 -- inductive Enum.{u} : Type u where | a | b
 -- set_option pp.universes true in
 -- #print noConfusionTypeEnum
+
+-- A possibly tricky universes case (resulting universe cannot be decremented)
+
+inductive UnivTest.{u,v} (α : Sort v): Sort (max u v 1) where
+  | mk1 : UnivTest α
+  | mk2 : (x : α) → UnivTest α