experiment: forbid large elim of recursive Prop inductives

src/Init/WF.lean

@@ -30,17 +30,6 @@ inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
   -/
   | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x
 
-noncomputable abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
-    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
-    {a : α} (n : Acc r a) : C a :=
-  n.rec m
-
-noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
-    {a : α} (n : Acc r a)
-    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
-    : C a :=
-  n.rec m
-
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
@@ -81,12 +70,59 @@ namespace WellFounded
 theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
+/--
+Graph of a well-founded fixpoint: `FixGraph F x c` holds when `c : C x` is the value
+obtained by unfolding `F` along the accessibility tree. This recursive `Prop` inductive
+is used to define `WellFounded.fix` without large elimination of `Acc`.
+-/
+inductive FixGraph {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) : (x : α) → C x → Prop where
+  | mk (x : α) (g : (y : α) → r y x → C y)
+       (ih : ∀ (y : α) (h : r y x), FixGraph F y (g y h))
+       : FixGraph F x (F x g)
+
+theorem FixGraph_nonempty
+    {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) {x : α} (acx : Acc r x) :
+    Nonempty {c : C x // FixGraph F x c} := by
+  induction acx with
+  | intro x' _ ih =>
+    refine ⟨?_⟩
+    refine ⟨F x' (fun y h => (Classical.choice (ih y h)).val),
+            FixGraph.mk x' _ (fun y h => ?_)⟩
+    exact (Classical.choice (ih y h)).property
+
+noncomputable def fixFImpl
+    {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (acx : Acc r x) : C x :=
+  (Classical.choice (FixGraph_nonempty F acx)).val
+
+theorem fixFImpl_graph
+    {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (acx : Acc r x) :
+    FixGraph F x (fixFImpl F x acx) :=
+  (Classical.choice (FixGraph_nonempty F acx)).property
+
+theorem FixGraph_funct
+    {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) {x : α} (acx : Acc r x) :
+    ∀ (c₁ c₂ : C x), FixGraph F x c₁ → FixGraph F x c₂ → c₁ = c₂ := by
+  induction acx with
+  | intro x _ ih =>
+    intro c₁ c₂ h₁ h₂
+    cases h₁ with
+    | mk _ g₁ ih₁ =>
+      cases h₂ with
+      | mk _ g₂ ih₂ =>
+        have hg : g₁ = g₂ :=
+          funext fun y => funext fun h => ih y h _ _ (ih₁ y h) (ih₂ y h)
+        exact hg ▸ rfl
+
 section
 variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
 
-noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
-  induction (apply hwf a) with
-  | intro x₁ _ ih => exact h x₁ ih
+noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
+  fixFImpl h a (apply hwf a)
 
 include hwf in
 theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
@@ -95,13 +131,15 @@ theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y)
 variable {C : α → Sort v}
 variable (F : ∀ x, (∀ y, r y x → C y) → C x)
 
-noncomputable def fixF (x : α) (a : Acc r x) : C x := by
-  induction a with
-  | intro x₁ _ ih => exact F x₁ ih
+noncomputable def fixF (x : α) (a : Acc r x) : C x :=
+  fixFImpl F x a
 
-theorem fixF_eq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
-  induction acx with
-  | intro x r _ => exact rfl
+theorem fixF_eq (x : α) (acx : Acc r x) :
+    fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
+  have h1 : FixGraph F x (fixF F x acx) := fixFImpl_graph F x acx
+  have h2 : FixGraph F x (F x (fun y p => fixF F y (Acc.inv acx p))) :=
+    FixGraph.mk x _ (fun y h => fixFImpl_graph F y (Acc.inv acx h))
+  exact FixGraph_funct F acx _ _ h1 h2
 
 /-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
 This can be used in recursive function definitions to explicitly use a different relation

src/Init/WFComputable.lean

@@ -10,23 +10,17 @@ import Init.NotationExtra
 import Init.WFTactics
 
 /-!
-# Computable Acc.rec and WellFounded.fix
-
-This file adds csimp theorems so that the compiler will be able to compile
-`Acc.rec`, `WellFounded.fix` and related operations.
-
-Without this change, the following code will fail to compile as
-`WellFounded.fix` is noncomputable.
-
-```
-def log2p1 : Nat → Nat :=
-  WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
-    let m := n / 2
-    if h : m < n then
-      IH m h + 1
-    else
-      0
-```
+# Compilable WellFounded.fix
+
+This module supplies `@[csimp]` lemmas so that `WellFounded.fixF` and
+`WellFounded.fix` compile to direct recursive code, even though their
+logical definitions go through `Classical.choice`.
+
+Under the no-large-elim-of-Acc experiment, `Acc.rec` is restricted to
+`Prop` motives, so the original `Acc.recC` / `Acc.ndrec` csimp pairs no
+longer typecheck (the recursor has lost its motive universe parameter).
+Code that compiled because of those rules now needs to rely on these
+`WellFounded.*` csimp rules instead.
 -/
 
 namespace Acc
@@ -35,64 +29,50 @@ public instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Ac
   rel := InvImage r (·.1)
   wf  := ⟨fun ac => InvImage.accessible _ ac.2⟩
 
-/-- A computable version of `Acc.rec`. -/
-@[specialize, elab_as_elim] public def recC {motive : (a : α) → Acc r a → Sort v}
-    (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
-     ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
-    {a : α} (t : Acc r a) : motive a t :=
-  intro a (fun _ h => t.inv h) (fun _ hr => recC intro (t.inv hr))
-termination_by Subtype.mk a t
-
-@[csimp] public theorem rec_eq_recC : @Acc.rec = @Acc.recC := by
-  funext α r motive intro a t
-  induction t with
-  | intro x h ih =>
-    rw [recC]
-    dsimp only
-    congr; funext y hr; exact ih _ hr
-
-/-- A computable version of `Acc.ndrec`. -/
-@[inline] public abbrev ndrecC {C : α → Sort v}
-    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
-    {a : α} (n : Acc r a) : C a :=
-  n.recC m
-
-@[csimp] public theorem ndrec_eq_ndrecC : @Acc.ndrec = @Acc.ndrecC := by
-  funext α r motive intro a t
-  rw [Acc.ndrec, rec_eq_recC, Acc.ndrecC]
-
-/-- A computable version of `Acc.ndrecOn`. -/
-@[inline] public abbrev ndrecOnC {C : α → Sort v} {a : α} (n : Acc r a)
-    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → r y x → C y) → C x) : C a :=
-  n.recC m
-
-@[csimp] public theorem ndrecOn_eq_ndrecOnC : @Acc.ndrecOn = @Acc.ndrecOnC := by
-  funext α r motive intro a t
-  rw [Acc.ndrecOn, rec_eq_recC, Acc.ndrecOnC]
-
 end Acc
 
 namespace WellFounded
 
-/-- A computable version of `WellFounded.fixF`. -/
-@[inline] public def fixFC {α : Sort u} {r : α → α → Prop}
-    {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) (a : Acc r x) : C x := by
-  induction a using Acc.recC with
-  | intro x₁ _ ih => exact F x₁ ih
+/-- A compilable version of `WellFounded.fixF`. -/
+@[specialize] public def fixFC {α : Sort u} {r : α → α → Prop}
+    {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) (a : Acc r x) : C x :=
+  F x (fun y h => fixFC F y (a.inv h))
+termination_by Subtype.mk x a
+
+unseal fixFC
+
+private theorem fixFC_graph {α : Sort u} {r : α → α → Prop} {C : α → Sort v}
+    (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x) :
+    FixGraph F x (fixFC F x a) := by
+  induction a with
+  | intro x _ ih =>
+    rw [fixFC]
+    exact FixGraph.mk x _ (fun y h => ih y h)
 
 @[csimp] public theorem fixF_eq_fixFC : @fixF = @fixFC := by
   funext α r C F x a
-  rw [fixF, Acc.rec_eq_recC, fixFC]
+  exact FixGraph_funct F a _ _ (fixFImpl_graph F x a) (fixFC_graph F x a)
 
-/-- A computable version of `fix`. -/
+/-- A compilable version of `WellFounded.fix`. -/
 @[specialize] public def fixC {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
     (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   F x (fun y _ => fixC hwf F y)
 termination_by hwf.wrap x
 
 unseal fixC
 
+private theorem fixC_graph {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
+    (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x)
+    (x : α) (acx : Acc r x) : FixGraph F x (fixC hwf F x) := by
+  induction acx with
+  | intro x _ ih =>
+    rw [fixC]
+    exact FixGraph.mk x _ (fun y h => ih y h)
+
 @[csimp] public theorem fix_eq_fixC : @fix = @fixC := by
-  rfl
+  funext α C r hwf F x
+  exact FixGraph_funct F (apply hwf x) _ _
+    (fixFImpl_graph F x (apply hwf x))
+    (fixC_graph hwf F x (apply hwf x))
 
 end WellFounded

src/Init/While.lean

@@ -31,16 +31,28 @@ variable {α : Type u} {m : Type u → Type v} [Monad m]
 public abbrev whileM.IsPlausibleStep (f : α → m (α ⊕ β)) : α → α → Prop :=
   fun a' a => Internal.MayReturn (f a) (.inl a')
 
+/-- One unfolding step of the loop body used by `whileM.fix`. -/
+private noncomputable def whileM.fixF {β : Type u} (f : α → m (α ⊕ β))
+    (hAttach : Exists (Internal.IsAttach (m := m)))
+    (x : α) (ih : ∀ y, whileM.IsPlausibleStep f y x → m β) : m β := do
+  let ⟨s, hp⟩ ← hAttach.choose (f x)
+  match s, hp with
+  | .inl x', hp => ih x' hp
+  | .inr b, _ => pure b
+
 /-- The classical `Acc`-induction defining `whileM`, factored out so it can be referenced from
 `whileM.Pred`, `whileM.impl`, and `whileM_eq` without duplicating the recursion. -/
 private noncomputable def whileM.fix {β : Type u} (f : α → m (α ⊕ β))
     (hAttach : Exists (Internal.IsAttach (m := m))) {a : α}
     (h_a : Acc (whileM.IsPlausibleStep f) a) : m β :=
-  h_a.recOn (motive := fun _ _ => m β) (fun x _ ih => do
-    let ⟨s, hp⟩ ← hAttach.choose (f x)
-    match s, hp with
-    | .inl x', hp => ih x' hp
-    | .inr b, _ => pure b)
+  WellFounded.fixF (whileM.fixF f hAttach) a h_a
+
+private theorem whileM.fix_eq {β : Type u} (f : α → m (α ⊕ β))
+    (hAttach : Exists (Internal.IsAttach (m := m))) {a : α}
+    (h_a : Acc (whileM.IsPlausibleStep f) a) :
+    whileM.fix f hAttach h_a =
+      whileM.fixF f hAttach a (fun _ p => whileM.fix f hAttach (h_a.inv p)) :=
+  WellFounded.fixF_eq _ a h_a
 
 /-- Pinning predicate for `whileM.impl`: trivial unless we have both an `Acc` and
 an attach for `m`, in which case `v` is pinned to the value computed by `whileM.fix`. -/
@@ -66,8 +78,8 @@ private theorem whileM.body_eq_fix
     (g : (a : α) → Subtype (whileM.Pred f a))
     {x : α} (h_x : Acc (whileM.IsPlausibleStep f) x) :
     whileM.body f (g · |>.val) x = whileM.fix f hAttach h_x := by
-  cases h_x with | intro x next =>
-  simp only [whileM.body, whileM.fix]
+  rw [whileM.fix_eq]
+  simp only [whileM.body, whileM.fixF]
   rw [← ((hAttach.choose_spec.erases (f x)).bind_eq)]
   apply bind_congr
   intro ⟨s, hp⟩
@@ -76,7 +88,7 @@ private theorem whileM.body_eq_fix
   | inl x' =>
     have hp_x' := (g x').property
     simp only [whileM.Pred,
-      dif_pos (show Acc _ x' ∧ _ from ⟨next x' hp, hAttach⟩)] at hp_x'
+      dif_pos (show Acc _ x' ∧ _ from ⟨h_x.inv hp, hAttach⟩)] at hp_x'
     exact hp_x'
 
 /-- Computational core of `whileM`: returns the loop value paired with its

src/kernel/inductive.cpp

@@ -500,6 +500,14 @@ class add_inductive_fn {
             return false;
         }
 
+        if (is_rec()) {
+            /* Recursive inductive predicates (e.g. `Acc`, `WellFounded`) only
+               eliminate into Prop.  This blocks `large elimination` of proof terms
+               obtained by recursive constructions; subsingleton-style products like
+               `And`, `Eq`, `Unit`, `Iff` are non-recursive and remain unaffected. */
+            return true;
+        }
+
         /* We have only one constructor, the final check is, the type of each argument
            that is not a parameter:
             1- It must live in Prop, *OR*

tests/elab/csimpCore.lean

@@ -9,8 +9,7 @@ version. The following list shows where this is not yet the case.
 -/
 
 /--
-info: (Acc.rec, Acc.recC)
-(Array.instDecidableEmpEq, Array.instDecidableEmpEqImpl)
+info: (Array.instDecidableEmpEq, Array.instDecidableEmpEqImpl)
 (Array.instDecidableEq, Array.instDecidableEqImpl)
 (Array.instDecidableEqEmp, Array.instDecidableEqEmpImpl)
 (Array.pmap, Array.pmapImpl)

tests/elab/kernelBacktrack.lean

@@ -16,6 +16,6 @@ theorem kernel_error
     (L : List Nat) (hL : L.length = 2 ∧ ∀ i : Fin L.length, L[i] = 0) (i : Nat) :
     L[i % 2] = 0 := sorry
 
-/-- info: 'kernel_error' depends on axioms: [propext, sorryAx, Quot.sound] -/
+/-- info: 'kernel_error' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] -/
 #guard_msgs in
 #print axioms kernel_error

tests/elab/print_cmd.lean

@@ -56,17 +56,15 @@ for Nat.succ (1 fields): fun motive zero succ n => succ n (Nat.rec zero succ n)
 -/
 #guard_msgs in #print Nat.rec
 /--
-info: recursor Acc.rec.{u_1, u} : {α : Sort u} →
-  {r : α → α → Prop} →
-    {motive : (a : α) → Acc r a → Sort u_1} →
-      ((x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯) →
-        {a : α} → (t : Acc r a) → motive a t
+info: recursor Acc.rec.{u} : ∀ {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Prop},
+  (∀ (x : α) (h : ∀ (y : α), r y x → Acc r y), (∀ (y : α) (a : r y x), motive y ⋯) → motive x ⋯) →
+    ∀ {a : α} (t : Acc r a), motive a t
 number of parameters: 2
 number of indices: 1
 number of motives: 1
 number of minors: 1
 rules:
-for Acc.intro (2 fields): fun {α} r motive intro x h => intro x h fun y a => Acc.rec intro ⋯
+for Acc.intro (2 fields): fun {α} r motive intro x h => intro x h fun y a => Acc.rec intro (h y a)
 -/
 #guard_msgs in #print Acc.rec
 /--