From 19e2b8d26f3ce10b14e27bb3830dec08a4270f61 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 20 Jan 2023 17:48:01 +0000
Subject: [PATCH] fix: make List.rec and Nat.rec computable (#1720)

This works around https://github.com/leanprover/lean4/issues/2049. By manually adding compiler support for these recursors, we make a large number of porting notes redundant.
---
 Mathlib/Algebra/FreeMonoid/Basic.lean |  6 +++---
 Mathlib/Data/Fin/Basic.lean           |  9 ++++----
 Mathlib/Data/Fin/Tuple/Basic.lean     |  3 +--
 Mathlib/Data/Finset/Pi.lean           |  3 +--
 Mathlib/Data/Fintype/Pi.lean          |  9 +++-----
 Mathlib/Data/Fintype/Vector.lean      |  3 ---
 Mathlib/Data/List/Defs.lean           | 30 +++++++++++++++++++++++++--
 Mathlib/Data/Multiset/Basic.lean      |  4 ----
 Mathlib/Data/Multiset/Pi.lean         |  2 --
 Mathlib/Data/Multiset/Sections.lean   |  4 +---
 Mathlib/Data/PNat/Basic.lean          |  3 ---
 Mathlib/Data/Vector/Basic.lean        |  9 +++-----
 Mathlib/Init/Data/Nat/Basic.lean      | 19 +++++++++++++++++
 13 files changed, 63 insertions(+), 41 deletions(-)

diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean
index 30e25e4099372..bc3ccc933898a 100644
--- a/Mathlib/Algebra/FreeMonoid/Basic.lean
+++ b/Mathlib/Algebra/FreeMonoid/Basic.lean
@@ -138,9 +138,9 @@ theorem of_injective : Function.Injective (@of α) := List.singleton_injective
 /-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
 @[elab_as_elim, to_additive "Recursor for `FreeAddMonoid` using `0` and `FreeAddMonoid.of x + xs`
 instead of `[]` and `x :: xs`."]
--- Porting note: added noncomputable
-noncomputable def recOn {C : FreeMonoid α → Sort _} (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.recOn xs h0 ih
+-- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
+def recOn {C : FreeMonoid α → Sort _} (xs : FreeMonoid α) (h0 : C 1)
+    (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs
 #align free_monoid.rec_on FreeMonoid.recOn
 
 @[to_additive (attr := simp)]
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 1444ddc095ab0..8a054d7660e73 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -1657,8 +1657,7 @@ This function has two arguments: `h0` handles the base case on `C 0`,
 and `hs` defines the inductive step using `C i.castSucc`.
 -/
 @[elab_as_elim]
---Porting note: marked noncomputable
-noncomputable def induction {C : Fin (n + 1) → Sort _} (h0 : C 0)
+def induction {C : Fin (n + 1) → Sort _} (h0 : C 0)
     (hs : ∀ i : Fin n, C (castSucc i) → C i.succ) :
     ∀ i : Fin (n + 1), C i := by
   rintro ⟨i, hi⟩
@@ -1696,7 +1695,7 @@ and `hs` defines the inductive step using `C i.castSucc`.
 A version of `Fin.induction` taking `i : Fin (n + 1)` as the first argument.
 -/
 @[elab_as_elim]
-noncomputable def inductionOn (i : Fin (n + 1)) {C : Fin (n + 1) → Sort _} (h0 : C 0)
+def inductionOn (i : Fin (n + 1)) {C : Fin (n + 1) → Sort _} (h0 : C 0)
     (hs : ∀ i : Fin n, C (castSucc i) → C i.succ) : C i :=
   induction h0 hs i
 #align fin.induction_on Fin.inductionOn
@@ -1704,7 +1703,7 @@ noncomputable def inductionOn (i : Fin (n + 1)) {C : Fin (n + 1) → Sort _} (h0
 /-- Define `f : Π i : Fin n.succ, C i` by separately handling the cases `i = 0` and
 `i = j.succ`, `j : Fin n`. -/
 @[elab_as_elim]
-noncomputable def cases {C : Fin (n + 1) → Sort _} (H0 : C 0) (Hs : ∀ i : Fin n, C i.succ) :
+def cases {C : Fin (n + 1) → Sort _} (H0 : C 0) (Hs : ∀ i : Fin n, C i.succ) :
     ∀ i : Fin (n + 1), C i :=
   induction H0 fun i _ => Hs i
 #align fin.cases Fin.cases
@@ -1783,7 +1782,7 @@ theorem reverse_induction_last {n : ℕ} {C : Fin (n + 1) → Sort _} (h0 : C (F
 @[simp]
 theorem reverse_induction_castSucc {n : ℕ} {C : Fin (n + 1) → Sort _} (h0 : C (Fin.last n))
     (hs : ∀ i : Fin n, C i.succ → C (castSucc i)) (i : Fin n) :
-    (reverseInduction h0 hs (castSucc i) : 
+    (reverseInduction h0 hs (castSucc i) :
     C (castSucc i)) = hs i (reverseInduction h0 hs i.succ) := by
   rw [reverseInduction, dif_neg (_root_.ne_of_lt (Fin.castSucc_lt_last i))]
   cases i
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index c59b4afbe7716..53178a3305ea0 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -66,9 +66,8 @@ theorem tail_def {n : ℕ} {α : Fin (n + 1) → Type _} {q : ∀ i, α i} :
   rfl
 #align fin.tail_def Fin.tail_def
 
--- Porting note: I made this noncomputable because Lean seemed to think it should be
 /-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
-noncomputable def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j
+def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j
 #align fin.cons Fin.cons
 
 @[simp]
diff --git a/Mathlib/Data/Finset/Pi.lean b/Mathlib/Data/Finset/Pi.lean
index 3646abdfaa699..fdf9231e9b6f2 100644
--- a/Mathlib/Data/Finset/Pi.lean
+++ b/Mathlib/Data/Finset/Pi.lean
@@ -38,8 +38,7 @@ variable {δ : α → Type _} [DecidableEq α]
 /-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
 Note that the elements of `s.pi t` are only partially defined, on `s`. -/
---Porting note: marked noncomputable
-noncomputable def pi (s : Finset α) (t : ∀ a, Finset (δ a)) : Finset (∀ a ∈ s, δ a) :=
+def pi (s : Finset α) (t : ∀ a, Finset (δ a)) : Finset (∀ a ∈ s, δ a) :=
   ⟨s.1.pi fun a => (t a).1, s.nodup.pi fun a _ => (t a).nodup⟩
 #align finset.pi Finset.pi
 
diff --git a/Mathlib/Data/Fintype/Pi.lean b/Mathlib/Data/Fintype/Pi.lean
index 19c202a6df4f5..c15e6c23bef40 100644
--- a/Mathlib/Data/Fintype/Pi.lean
+++ b/Mathlib/Data/Fintype/Pi.lean
@@ -28,7 +28,7 @@ variable [DecidableEq α] [Fintype α] {δ : α → Type _}
 finset `Fintype.piFinset t` of all functions taking values in `t a` for all `a`. This is the
 analogue of `Finset.pi` where the base finset is `univ` (but formally they are not the same, as
 there is an additional condition `i ∈ Finset.univ` in the `Finset.pi` definition). -/
-noncomputable def piFinset (t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a) :=
+def piFinset (t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a) :=
   (Finset.univ.pi t).map ⟨fun f a => f a (mem_univ a), fun _ _ =>
     by simp (config := {contextual := true}) [Function.funext_iff]⟩
 #align fintype.pi_finset Fintype.piFinset
@@ -84,10 +84,8 @@ end Fintype
 
 /-! ### pi -/
 
-
---Porting note: added noncomputable
 /-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
-noncomputable instance Pi.fintype {α : Type _} {β : α → Type _} [DecidableEq α] [Fintype α]
+instance Pi.fintype {α : Type _} {β : α → Type _} [DecidableEq α] [Fintype α]
     [∀ a, Fintype (β a)] : Fintype (∀ a, β a) :=
   ⟨Fintype.piFinset fun _ => univ, by simp⟩
 #align pi.fintype Pi.fintype
@@ -100,8 +98,7 @@ theorem Fintype.piFinset_univ {α : Type _} {β : α → Type _} [DecidableEq α
   rfl
 #align fintype.pi_finset_univ Fintype.piFinset_univ
 
---Porting note: added noncomputable
-noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β]
+instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β]
     [DecidableEq α] [DecidableEq β] : Fintype (α ↪ β) :=
   Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
 #align function.embedding.fintype Function.Embedding.fintype
diff --git a/Mathlib/Data/Fintype/Vector.lean b/Mathlib/Data/Fintype/Vector.lean
index 130e87fc9d44d..7c298fb036582 100644
--- a/Mathlib/Data/Fintype/Vector.lean
+++ b/Mathlib/Data/Fintype/Vector.lean
@@ -17,18 +17,15 @@ import Mathlib.Data.Sym.Basic
 
 variable {α : Type _}
 
-noncomputable -- Porting note: added noncomputable
 instance Vector.fintype [Fintype α] {n : ℕ} : Fintype (Vector α n) :=
   Fintype.ofEquiv _ (Equiv.vectorEquivFin _ _).symm
 #align vector.fintype Vector.fintype
 
-noncomputable -- Porting note: added noncomputable
 instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym.Sym' α n) := by
   refine @Quotient.fintype _ _ _ ?_
   -- Porting note: had to build the instance manually
   intros x y
   apply List.decidablePerm
 
-noncomputable -- Porting note: added noncomputable
 instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym α n) :=
   Fintype.ofEquiv _ Sym.symEquivSym'.symm
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
index d334f8e5f0f45..747630e1b2374 100644
--- a/Mathlib/Data/List/Defs.lean
+++ b/Mathlib/Data/List/Defs.lean
@@ -32,6 +32,32 @@ namespace List
 
 open Function Nat
 
+section recursor_workarounds
+/-- A computable version of `List.rec`. Workaround until Lean has native support for this. -/
+def recC.{u_1, u} {α : Type u} {motive : List α → Sort u_1} (nil : motive [])
+  (cons : (head : α) → (tail : List α) → motive tail → motive (head :: tail)) :
+    (l : List α) → motive l
+| [] => nil
+| (x :: xs) => cons x xs (List.recC nil cons xs)
+
+@[csimp]
+lemma rec_eq_recC : @List.rec = @List.recC := by
+  ext α motive nil cons l
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    rw [List.recC, ←ih]
+
+/-- A computable version of `List._sizeOf_inst`. -/
+def _sizeOf_instC.{u} (α : Type u) [SizeOf α] : SizeOf (List α) where
+  sizeOf t := List.rec 1 (fun head _ tail_ih => 1 + SizeOf.sizeOf head + tail_ih) t
+
+@[csimp]
+lemma _sizeOfinst_eq_sizeOfinstC : @List._sizeOf_inst = @List._sizeOf_instC := by
+  simp [List._sizeOf_1, List._sizeOf_instC, _sizeOf_inst]
+
+end recursor_workarounds
+
 universe u v w x
 
 variable {α β γ δ ε ζ : Type _}
@@ -344,14 +370,14 @@ theorem chain_cons {a b : α} {l : List α} : Chain R a (b :: l) ↔ R a b ∧ C
    fun ⟨n, p⟩ ↦ p.cons n⟩
 #align list.chain_cons List.chain_cons
 
-noncomputable instance decidableChain [DecidableRel R] (a : α) (l : List α) :
+instance decidableChain [DecidableRel R] (a : α) (l : List α) :
     Decidable (Chain R a l) := by
   induction l generalizing a with
   | nil => simp only [List.Chain.nil]; infer_instance
   | cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
 #align list.decidable_chain List.decidableChain
 
-noncomputable instance decidableChain' [DecidableRel R] (l : List α) : Decidable (Chain' R l) := by
+instance decidableChain' [DecidableRel R] (l : List α) : Decidable (Chain' R l) := by
   cases l <;> dsimp only [List.Chain'] <;> infer_instance
 #align list.decidable_chain' List.decidableChain'
 
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
index efcc6e07d89c4..95ef411284c88 100644
--- a/Mathlib/Data/Multiset/Basic.lean
+++ b/Mathlib/Data/Multiset/Basic.lean
@@ -71,12 +71,10 @@ instance decidableEq [DecidableEq α] : DecidableEq (Multiset α)
 
 /-- defines a size for a multiset by referring to the size of the underlying list -/
 protected
-noncomputable -- Porting note: added
 def sizeOf [SizeOf α] (s : Multiset α) : ℕ :=
   (Quot.liftOn s SizeOf.sizeOf) fun _ _ => Perm.sizeOf_eq_sizeOf
 #align multiset.sizeof Multiset.sizeOf
 
-noncomputable -- Porting note: added
 instance [SizeOf α] : SizeOf (Multiset α) :=
   ⟨Multiset.sizeOf⟩
 
@@ -178,7 +176,6 @@ TODO: should be @[recursor 6], but then the definition of `Multiset.pi` fails wi
 overflow in `whnf`.
 -/
 protected
-noncomputable -- Porting note: added
 def rec (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
     (C_cons_heq :
       ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b)))
@@ -192,7 +189,6 @@ def rec (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
 /-- Companion to `Multiset.rec` with more convenient argument order. -/
 @[elab_as_elim]
 protected
-noncomputable -- Porting note: added
 def recOn (m : Multiset α) (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
     (C_cons_heq :
       ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) :
diff --git a/Mathlib/Data/Multiset/Pi.lean b/Mathlib/Data/Multiset/Pi.lean
index 2a8231d8ab15f..13c9616c30856 100644
--- a/Mathlib/Data/Multiset/Pi.lean
+++ b/Mathlib/Data/Multiset/Pi.lean
@@ -61,9 +61,7 @@ theorem Pi.cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f :
   all_goals simp [*, Pi.cons_same, Pi.cons_ne]
 #align multiset.pi.cons_swap Multiset.Pi.cons_swap
 
---Porting note: Added noncomputable
 /-- `pi m t` constructs the Cartesian product over `t` indexed by `m`. -/
-noncomputable
 def pi (m : Multiset α) (t : ∀ a, Multiset (δ a)) : Multiset (∀ a ∈ m, δ a) :=
   m.recOn {Pi.empty δ}
     (fun a m (p : Multiset (∀ a ∈ m, δ a)) => (t a).bind fun b => p.map <| Pi.cons m a b)
diff --git a/Mathlib/Data/Multiset/Sections.lean b/Mathlib/Data/Multiset/Sections.lean
index 26e865d377f1c..bbdd3e11dec2c 100644
--- a/Mathlib/Data/Multiset/Sections.lean
+++ b/Mathlib/Data/Multiset/Sections.lean
@@ -25,9 +25,7 @@ section Sections
 which can be put in bijection with `s`, so each element is an member of the corresponding multiset.
 -/
 
--- Porting note: `Sections` depends on `recOn` which is noncomputable.
--- This may be removed when `Multiset.recOn` becomes computable.
-noncomputable def Sections (s : Multiset (Multiset α)) : Multiset (Multiset α) :=
+def Sections (s : Multiset (Multiset α)) : Multiset (Multiset α) :=
   Multiset.recOn s {0} (fun s _ c => s.bind fun a => c.map (Multiset.cons a)) fun a₀ a₁ _ pi => by
     simp [map_bind, bind_bind a₀ a₁, cons_swap]
 #align multiset.sections Multiset.Sections
diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean
index d77d2eee06a77..f83dd83882a51 100644
--- a/Mathlib/Data/PNat/Basic.lean
+++ b/Mathlib/Data/PNat/Basic.lean
@@ -321,7 +321,6 @@ def caseStrongInductionOn {p : ℕ+ → Sort _} (a : ℕ+) (hz : p 1)
 /-- An induction principle for `ℕ+`: it takes values in `Sort*`, so it applies also to Types,
 not only to `Prop`. -/
 @[elab_as_elim]
-noncomputable
 def recOn (n : ℕ+) {p : ℕ+ → Sort _} (p1 : p 1) (hp : ∀ n, p n → p (n + 1)) : p n := by
   rcases n with ⟨n, h⟩
   induction' n with n IH
@@ -329,8 +328,6 @@ def recOn (n : ℕ+) {p : ℕ+ → Sort _} (p1 : p 1) (hp : ∀ n, p n → p (n
   · cases' n with n
     · exact p1
     · exact hp _ (IH n.succ_pos)
--- Porting note: added `noncomputable` because of
--- "code generator does not support recursor 'Nat.rec' yet" error.
 #align pnat.rec_on PNat.recOn
 
 @[simp]
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 1e1ca7cde0d52..bd3726006ea6e 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -449,9 +449,8 @@ This function has two arguments: `h_nil` handles the base case on `C nil`,
 and `h_cons` defines the inductive step using `∀ x : α, C w → C (x ::ᵥ w)`.
 
 This can be used as `induction v using Vector.inductionOn`. -/
--- porting notes: requires noncomputable
 @[elab_as_elim]
-noncomputable def inductionOn {C : ∀ {n : ℕ}, Vector α n → Sort _} {n : ℕ} (v : Vector α n)
+def inductionOn {C : ∀ {n : ℕ}, Vector α n → Sort _} {n : ℕ} (v : Vector α n)
     (h_nil : C nil) (h_cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : C v := by
   -- porting notes: removed `generalizing`: already generalized
   induction' n with n ih
@@ -469,9 +468,8 @@ example (v : Vector α n) : True := by induction v using Vector.inductionOn <;>
 variable {β γ : Type _}
 
 /-- Define `C v w` by induction on a pair of vectors `v : Vector α n` and `w : Vector β n`. -/
--- porting notes: requires noncomputable
 @[elab_as_elim]
-noncomputable def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → Sort _}
+def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → Sort _}
     (v : Vector α n) (w : Vector β n)
     (nil : C nil nil) (cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) :
     C v w := by
@@ -490,9 +488,8 @@ noncomputable def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → S
 
 /-- Define `C u v w` by induction on a triplet of vectors
 `u : Vector α n`, `v : Vector β n`, and `w : Vector γ b`. -/
--- porting notes: requires noncomputable
 @[elab_as_elim]
-noncomputable def inductionOn₃ {C : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort _}
+def inductionOn₃ {C : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort _}
     (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C nil nil nil)
     (cons : ∀ {n a b c} {x : Vector α n} {y z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
     C u v w := by
diff --git a/Mathlib/Init/Data/Nat/Basic.lean b/Mathlib/Init/Data/Nat/Basic.lean
index 599bea021d826..f8e01d6bf3bc3 100644
--- a/Mathlib/Init/Data/Nat/Basic.lean
+++ b/Mathlib/Init/Data/Nat/Basic.lean
@@ -8,6 +8,25 @@ import Mathlib.Init.Data.Nat.Notation
 
 namespace Nat
 
+
+section recursor_workarounds
+
+/-- A computable version of `Nat.rec`. Workaround until Lean has native support for this. -/
+def recC.{u} {motive : ℕ → Sort u} (zero : motive zero)
+  (succ : (n : ℕ) → motive n → motive (succ n)) :
+  (t : ℕ) → motive t
+| 0 => zero
+| (n + 1) => succ n (recC zero succ n)
+
+@[csimp]
+theorem rec_eq_recC : @Nat.rec = @Nat.recC := by
+  funext motive zero succ n
+  induction n with
+  | zero => rfl
+  | succ n ih => rw [Nat.recC, ←ih]
+
+end recursor_workarounds
+
 set_option linter.deprecated false
 
 protected theorem bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) :=