feat: make Acc.rec and many related defs computable (#3535)

Lean 4 code generator has had no native supports for `Acc.rec`.
This PR makes `Acc.rec` computable.
This change makes many defs computable. Especially, computable `PFun.fix` and `Part.hasFix` enables us to reason about `partial` functions.
This PR also renames some instances and gives `PFun.lift` `@[coe]` attr.

Author: Komyyy

Mathlib/Computability/TuringMachine.lean

@@ -739,8 +739,7 @@ theorem Tape.map_mk₁ {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap 
 /-- Run a state transition function `σ → Option σ` "to completion". The return value is the last
 state returned before a `none` result. If the state transition function always returns `some`,
 then the computation diverges, returning `Part.none`. -/
--- Porting note: Added noncomputable, because `PFun.fix` is noncomputable.
-noncomputable def eval {σ} (f : σ → Option σ) : σ → Part σ :=
+def eval {σ} (f : σ → Option σ) : σ → Part σ :=
   PFun.fix fun s ↦ Part.some <| (f s).elim (Sum.inl s) Sum.inr
 #align turing.eval Turing.eval
 
@@ -826,9 +825,8 @@ theorem Reaches₀.tail' {σ} {f : σ → Option σ} {a b c : σ} (h : Reaches
 which is either terminal (meaning `a = b`) or where the next point also satisfies `C`, then it
 holds of any point where `eval f a` evaluates to `b`. This formalizes the notion that if
 `eval f a` evaluates to `b` then it reaches terminal state `b` in finitely many steps. -/
--- Porting note: Added noncomputable
 @[elab_as_elim]
-noncomputable def evalInduction {σ} {f : σ → Option σ} {b : σ} {C : σ → Sort _} {a : σ}
+def evalInduction {σ} {f : σ → Option σ} {b : σ} {C : σ → Sort _} {a : σ}
     (h : b ∈ eval f a) (H : ∀ a, b ∈ eval f a → (∀ a', f a = some a' → C a') → C a) : C a :=
   PFun.fixInduction h fun a' ha' h' ↦
     H _ ha' fun b' e ↦ h' _ <| Part.mem_some_iff.2 <| by rw [e]; rfl
@@ -1099,8 +1097,7 @@ def init (l : List Γ) : Cfg₀ :=
 
 /-- Evaluate a Turing machine on initial input to a final state,
   if it terminates. -/
--- Porting note: Added noncomputable
-noncomputable def eval (M : Machine₀) (l : List Γ) : Part (ListBlank Γ) :=
+def eval (M : Machine₀) (l : List Γ) : Part (ListBlank Γ) :=
   (Turing.eval (step M) (init l)).map fun c ↦ c.Tape.right₀
 #align turing.TM0.eval Turing.TM0.eval
 
@@ -1411,8 +1408,7 @@ def init (l : List Γ) : Cfg₁ :=
 
 /-- Evaluate a TM to completion, resulting in an output list on the tape (with an indeterminate
 number of blanks on the end). -/
--- Porting note: Added noncomputable
-noncomputable def eval (M : Λ → Stmt₁) (l : List Γ) : Part (ListBlank Γ) :=
+def eval (M : Λ → Stmt₁) (l : List Γ) : Part (ListBlank Γ) :=
   (Turing.eval (step M) (init l)).map fun c ↦ c.Tape.right₀
 #align turing.TM1.eval Turing.TM1.eval
 
@@ -2279,8 +2275,7 @@ def init (k : K) (L : List (Γ k)) : Cfg₂ :=
 #align turing.TM2.init Turing.TM2.init
 
 /-- Evaluates a TM2 program to completion, with the output on the same stack as the input. -/
--- Porting note: Added noncomputable
-noncomputable def eval (M : Λ → Stmt₂) (k : K) (L : List (Γ k)) : Part (List (Γ k)) :=
+def eval (M : Λ → Stmt₂) (k : K) (L : List (Γ k)) : Part (List (Γ k)) :=
   (Turing.eval (step M) (init k L)).map fun c ↦ c.stk k
 #align turing.TM2.eval Turing.TM2.eval
 

Mathlib/Control/Fix.lean

@@ -68,8 +68,7 @@ it satisfies the equations:
   1. `fix f = f (fix f)`          (is a fixed point)
   2. `∀ X, f X ≤ X → fix f ≤ X`   (least fixed point)
 -/
--- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)
-protected noncomputable def fix (x : α) : Part (β x) :=
+protected def fix (x : α) : Part (β x) :=
   (Part.assert (∃ i, (Fix.approx f i x).Dom)) fun h =>
     WellFounded.fix.{1} (Nat.Upto.wf h) (fixAux f) Nat.Upto.zero x
 #align part.fix Part.fix
@@ -122,18 +121,17 @@ end Part
 
 namespace Part
 
--- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)
-noncomputable instance : Fix (Part α) :=
+instance hasFix : Fix (Part α) :=
   ⟨fun f => Part.fix (fun x u => f (x u)) ()⟩
+#align part.has_fix Part.hasFix
 
 end Part
 
 open Sigma
 
 namespace Pi
 
--- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)
-noncomputable instance Part.hasFix {β} : Fix (α → Part β) :=
+instance Part.hasFix {β} : Fix (α → Part β) :=
   ⟨Part.fix⟩
 #align pi.part.has_fix Pi.Part.hasFix
 

Mathlib/Control/LawfulFix.lean

@@ -208,9 +208,7 @@ theorem to_unit_cont (f : Part α →o Part α) (hc : Continuous f) : Continuous
     erw [hc, Chain.map_comp]; rfl
 #align part.to_unit_cont Part.to_unit_cont
 
--- Porting note: `noncomputable` is required because the code generator does not support recursor
---               `Acc.rec` yet.
-noncomputable instance lawfulFix : LawfulFix (Part α) :=
+instance lawfulFix : LawfulFix (Part α) :=
   ⟨fun {f : Part α →o Part α} hc ↦ show Part.fix (toUnitMono f) () = _ by
     rw [Part.fix_eq (to_unit_cont f hc)]; rfl⟩
 #align part.lawful_fix Part.lawfulFix
@@ -221,9 +219,7 @@ open Sigma
 
 namespace Pi
 
--- Porting note: `noncomputable` is required because the code generator does not support recursor
---               `Acc.rec` yet.
-noncomputable instance lawfulFix {β} : LawfulFix (α → Part β) :=
+instance lawfulFix {β} : LawfulFix (α → Part β) :=
   ⟨fun {_f} ↦ Part.fix_eq⟩
 #align pi.lawful_fix Pi.lawfulFix
 

Mathlib/Data/Finset/PImage.lean

@@ -61,7 +61,7 @@ variable [DecidableEq β] {f g : α →. β} [∀ x, Decidable (f x).Dom] [∀ x
   {s t : Finset α} {b : β}
 
 /-- Image of `s : Finset α` under a partially defined function `f : α →. β`. -/
-noncomputable def pimage (f : α →. β) [∀ x, Decidable (f x).Dom] (s : Finset α) : Finset β :=
+def pimage (f : α →. β) [∀ x, Decidable (f x).Dom] (s : Finset α) : Finset β :=
   s.bunionᵢ fun x => (f x).toFinset
 #align finset.pimage Finset.pimage
 

Mathlib/Data/PFun.lean

@@ -70,8 +70,9 @@ namespace PFun
 
 variable {α β γ δ ε ι : Type _}
 
-instance : Inhabited (α →. β) :=
+instance inhabited : Inhabited (α →. β) :=
   ⟨fun _ => Part.none⟩
+#align pfun.inhabited PFun.inhabited
 
 /-- The domain of a partial function -/
 def Dom (f : α →. β) : Set α :=
@@ -134,11 +135,13 @@ theorem asSubtype_eq_of_mem {f : α →. β} {x : α} {y : β} (fxy : y ∈ f x)
 #align pfun.as_subtype_eq_of_mem PFun.asSubtype_eq_of_mem
 
 /-- Turn a total function into a partial function. -/
+@[coe]
 protected def lift (f : α → β) : α →. β := fun a => Part.some (f a)
 #align pfun.lift PFun.lift
 
-instance : Coe (α → β) (α →. β) :=
+instance coe : Coe (α → β) (α →. β) :=
   ⟨PFun.lift⟩
+#align pfun.has_coe PFun.coe
 
 @[simp]
 theorem coe_val (f : α → β) (a : α) : (f : α →. β) a = Part.some (f a) :=
@@ -219,16 +222,18 @@ theorem bind_apply (f : α →. β) (g : β → α →. γ) (a : α) : f.bind g
 def map (f : β → γ) (g : α →. β) : α →. γ := fun a => (g a).map f
 #align pfun.map PFun.map
 
-instance : Monad (PFun α) where
+instance monad : Monad (PFun α) where
   pure := PFun.pure
   bind := PFun.bind
   map := PFun.map
+#align pfun.monad PFun.monad
 
-instance : LawfulMonad (PFun α) := LawfulMonad.mk'
+instance lawfulMonad : LawfulMonad (PFun α) := LawfulMonad.mk'
   (bind_pure_comp := fun f x => funext fun a => Part.bind_some_eq_map _ _)
   (id_map := fun f => by funext a ; dsimp [Functor.map, PFun.map] ; cases f a; rfl)
   (pure_bind := fun x f => funext fun a => Part.bind_some _ (f x))
   (bind_assoc := fun f g k => funext fun a => (f a).bind_assoc (fun b => g b a) fun b => k b a)
+#align pfun.is_lawful_monad PFun.lawfulMonad
 
 theorem pure_defined (p : Set α) (x : β) : p ⊆ (@PFun.pure α _ x).Dom :=
   p.subset_univ
@@ -245,8 +250,7 @@ exists. By abusing notation to illustrate, either `f a` is in the `β` part of `
 case `f.fix a` returns `f a`), or it is undefined (in which case `f.fix a` is undefined as well), or
 it is in the `α` part of `β ⊕ α` (in which case we repeat the procedure, so `f.fix a` will return
 `f.fix (f a)`). -/
--- Porting note: had to mark `noncomputable`
-noncomputable def fix (f : α →. Sum β α) : α →. β := fun a =>
+def fix (f : α →. Sum β α) : α →. β := fun a =>
   Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) $ fun h =>
     WellFounded.fixF
       (fun a IH =>
@@ -323,9 +327,8 @@ theorem fix_fwd {f : α →. Sum β α} {b : β} {a a' : α} (hb : b ∈ f.fix a
 #align pfun.fix_fwd PFun.fix_fwd
 
 /-- A recursion principle for `PFun.fix`. -/
--- Porting note: had to add `noncomputable`
 @[elab_as_elim]
-noncomputable def fixInduction {C : α → Sort _} {f : α →. Sum β α} {b : β} {a : α} (h : b ∈ f.fix a)
+def fixInduction {C : α → Sort _} {f : α →. Sum β α} {b : β} {a : α} (h : b ∈ f.fix a)
     (H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') : C a := by
   have h₂ := (Part.mem_assert_iff.1 h).snd;
   -- Porting note: revert/intro trick required to address `generalize_proofs` bug
@@ -351,7 +354,7 @@ theorem fixInduction_spec {C : α → Sort _} {f : α →. Sum β α} {b : β} {
 `a` given that `f a` inherits `P` from `a` and `P` holds for preimages of `b`.
 -/
 @[elab_as_elim]
-noncomputable def fixInduction' {C : α → Sort _} {f : α →. Sum β α} {b : β} {a : α}
+def fixInduction' {C : α → Sort _} {f : α →. Sum β α} {b : β} {a : α}
     (h : b ∈ f.fix a) (hbase : ∀ a_final : α, Sum.inl b ∈ f a_final → C a_final)
     (hind : ∀ a₀ a₁ : α, b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) : C a := by
   refine' fixInduction h fun a' h ih => _

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -39,7 +39,7 @@ instance linearOrder : LinearOrder ℕ where
 
 protected def strong_rec_on {p : ℕ → Sort u}
   (n : ℕ) (H : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
-Nat.lt_wfRel.wf.fix' H n
+Nat.lt_wfRel.wf.fix H n
 
 @[elab_as_elim]
 protected lemma strong_induction_on {p : Nat → Prop} (n : Nat) (h : ∀ n, (∀ m, m < n → p m) → p n) :
@@ -257,7 +257,7 @@ private def wf_lbp : WellFounded (lbp p) := by
   | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)
 /-- Used in the definition of `Nat.find`. Returns the smallest natural satisfying `p`-/
 protected def findX : {n // p n ∧ ∀ m, m < n → ¬p m} :=
-(wf_lbp H).fix' (C := fun k ↦ (∀n, n < k → ¬p n) → {n // p n ∧ ∀ m, m < n → ¬p m})
+(wf_lbp H).fix (C := fun k ↦ (∀n, n < k → ¬p n) → {n // p n ∧ ∀ m, m < n → ¬p m})
   (fun m IH al ↦ if pm : p m then ⟨m, pm, al⟩ else
       have this : ∀ n, n ≤ m → ¬p n := fun n h ↦
         (lt_or_eq_of_le h).elim (al n) fun e ↦ by rw [e]; exact pm

Mathlib/Init/Logic.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 import Std.Tactic.Ext
 import Std.Tactic.Lint.Basic
 import Std.Logic
+import Std.WF
 import Mathlib.Tactic.Alias
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Relation.Rfl
@@ -543,18 +544,6 @@ theorem right_comm : Commutative f → Associative f → RightCommutative f :=
 
 end Binary
 
-namespace WellFounded
-
-variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
-
-unsafe def fix'.impl (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
-  F x fun y _ ↦ impl hwf F y
-
-@[implemented_by fix'.impl]
-def fix' (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := hwf.fix F x
-
-end WellFounded
-
 #align not.elim Not.elim
 #align not.imp Not.imp
 #align not_not_of_not_imp not_not_of_not_imp

Mathlib/Order/GameAdd.lean

@@ -122,7 +122,7 @@ namespace Prod
 
 /-- Recursion on the well-founded `Prod.GameAdd` relation.
   Note that it's strictly more general to recurse on the lexicographic order instead. -/
-noncomputable def GameAdd.fix {C : α → β → Sort _} (hα : WellFounded rα) (hβ : WellFounded rβ)
+def GameAdd.fix {C : α → β → Sort _} (hα : WellFounded rα) (hβ : WellFounded rβ)
     (IH : ∀ a₁ b₁, (∀ a₂ b₂, GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α) (b : β) :
     C a b :=
   @WellFounded.fix (α × β) (fun x => C x.1 x.2) _ (hα.prod_gameAdd hβ)
@@ -229,7 +229,7 @@ theorem WellFounded.sym2_gameAdd (h : WellFounded rα) : WellFounded (Sym2.GameA
 namespace Sym2
 
 /-- Recursion on the well-founded `Sym2.GameAdd` relation. -/
-noncomputable def GameAdd.fix {C : α → α → Sort _} (hr : WellFounded rα)
+def GameAdd.fix {C : α → α → Sort _} (hr : WellFounded rα)
     (IH : ∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα ⟦(a₂, b₂)⟧ ⟦(a₁, b₁)⟧ → C a₂ b₂) → C a₁ b₁) (a b : α) :
     C a b :=
   @WellFounded.fix (α × α) (fun x => C x.1 x.2) _ hr.sym2_gameAdd.of_quotient_lift₂

lake-manifest.json

@@ -16,6 +16,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "1852d720729c4651f251793f0155d8240d28acc2",
+    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
     "name": "std",
     "inputRev?": "main"}}]}