bump to nightly-2023-03-25-16

mathlib commit leanprover-community/mathlib@d11893b

Mathbin/Computability/Halting.lean

@@ -324,7 +324,7 @@ theorem head {n : ℕ} : @Partrec' n.succ (@head ℕ n) :=
 #align nat.partrec'.head Nat.Partrec'.head
 
 theorem tail {n f} (hf : @Partrec' n f) : @Partrec' n.succ fun v => f v.tail :=
-  (hf.comp _ fun i => @prim _ _ <| Nat.Primrec'.nth i.succ).of_eq fun v => by
+  (hf.comp _ fun i => @prim _ _ <| Nat.Primrec'.get i.succ).of_eq fun v => by
     simp <;> rw [← of_fn_nth v.tail] <;> congr <;> funext i <;> simp
 #align nat.partrec'.tail Nat.Partrec'.tail
 
@@ -333,7 +333,7 @@ protected theorem bind {n f g} (hf : @Partrec' n f) (hg : @Partrec' (n + 1) g) :
   (@comp n (n + 1) g (fun i => Fin.cases f (fun i v => some (v.get? i)) i) hg fun i =>
         by
         refine' Fin.cases _ (fun i => _) i <;> simp [*]
-        exact prim (Nat.Primrec'.nth _)).of_eq
+        exact prim (Nat.Primrec'.get _)).of_eq
     fun v => by simp [m_of_fn, Part.bind_assoc, pure]
 #align nat.partrec'.bind Nat.Partrec'.bind
 

Mathbin/Computability/Partrec.lean

@@ -491,7 +491,7 @@ theorem to₂ {f : α × β →. σ} (hf : Partrec f) : Partrec₂ fun a b => f
   hf.of_eq fun ⟨a, b⟩ => rfl
 #align partrec.to₂ Partrec.to₂
 
-theorem nat_elim {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g)
+theorem nat_rec {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g)
     (hh : Partrec₂ h) : Partrec fun a => (f a).elim (g a) fun y IH => IH.bind fun i => h a (y, i) :=
   (Nat.Partrec.prec' hf hg hh).of_eq fun n =>
     by
@@ -500,7 +500,7 @@ theorem nat_elim {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ
     rw [IH, bind_map]
     congr ; funext s
     simp [encodek]
-#align partrec.nat_elim Partrec.nat_elim
+#align partrec.nat_elim Partrec.nat_rec
 
 theorem comp {f : β →. σ} {g : α → β} (hf : Partrec f) (hg : Computable g) :
     Partrec fun a => f (g a) :=
@@ -602,20 +602,20 @@ theorem rfindOpt {f : α → ℕ → Option σ} (hf : Computable₂ f) :
   (rfind (Primrec.option_isSome.to_comp.comp hf).Partrec.to₂).bind (of_option hf)
 #align partrec.rfind_opt Partrec.rfindOpt
 
-theorem nat_cases_right {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ} (hf : Computable f)
+theorem nat_casesOn_right {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ} (hf : Computable f)
     (hg : Computable g) (hh : Partrec₂ h) : Partrec fun a => (f a).cases (some (g a)) (h a) :=
-  (nat_elim hf hg (hh.comp fst (pred.comp <| hf.comp fst)).to₂).of_eq fun a =>
+  (nat_rec hf hg (hh.comp fst (pred.comp <| hf.comp fst)).to₂).of_eq fun a =>
     by
     simp; cases f a <;> simp
     refine' ext fun b => ⟨fun H => _, fun H => _⟩
     · rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩
       exact h₂
-    · have : ∀ m, (Nat.elim (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom :=
+    · have : ∀ m, (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom :=
         by
         intro
         induction m <;> simp [*, H.fst]
       exact ⟨⟨this n, H.fst⟩, H.snd⟩
-#align partrec.nat_cases_right Partrec.nat_cases_right
+#align partrec.nat_cases_right Partrec.nat_casesOn_right
 
 theorem bind_decode₂_iff {f : α →. σ} :
     Partrec f ↔ Nat.Partrec fun n => Part.bind (decode₂ α n) fun a => (f a).map encode :=
@@ -672,7 +672,7 @@ theorem bind_decode_iff {f : α → β → Option σ} :
     have :
       Partrec fun a : α × ℕ =>
         (encode (decode β a.2)).cases (some Option.none) fun n => Part.map (f a.1) (decode β n) :=
-      Partrec.nat_cases_right (primrec.encdec.to_comp.comp snd) (const none)
+      Partrec.nat_casesOn_right (primrec.encdec.to_comp.comp snd) (const none)
         ((of_option (computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
     refine' this.of_eq fun a => _
     simp; cases decode β a.2 <;> simp [encodek]⟩
@@ -683,26 +683,26 @@ theorem map_decode_iff {f : α → β → σ} :
   bind_decode_iff.trans option_some_iff
 #align computable.map_decode_iff Computable.map_decode_iff
 
-theorem nat_elim {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ} (hf : Computable f) (hg : Computable g)
+theorem nat_rec {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ} (hf : Computable f) (hg : Computable g)
     (hh : Computable₂ h) : Computable fun a => (f a).elim (g a) fun y IH => h a (y, IH) :=
-  (Partrec.nat_elim hf hg hh.Partrec₂).of_eq fun a => by simp <;> induction f a <;> simp [*]
-#align computable.nat_elim Computable.nat_elim
+  (Partrec.nat_rec hf hg hh.Partrec₂).of_eq fun a => by simp <;> induction f a <;> simp [*]
+#align computable.nat_elim Computable.nat_rec
 
-theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ} (hf : Computable f) (hg : Computable g)
+theorem nat_casesOn {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ} (hf : Computable f) (hg : Computable g)
     (hh : Computable₂ h) : Computable fun a => (f a).cases (g a) (h a) :=
-  nat_elim hf hg (hh.comp fst <| fst.comp snd).to₂
-#align computable.nat_cases Computable.nat_cases
+  nat_rec hf hg (hh.comp fst <| fst.comp snd).to₂
+#align computable.nat_cases Computable.nat_casesOn
 
 theorem cond {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Computable c) (hf : Computable f)
     (hg : Computable g) : Computable fun a => cond (c a) (f a) (g a) :=
-  (nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl
+  (nat_casesOn (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl
 #align computable.cond Computable.cond
 
 theorem option_cases {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Computable o)
     (hf : Computable f) (hg : Computable₂ g) :
     @Computable _ σ _ _ fun a => Option.casesOn (o a) (f a) (g a) :=
   option_some_iff.1 <|
-    (nat_cases (encode_iff.2 ho) (option_some_iff.2 hf) (map_decode_iff.2 hg)).of_eq fun a => by
+    (nat_casesOn (encode_iff.2 ho) (option_some_iff.2 hf) (map_decode_iff.2 hg)).of_eq fun a => by
       cases o a <;> simp [encodek] <;> rfl
 #align computable.option_cases Computable.option_cases
 
@@ -745,7 +745,7 @@ theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ
       (list_get?.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq fun a => by
         simp [List.get?_range (Nat.lt_succ_self a.2)] <;> rfl
   option_some_iff.1 <|
-    (nat_elim snd (const (Option.some []))
+    (nat_rec snd (const (Option.some []))
           (to₂ <|
             option_bind (snd.comp snd) <|
               to₂ <|
@@ -789,8 +789,8 @@ theorem option_cases_right {o : α → Option β} {f : α → σ} {g : α → β
     @Partrec _ σ _ _ fun a => Option.casesOn (o a) (some (f a)) (g a) :=
   have :
     Partrec fun a : α =>
-      Nat.cases (Part.some (f a)) (fun n => Part.bind (decode β n) (g a)) (encode (o a)) :=
-    nat_cases_right (encode_iff.2 ho) hf.Partrec <|
+      Nat.casesOn (Part.some (f a)) (fun n => Part.bind (decode β n) (g a)) (encode (o a)) :=
+    nat_casesOn_right (encode_iff.2 ho) hf.Partrec <|
       ((@Computable.decode β _).comp snd).ofOption.bind (hg.comp (fst.comp fst) snd).to₂
   this.of_eq fun a => by cases' o a with b <;> simp [encodek]
 #align partrec.option_cases_right Partrec.option_cases_right
@@ -866,7 +866,7 @@ theorem fix {f : α →. Sum σ α} (hf : Partrec f) : Partrec (PFun.fix f) :=
   let F : α → ℕ →. Sum σ α := fun a n =>
     n.elim (some (Sum.inr a)) fun y IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f
   have hF : Partrec₂ F :=
-    Partrec.nat_elim snd (sum_inr.comp fst).Partrec
+    Partrec.nat_rec snd (sum_inr.comp fst).Partrec
       (sum_cases_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂
   let p a n := @Part.map _ Bool (fun s => Sum.casesOn s (fun _ => true) fun _ => false) (F a n)
   have hp : Partrec₂ p :=

Mathbin/Computability/PartrecCode.lean

@@ -239,8 +239,8 @@ theorem pair_prim : Primrec₂ pair :=
   Primrec₂.ofNat_iff.2 <|
     Primrec₂.encode_iff.1 <|
       nat_add.comp
-        (nat_bit0.comp <|
-          nat_bit0.comp <|
+        (nat_double.comp <|
+          nat_double.comp <|
             Primrec₂.mkpair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
               (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
         (Primrec₂.const 4)
@@ -250,8 +250,8 @@ theorem comp_prim : Primrec₂ comp :=
   Primrec₂.ofNat_iff.2 <|
     Primrec₂.encode_iff.1 <|
       nat_add.comp
-        (nat_bit0.comp <|
-          nat_bit1.comp <|
+        (nat_double.comp <|
+          nat_double_succ.comp <|
             Primrec₂.mkpair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
               (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
         (Primrec₂.const 4)
@@ -261,8 +261,8 @@ theorem prec_prim : Primrec₂ prec :=
   Primrec₂.ofNat_iff.2 <|
     Primrec₂.encode_iff.1 <|
       nat_add.comp
-        (nat_bit1.comp <|
-          nat_bit0.comp <|
+        (nat_double_succ.comp <|
+          nat_double.comp <|
             Primrec₂.mkpair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
               (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
         (Primrec₂.const 4)
@@ -271,7 +271,9 @@ theorem prec_prim : Primrec₂ prec :=
 theorem rfind_prim : Primrec rfind' :=
   ofNat_iff.2 <|
     encode_iff.1 <|
-      nat_add.comp (nat_bit1.comp <| nat_bit1.comp <| encode_iff.2 <| Primrec.ofNat Code) (const 4)
+      nat_add.comp
+        (nat_double_succ.comp <| nat_double_succ.comp <| encode_iff.2 <| Primrec.ofNat Code)
+        (const 4)
 #align nat.partrec.code.rfind_prim Nat.Partrec.Code.rfind_prim
 
 theorem rec_prim' {α σ} [Primcodable α] [Primcodable σ] {c : α → Code} (hc : Primrec c) {z : α → σ}
@@ -617,7 +619,7 @@ def eval : Code → ℕ →. ℕ
 /-- Helper lemma for the evaluation of `prec` in the base case. -/
 @[simp]
 theorem eval_prec_zero (cf cg : Code) (a : ℕ) : eval (prec cf cg) (mkpair a 0) = eval cf a := by
-  rw [eval, Nat.unpaired, Nat.unpair_mkpair, Nat.elim_zero]
+  rw [eval, Nat.unpaired, Nat.unpair_mkpair, Nat.rec_zero]
 #align nat.partrec.code.eval_prec_zero Nat.Partrec.Code.eval_prec_zero
 
 /-- Helper lemma for the evaluation of `prec` in the recursive case. -/
@@ -626,7 +628,7 @@ theorem eval_prec_succ (cf cg : Code) (a k : ℕ) :
       let ih ← eval (prec cf cg) (mkpair a k)
       eval cg (mkpair a (mkpair k ih)) :=
   by
-  rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_mkpair, Nat.elim_succ]
+  rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_mkpair, Nat.rec_add_one]
   simp
 #align nat.partrec.code.eval_prec_succ Nat.Partrec.Code.eval_prec_succ