feat: add compile_inductive% and compile_def% commands (#4097)

Add a `#compile inductive` command to compile the recursors of an inductive type, which works by creating a recursive definition and using `@[csimp]`.



Co-authored-by: Parth Shastri <31370288+cppio@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: 3 people

Mathlib.lean

@@ -2538,6 +2538,7 @@ import Mathlib.Util.AddRelatedDecl
 import Mathlib.Util.AssertExists
 import Mathlib.Util.AssertNoSorry
 import Mathlib.Util.AtomM
+import Mathlib.Util.CompileInductive
 import Mathlib.Util.Export
 import Mathlib.Util.IncludeStr
 import Mathlib.Util.LongNames

Mathlib/Algebra/DirectSum/Basic.lean

@@ -328,10 +328,9 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i)
   @Dfinsupp.sigmaCurry_apply _ _ δ _ _ i j
 #align direct_sum.sigma_curry_apply DirectSum.sigmaCurry_apply
 
--- Porting note: marked noncomputable
 /-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`.-/
-noncomputable def sigmaUncurry [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)] :
+def sigmaUncurry [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)] :
     (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2
     where
   toFun := Dfinsupp.sigmaUncurry

Mathlib/Algebra/Free.lean

@@ -39,6 +39,7 @@ inductive FreeAddMagma (α : Type u) : Type u
   | add : FreeAddMagma α → FreeAddMagma α → FreeAddMagma α
   deriving DecidableEq
 #align free_add_magma FreeAddMagma
+compile_inductive% FreeAddMagma
 
 /-- Free magma over a given alphabet. -/
 @[to_additive]
@@ -47,6 +48,7 @@ inductive FreeMagma (α : Type u) : Type u
   | mul : FreeMagma α → FreeMagma α → FreeMagma α
   deriving DecidableEq
 #align free_magma FreeMagma
+compile_inductive% FreeMagma
 
 namespace FreeMagma
 
@@ -75,8 +77,7 @@ attribute [nolint simpNF] FreeMagma.mul.injEq
 /-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`. -/
 @[to_additive (attr := elab_as_elim) "Recursor for `FreeAddMagma` using `x + y` instead of
 `FreeAddMagma.add x y`."]
--- Porting note: added noncomputable
-noncomputable def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x))
+def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x))
     (ih2 : ∀ x y, C x → C y → C (x * y)) : C x :=
   FreeMagma.recOn x ih1 ih2
 #align free_magma.rec_on_mul FreeMagma.recOnMul
@@ -164,8 +165,7 @@ instance : Monad FreeMagma where
 
 /-- Recursor on `FreeMagma` using `pure` instead of `of`. -/
 @[to_additive (attr := elab_as_elim) "Recursor on `FreeAddMagma` using `pure` instead of `of`."]
--- Porting note: added noncomputable
-protected noncomputable def recOnPure {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (pure x))
+protected def recOnPure {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (pure x))
     (ih2 : ∀ x y, C x → C y → C (x * y)) : C x :=
   FreeMagma.recOnMul x ih1 ih2
 #align free_magma.rec_on_pure FreeMagma.recOnPure
@@ -449,6 +449,7 @@ structure FreeAddSemigroup (α : Type u) where
 /-- The tail of the element -/
   tail : List α
 #align free_add_semigroup FreeAddSemigroup
+compile_inductive% FreeAddSemigroup
 
 /-- Free semigroup over a given alphabet. -/
 @[to_additive (attr := ext)]
@@ -458,6 +459,7 @@ structure FreeSemigroup (α : Type u) where
 /-- The tail of the element -/
   tail : List α
 #align free_semigroup FreeSemigroup
+compile_inductive% FreeSemigroup
 
 namespace FreeSemigroup
 
@@ -505,8 +507,7 @@ instance [Inhabited α] : Inhabited (FreeSemigroup α) := ⟨of default⟩
 
 /-- Recursor for free semigroup using `of` and `*`. -/
 @[to_additive (attr := elab_as_elim) "Recursor for free additive semigroup using `of` and `+`."]
--- Porting note: added noncomputable
-protected noncomputable def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (of x))
+protected def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (of x))
     (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : C x :=
       FreeSemigroup.recOn x fun f s ↦
       List.recOn s ih1 (fun hd tl ih f ↦ ih2 f ⟨hd, tl⟩ (ih1 f) (ih hd)) f
@@ -587,8 +588,7 @@ instance : Monad FreeSemigroup where
 
 /-- Recursor that uses `pure` instead of `of`. -/
 @[to_additive (attr := elab_as_elim) "Recursor that uses `pure` instead of `of`."]
--- Porting note: added noncomputable
-noncomputable def recOnPure {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (pure x))
+def recOnPure {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (pure x))
     (ih2 : ∀ x y, C (pure x) → C y → C (pure x * y)) : C x :=
   FreeSemigroup.recOnMul x ih1 ih2
 #align free_semigroup.rec_on_pure FreeSemigroup.recOnPure
@@ -631,15 +631,13 @@ instance : LawfulMonad FreeSemigroup.{u} := LawfulMonad.mk'
 
 /-- `FreeSemigroup` is traversable. -/
 @[to_additive "`FreeAddSemigroup` is traversable."]
--- Porting note: added noncomputable
-protected noncomputable def traverse {m : Type u → Type u} [Applicative m] {α β : Type u}
+protected def traverse {m : Type u → Type u} [Applicative m] {α β : Type u}
     (F : α → m β) (x : FreeSemigroup α) : m (FreeSemigroup β) :=
   recOnPure x (fun x ↦ pure <$> F x) fun _x _y ihx ihy ↦ (· * ·) <$> ihx <*> ihy
 #align free_semigroup.traverse FreeSemigroup.traverse
 
 @[to_additive]
--- Porting note: added noncomputable
-noncomputable instance : Traversable FreeSemigroup := ⟨@FreeSemigroup.traverse⟩
+instance : Traversable FreeSemigroup := ⟨@FreeSemigroup.traverse⟩
 
 variable {m : Type u → Type u} [Applicative m] (F : α → m β)
 
@@ -686,9 +684,8 @@ theorem mul_map_seq (x y : FreeSemigroup α) :
     ((· * ·) <$> x <*> y : Id (FreeSemigroup α)) = (x * y : FreeSemigroup α) := rfl
 #align free_semigroup.mul_map_seq FreeSemigroup.mul_map_seq
 
--- Porting note: Added noncomputable
 @[to_additive]
-noncomputable instance : IsLawfulTraversable FreeSemigroup.{u} :=
+instance : IsLawfulTraversable FreeSemigroup.{u} :=
   { instLawfulMonadFreeSemigroupInstMonadFreeSemigroup with
     id_traverse := fun x ↦
       FreeSemigroup.recOnMul x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by

Mathlib/Algebra/Star/Basic.lean

@@ -56,6 +56,9 @@ class Star (R : Type u) where
   star : R → R
 #align has_star Star
 
+-- https://github.com/leanprover/lean4/issues/2096
+compile_def% Star.star
+
 variable {R : Type u}
 
 export Star (star)

Mathlib/Algebra/Star/Pointwise.lean

@@ -97,10 +97,8 @@ theorem iUnion_star {ι : Sort _} [Star α] (s : ι → Set α) : (⋃ i, s i)
 theorem compl_star [Star α] : (sᶜ)⋆ = s⋆ᶜ := preimage_compl
 #align set.compl_star Set.compl_star
 
--- Porting note: add noncomputable to instance
 @[simp]
-noncomputable instance [InvolutiveStar α] : InvolutiveStar (Set α)
-    where
+instance [InvolutiveStar α] : InvolutiveStar (Set α) where
   star := Star.star
   star_involutive s := by simp only [← star_preimage, preimage_preimage, star_star, preimage_id']
 

Mathlib/Combinatorics/Quiver/Path.lean

@@ -32,20 +32,7 @@ inductive Path {V : Type u} [Quiver.{v} V] (a : V) : V → Sort max (u + 1) v
 #align quiver.path Quiver.Path
 
 -- See issue lean4#2049
-/-- A computable version of `Quiver.Path.rec`. Workaround until Lean has native support for this. -/
-def Path.recC.{w, z, t} {V : Type t} [Quiver.{z} V] {a : V} {motive : (b : V) → Path a b → Sort w}
-    (nil : motive a Path.nil)
-    (cons : ({b c : V} → (p : Path a b) → (e : b ⟶ c) → motive b p → motive c (p.cons e))) :
-    {b : V} → (p : Path a b) → motive b p
-  | _, .nil => nil
-  | _, (.cons p e) => cons p e (Quiver.Path.recC nil cons p)
-
-@[csimp] lemma Path.rec_eq_recC : @Path.rec = @Path.recC := by
-  ext V _ a motive nil cons b p
-  induction p with
-  | nil => rfl
-  | cons p e ih =>
-    rw [Path.recC, ←ih]
+compile_inductive% Path
 
 /-- An arrow viewed as a path of length one. -/
 def Hom.toPath {V} [Quiver V] {a b : V} (e : a ⟶ b) : Path a b :=

Mathlib/Computability/PartrecCode.lean

@@ -88,59 +88,7 @@ inductive Code : Type
 #align nat.partrec.code Nat.Partrec.Code
 
 -- Porting note: `Nat.Partrec.Code.recOn` is noncomputable in Lean4, so we make it computable.
-
-/-- A computable version of `Nat.Partrec.Code.rec`.
-Workaround until Lean has native support for this. -/
-@[elab_as_elim] private abbrev Code.recC.{u} {motive : Code → Sort u}
-    (zero : motive .zero) (succ : motive .succ)
-    (left : motive .left) (right : motive .right)
-    (pair : (a a_1 : Code) → motive a → motive a_1 → motive (.pair a a_1))
-    (comp : (a a_1 : Code) → motive a → motive a_1 → motive (.comp a a_1))
-    (prec : (a a_1 : Code) → motive a → motive a_1 → motive (.prec a a_1))
-    (rfind' : (a : Code) → motive a → motive (.rfind' a)) :
-    (t : Code) → motive t
-  | .zero => zero
-  | .succ => succ
-  | .left => left
-  | .right => right
-  | .pair a a_1 => pair a a_1
-    (Code.recC zero succ left right pair comp prec rfind' a)
-    (Code.recC zero succ left right pair comp prec rfind' a_1)
-  | .comp a a_1 => comp a a_1
-    (Code.recC zero succ left right pair comp prec rfind' a)
-    (Code.recC zero succ left right pair comp prec rfind' a_1)
-  | .prec a a_1 => prec a a_1
-    (Code.recC zero succ left right pair comp prec rfind' a)
-    (Code.recC zero succ left right pair comp prec rfind' a_1)
-  | .rfind' a => rfind' a
-    (Code.recC zero succ left right pair comp prec rfind' a)
-
-@[csimp] private theorem Code.rec_eq_recC : @Code.rec = @Code.recC := by
-  funext motive zero succ left right pair comp prec rfind' t
-  induction t with
-  | zero => rfl
-  | succ => rfl
-  | left => rfl
-  | right => rfl
-  | pair a a_1 ia ia_1 => rw [Code.recC, ← ia, ← ia_1]
-  | comp a a_1 ia ia_1 => rw [Code.recC, ← ia, ← ia_1]
-  | prec a a_1 ia ia_1 => rw [Code.recC, ← ia, ← ia_1]
-  | rfind' a ia => rw [Code.recC, ← ia]
-
-/-- A computable version of `Nat.Partrec.Code.recOn`.
-Workaround until Lean has native support for this. -/
-@[elab_as_elim] private abbrev Code.recOnC.{u} {motive : Code → Sort u} (t : Code)
-    (zero : motive .zero) (succ : motive .succ)
-    (left : motive .left) (right : motive .right)
-    (pair : (a a_1 : Code) → motive a → motive a_1 → motive (.pair a a_1))
-    (comp : (a a_1 : Code) → motive a → motive a_1 → motive (.comp a a_1))
-    (prec : (a a_1 : Code) → motive a → motive a_1 → motive (.prec a a_1))
-    (rfind' : (a : Code) → motive a → motive (.rfind' a)) : motive t :=
-  Code.recC (motive := motive) zero succ left right pair comp prec rfind' t
-
-@[csimp] private theorem Code.recOn_eq_recOnC : @Code.recOn = @Code.recOnC := by
-  funext motive t zero succ left right pair comp prec rfind'
-  rw [Code.recOn, Code.rec_eq_recC, Code.recOnC]
+compile_inductive% Code
 
 end Nat.Partrec
 

Mathlib/Computability/TMToPartrec.lean

@@ -940,34 +940,10 @@ inductive Λ'
 #align turing.partrec_to_TM2.Λ'.ret Turing.PartrecToTM2.Λ'.ret
 
 -- Porting note: `Turing.PartrecToTM2.Λ'.rec` is noncomputable in Lean4, so we make it computable.
-
-/-- A computable version of `Turing.PartrecToTM2.Λ'.rec`.
-Workaround until Lean has native support for this. The compiler fails to check the termination,
-so this should be `unsafe`. -/
-@[elab_as_elim] private unsafe abbrev Λ'.recU.{u} {motive : Λ' → Sort u}
-    (move : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → motive q → motive (Λ'.move p k₁ k₂ q))
-    (clear : (p : Γ' → Bool) → (k : K') → (q : Λ') → motive q → motive (Λ'.clear p k q))
-    (copy : (q : Λ') → motive q → motive (Λ'.copy q))
-    (push : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → motive q → motive (Λ'.push k s q))
-    (read : (f : Option Γ' → Λ') → ((a : Option Γ') → motive (f a)) → motive (Λ'.read f))
-    (succ : (q : Λ') → motive q → motive (Λ'.succ q))
-    (pred : (q₁ q₂ : Λ') → motive q₁ → motive q₂ → motive (Λ'.pred q₁ q₂))
-    (ret : (k : Cont') → motive (Λ'.ret k)) :
-    (t : Λ') → motive t
-  | Λ'.move p k₁ k₂ q => move p k₁ k₂ q (Λ'.recU move clear copy push read succ pred ret q)
-  | Λ'.clear p k q => clear p k q (Λ'.recU move clear copy push read succ pred ret q)
-  | Λ'.copy q => copy q (Λ'.recU move clear copy push read succ pred ret q)
-  | Λ'.push k s q => push k s q (Λ'.recU move clear copy push read succ pred ret q)
-  | Λ'.read f => read f (fun a => Λ'.recU move clear copy push read succ pred ret (f a))
-  | Λ'.succ q => succ q (Λ'.recU move clear copy push read succ pred ret q)
-  | Λ'.pred q₁ q₂ => pred q₁ q₂
-      (Λ'.recU move clear copy push read succ pred ret q₁)
-      (Λ'.recU move clear copy push read succ pred ret q₂)
-  | Λ'.ret k => ret k
-
-@[elab_as_elim, implemented_by Λ'.recU] private abbrev Λ'.recC.{u} := @Λ'.rec.{u}
-
-@[csimp] private theorem Λ'.rec_eq_recC : @Λ'.rec = @Λ'.recC := rfl
+compile_inductive% Code
+compile_inductive% Cont'
+compile_inductive% K'
+compile_inductive% Λ'
 
 instance Λ'.instInhabited : Inhabited Λ' :=
   ⟨Λ'.ret Cont'.halt⟩

Mathlib/Data/Analysis/Filter.lean

@@ -122,9 +122,8 @@ def ofEq {f g : Filter α} (e : f = g) (F : f.Realizer) : g.Realizer :=
   ⟨F.σ, F.F, F.eq.trans e⟩
 #align filter.realizer.of_eq Filter.Realizer.ofEq
 
--- Porting note: Added `noncomputable`
 /-- A filter realizes itself. -/
-noncomputable def ofFilter (f : Filter α) : f.Realizer :=
+def ofFilter (f : Filter α) : f.Realizer :=
   ⟨f.sets,
     { f := Subtype.val
       pt := ⟨univ, univ_mem⟩

Mathlib/Data/Dfinsupp/Basic.lean

@@ -1524,7 +1524,7 @@ theorem sigmaCurry_single [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)]
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
 /-- The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`.-/
-noncomputable def sigmaUncurry [∀ i j, Zero (δ i j)]
+def sigmaUncurry [∀ i j, Zero (δ i j)]
     [∀ i, DecidableEq (α i)] [∀ i j (x : δ i j), Decidable (x ≠ 0)]
     (f : Π₀ (i) (j), δ i j) :
     Π₀ i : Σi, _, δ i.1 i.2 where