diff --git a/Foundation/FirstOrder/Arith/Representation.lean b/Foundation/FirstOrder/Arith/Representation.lean index b10f73b5..03899d06 100644 --- a/Foundation/FirstOrder/Arith/Representation.lean +++ b/Foundation/FirstOrder/Arith/Representation.lean @@ -8,14 +8,14 @@ lemma unit_dom_iff (x : Part Unit) : x.Dom ↔ () ∈ x := by simp [dom_iff_mem, end Part -namespace Mathlib.Mathlib.Vector +namespace Mathlib.List.Vector variable {α : Type*} -lemma cons_get (a : α) (v : Mathlib.Vector α k) : (a ::ᵥ v).get = a :> v.get := by +lemma cons_get (a : α) (v : List.Vector α k) : (a ::ᵥ v).get = a :> v.get := by ext i; cases i using Fin.cases <;> simp -end Mathlib.Mathlib.Vector +end Mathlib.List.Vector open Encodable Denumerable @@ -156,7 +156,7 @@ open Mathlib Encodable Semiterm.Operator.GoedelNumber section -lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Mathlib.Vector ℕ k ↦ t.valm ℕ v.get f) +lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : List.Vector ℕ k ↦ t.valm ℕ v.get f) | #x => by simpa using Primrec.vector_get.comp .id (.const _) | &x => by simpa using Primrec.const _ | Semiterm.func Language.Zero.zero _ => by simpa using Primrec.const 0 @@ -167,32 +167,32 @@ lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Ma simpa [Semiterm.val_func] using Primrec.nat_mul.comp (term_primrec (v 0)) (term_primrec (v 1)) lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hierarchy 𝚺 1 φ) : - RePred fun v : Mathlib.Vector ℕ k ↦ Semiformula.Evalm ℕ v.get ε φ := by + RePred fun v : List.Vector ℕ k ↦ Semiformula.Evalm ℕ v.get ε φ := by apply sigma₁_induction' hp case hVerum => simp case hFalsum => simp case hEQ => intro n t₁ t₂ refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr - <| ⟨fun v : Mathlib.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : List.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ · apply Primrec.to_comp <| Primrec.eq.comp (term_primrec t₁) (term_primrec t₂) · simp case hNEQ => intro n t₁ t₂ refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr - <| ⟨fun v : Mathlib.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : List.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ · apply Primrec.to_comp <| Primrec.not.comp <| Primrec.eq.comp (term_primrec t₁) (term_primrec t₂) · simp case hLT => intro n t₁ t₂ refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr - <| ⟨fun v : Mathlib.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : List.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ · apply Primrec.to_comp <| Primrec.nat_lt.comp (term_primrec t₁) (term_primrec t₂) · simp case hNLT => intro n t₁ t₂ refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr - <| ⟨fun v : Mathlib.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : List.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ · apply Primrec.to_comp <| Primrec.not.comp <| Primrec.nat_lt.comp (term_primrec t₁) (term_primrec t₂) · simp case hAnd => @@ -204,7 +204,7 @@ lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hi case hBall => intro n t φ _ ih rcases RePred.iff'.mp ih with ⟨f, hf, H⟩ - let g : Mathlib.Vector ℕ n →. Unit := fun v ↦ + let g : List.Vector ℕ n →. Unit := fun v ↦ Nat.rec (.some ()) (fun x ih ↦ ih.bind fun _ ↦ f (x ::ᵥ v)) (t.valm ℕ v.get ε) have : Partrec g := Partrec.nat_rec (term_primrec t).to_comp (Computable.const ()) @@ -220,16 +220,16 @@ lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hi constructor · intro h exact ⟨fun x hx ↦ h x (lt_trans hx (by simp)), - (H (k ::ᵥ v)).mp (by simpa [Mathlib.Vector.cons_get] using h k (by simp))⟩ + (H (k ::ᵥ v)).mp (by simpa [List.Vector.cons_get] using h k (by simp))⟩ · rintro ⟨hs, hd⟩ x hx rcases lt_or_eq_of_le (Nat.le_of_lt_succ hx) with (hx | rfl) · exact hs x hx - · simpa [Mathlib.Vector.cons_get] using (H (x ::ᵥ v)).mpr hd + · simpa [List.Vector.cons_get] using (H (x ::ᵥ v)).mpr hd case hEx => intro n φ _ ih rcases RePred.iff'.mp ih with ⟨f, _, _⟩ - have : RePred fun vx : Mathlib.Vector ℕ n × ℕ ↦ Semiformula.Evalm ℕ (vx.2 :> vx.1.get) ε φ := by - simpa [Mathlib.Vector.cons_get] using ih.comp (Primrec.to_comp <| Primrec.vector_cons.comp .snd .fst) + have : RePred fun vx : List.Vector ℕ n × ℕ ↦ Semiformula.Evalm ℕ (vx.2 :> vx.1.get) ε φ := by + simpa [List.Vector.cons_get] using ih.comp (Primrec.to_comp <| Primrec.vector_cons.comp .snd .fst) simpa using this.projection end @@ -313,8 +313,8 @@ private lemma codeAux_sigma_one {k} (c : Nat.ArithPart₁.Code k) : Hierarchy @[simp] lemma natCast_nat (n : ℕ) : Nat.cast n = n := by rfl -private lemma models_codeAux {c : Code k} {f : Mathlib.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : - Semiformula.Evalfm ℕ (y :> v) (codeAux c) ↔ f (Mathlib.Vector.ofFn v) = Part.some y := by +private lemma models_codeAux {c : Code k} {f : List.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : + Semiformula.Evalfm ℕ (y :> v) (codeAux c) ↔ f (List.Vector.ofFn v) = Part.some y := by induction hc generalizing y <;> simp [code, codeAux, models_iff] case zero => have : (0 : Part ℕ) = Part.some 0 := rfl @@ -334,33 +334,33 @@ private lemma models_codeAux {c : Code k} {f : Mathlib.Vector ℕ k →. ℕ} (h simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons'] constructor · rintro ⟨e, hf, hg⟩ - have hf : f (Mathlib.Vector.ofFn e) = Part.some y := (ihf _ _).mp hf - have hg : ∀ i, g i (Mathlib.Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i) + have hf : f (List.Vector.ofFn e) = Part.some y := (ihf _ _).mp hf + have hg : ∀ i, g i (List.Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i) simp [hg, hf] · intro h - have : ∃ w, (∀ i, Mathlib.Vector.get w i ∈ g i (Mathlib.Vector.ofFn v)) ∧ y ∈ f w := by + have : ∃ w, (∀ i, List.Vector.get w i ∈ g i (List.Vector.ofFn v)) ∧ y ∈ f w := by simpa using Part.eq_some_iff.mp h rcases this with ⟨w, hw, hy⟩ exact ⟨w.get, (ihf y w.get).mpr (by simpa[Part.eq_some_iff] using hy), fun i => (ihg i (w.get i) v).mpr (by simpa[Part.eq_some_iff] using hw i)⟩ case rfind c f _ ihf => - simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Mathlib.Vector.ofFn_vecCons] + simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons', ihf, List.Vector.ofFn_vecCons] constructor · rintro ⟨hy, h⟩; simp [Part.eq_some_iff] exact ⟨by simpa using hy, by intro z hz; exact Nat.not_eq_zero_of_lt (h z hz)⟩ · intro h; simpa [pos_iff_ne_zero] using Nat.mem_rfind.mp (Part.eq_some_iff.mp h) -lemma models_code {c : Code k} {f : Mathlib.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : - Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by +lemma models_code {c : Code k} {f : List.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : + Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (List.Vector.ofFn v) := by simpa[code, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp_def, Matrix.comp_vecCons', ←Part.eq_some_iff] using models_codeAux hc y v -noncomputable def codeOfPartrec' {k} (f : Mathlib.Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1) := - code <| Classical.epsilon (fun c ↦ ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v)) +noncomputable def codeOfPartrec' {k} (f : List.Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1) := + code <| Classical.epsilon (fun c ↦ ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (List.Vector.ofFn v)) -lemma codeOfPartrec'_spec {k} {f : Mathlib.Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} : - ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by - have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by +lemma codeOfPartrec'_spec {k} {f : List.Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} : + ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (List.Vector.ofFn v) := by + have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (List.Vector.ofFn v) := by rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩ exact ⟨c, models_code hc⟩ exact Classical.epsilon_spec this y v @@ -375,7 +375,7 @@ lemma codeOfRePred_spec {p : ℕ → Prop} (hp : RePred p) {x : ℕ} : ℕ ⊧/![x] (codeOfRePred p) ↔ p x := by let f : ℕ →. Unit := fun a ↦ Part.assert (p a) fun _ ↦ Part.some () suffices ℕ ⊧/![x] ((codeOfPartrec' fun v ↦ Part.map (fun _ ↦ 0) (f (v.get 0)))/[‘0’, #0]) ↔ p x from this - have : Partrec fun v : Mathlib.Vector ℕ 1 ↦ (f (v.get 0)).map fun _ ↦ 0 := by + have : Partrec fun v : List.Vector ℕ 1 ↦ (f (v.get 0)).map fun _ ↦ 0 := by refine Partrec.map (Partrec.comp hp (Primrec.to_comp <| Primrec.vector_get.comp .id (.const 0))) (Computable.const 0).to₂ simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton] apply (codeOfPartrec'_spec (Nat.Partrec'.of_part this) (v := ![x]) (y := 0)).trans (by simp [f]) diff --git a/Foundation/Vorspiel/Arith.lean b/Foundation/Vorspiel/Arith.lean index 2f21143d..52295334 100644 --- a/Foundation/Vorspiel/Arith.lean +++ b/Foundation/Vorspiel/Arith.lean @@ -4,7 +4,7 @@ import Mathlib.Data.Nat.ModEq import Mathlib.Data.List.FinRange import Mathlib.Logic.Godel.GodelBetaFunction -open Mathlib Mathlib.Vector Part +open Mathlib List.Vector Part namespace Nat @@ -75,20 +75,20 @@ lemma ball_pos_iff_eq_one {φ : ℕ → ℕ} {n : ℕ} : ball n φ = 1 ↔ 0 < b · intro h; simpa using pos_of_eq_one h · intro h; simpa[and_eq_one] using h -inductive ArithPart₁ : ∀ {n}, (Mathlib.Vector ℕ n →. ℕ) → Prop +inductive ArithPart₁ : ∀ {n}, (List.Vector ℕ n →. ℕ) → Prop | zero {n} : @ArithPart₁ n (fun _ => 0) | one {n} : @ArithPart₁ n (fun _ => 1) - | add {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i + v.get j : Mathlib.Vector ℕ n → ℕ) - | mul {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i * v.get j : Mathlib.Vector ℕ n → ℕ) - | proj {n} (i : Fin n) : @ArithPart₁ n (fun v => v.get i : Mathlib.Vector ℕ n → ℕ) - | equal {n} (i j : Fin n) : @ArithPart₁ n (fun v => isEqNat (v.get i) (v.get j) : Mathlib.Vector ℕ n → ℕ) - | lt {n} (i j : Fin n) : @ArithPart₁ n (fun v => isLtNat (v.get i) (v.get j) : Mathlib.Vector ℕ n → ℕ) - | comp {m n f} (g : Fin n → Mathlib.Vector ℕ m →. ℕ) : - ArithPart₁ f → (∀ i, ArithPart₁ (g i)) → ArithPart₁ fun v => (Mathlib.Vector.mOfFn fun i => g i v) >>= f - | rfind {n} {f : Mathlib.Vector ℕ (n + 1) → ℕ} : + | add {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i + v.get j : List.Vector ℕ n → ℕ) + | mul {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i * v.get j : List.Vector ℕ n → ℕ) + | proj {n} (i : Fin n) : @ArithPart₁ n (fun v => v.get i : List.Vector ℕ n → ℕ) + | equal {n} (i j : Fin n) : @ArithPart₁ n (fun v => isEqNat (v.get i) (v.get j) : List.Vector ℕ n → ℕ) + | lt {n} (i j : Fin n) : @ArithPart₁ n (fun v => isLtNat (v.get i) (v.get j) : List.Vector ℕ n → ℕ) + | comp {m n f} (g : Fin n → List.Vector ℕ m →. ℕ) : + ArithPart₁ f → (∀ i, ArithPart₁ (g i)) → ArithPart₁ fun v => (List.Vector.mOfFn fun i => g i v) >>= f + | rfind {n} {f : List.Vector ℕ (n + 1) → ℕ} : ArithPart₁ (n := n + 1) f → ArithPart₁ (fun v => rfind fun n => Part.some (f (n ::ᵥ v) = 0)) -def Arith₁ (f : Mathlib.Vector ℕ n → ℕ) := ArithPart₁ (n := n) f +def Arith₁ (f : List.Vector ℕ n → ℕ) := ArithPart₁ (n := n) f end Nat @@ -96,7 +96,7 @@ namespace Nat.ArithPart₁ open Primrec -lemma to_partrec' {n} {f : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partrec' f := by +lemma to_partrec' {n} {f : List.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partrec' f := by induction hf case zero => exact Partrec'.of_part (Partrec.const' 0) case one => exact Partrec'.of_part (Partrec.const' 1) @@ -112,7 +112,7 @@ lemma to_partrec' {n} {f : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) exact Partrec'.of_part (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)).to_comp.partrec case equal n i j => - have : Primrec (fun (v : Mathlib.Vector ℕ n) => if v.get i = v.get j then 1 else 0) := + have : Primrec (fun (v : List.Vector ℕ n) => if v.get i = v.get j then 1 else 0) := Primrec.ite (Primrec.eq.comp (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)) @@ -121,7 +121,7 @@ lemma to_partrec' {n} {f : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (_root_.Primrec.const 0) exact Partrec'.of_part this.to_comp.partrec case lt n i j => - have : Primrec (fun (v : Mathlib.Vector ℕ n) => if v.get i < v.get j then 1 else 0) := + have : Primrec (fun (v : List.Vector ℕ n) => if v.get i < v.get j then 1 else 0) := Primrec.ite (Primrec.nat_lt.comp (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)) @@ -134,22 +134,22 @@ lemma to_partrec' {n} {f : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) case rfind f _ hf => exact Partrec'.rfind hf -lemma of_eq {n} {f g : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (H : ∀ i, f i = g i) : ArithPart₁ g := +lemma of_eq {n} {f g : List.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (H : ∀ i, f i = g i) : ArithPart₁ g := (funext H : f = g) ▸ hf -lemma bind (f : Mathlib.Vector ℕ n → ℕ →. ℕ) (hf : @ArithPart₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : +lemma bind (f : List.Vector ℕ n → ℕ →. ℕ) (hf : @ArithPart₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : @ArithPart₁ n fun v => (g v).bind (f v) := (hf.comp (g :> fun i v => v.get i) (fun i => by cases i using Fin.cases <;> simp[*]; exact proj _)).of_eq (by intro v; simp rcases Part.eq_none_or_eq_some (g v) with (hgv | ⟨x, hgv⟩) - · simp[hgv, Mathlib.Vector.mOfFn] + · simp[hgv, List.Vector.mOfFn] · simp[hgv, Matrix.comp_vecCons'] - have : Mathlib.Vector.mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (Mathlib.Vector.ofFn (x :> fun j => v.get j)) := by - rw[←Vector.mOfFn_pure]; apply congr_arg + have : List.Vector.mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (List.Vector.ofFn (x :> fun j => v.get j)) := by + rw[←List.Vector.mOfFn_pure]; apply congr_arg funext i; cases i using Fin.cases <;> simp[hgv] simp[this]) -lemma map (f : Mathlib.Vector ℕ n → ℕ → ℕ) (hf : @Arith₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : +lemma map (f : List.Vector ℕ n → ℕ → ℕ) (hf : @Arith₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : @ArithPart₁ n fun v => (g v).map (f v) := (bind (Part.some $ f · ·) (hf.of_eq <| by simp) hg).of_eq <| by intro v; rcases Part.eq_none_or_eq_some (g v) with (_ | ⟨x, _⟩) <;> simp[*] @@ -162,11 +162,11 @@ lemma comp₂ (f : ℕ → ℕ →. ℕ) (hf : @ArithPart₁ 2 fun v => f (v.get @ArithPart₁ n fun v => f (g v) (h v) := (hf.comp ![g, h] (fun i => i.cases hg (fun i => by simpa using hh))).of_eq (by intro i - have : (fun j => (![↑g, h] : Fin 2 → Mathlib.Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by + have : (fun j => (![↑g, h] : Fin 2 → List.Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by funext j; cases j using Fin.cases <;> simp[Fin.eq_zero] simp[Matrix.comp_vecCons']; simp[this] ) -lemma rfind' {n} {f : ℕ → Mathlib.Vector ℕ n → ℕ} (h : Arith₁ (n := n + 1) (fun v => f v.head v.tail)) : +lemma rfind' {n} {f : ℕ → List.Vector ℕ n → ℕ} (h : Arith₁ (n := n + 1) (fun v => f v.head v.tail)) : ArithPart₁ (fun v => Nat.rfind fun n => Part.some (f n v = 0)) := rfind h lemma rfind'₁ {n} (i : Fin n) {f : ℕ → ℕ → ℕ} (h : Arith₁ (n := 2) (fun v => f (v.get 0) (v.get 1))) : @@ -177,12 +177,12 @@ end Nat.ArithPart₁ namespace Nat.Arith₁ -lemma of_eq {n} {f g : Mathlib.Vector ℕ n → ℕ} (hf : Arith₁ f) (H : ∀ i, f i = g i) : Arith₁ g := +lemma of_eq {n} {f g : List.Vector ℕ n → ℕ} (hf : Arith₁ f) (H : ∀ i, f i = g i) : Arith₁ g := (funext H : f = g) ▸ hf -lemma zero {n} : @Arith₁ n (fun _ => 0 : Mathlib.Vector ℕ n → ℕ) := Nat.ArithPart₁.zero +lemma zero {n} : @Arith₁ n (fun _ => 0 : List.Vector ℕ n → ℕ) := Nat.ArithPart₁.zero -lemma one {n} : @Arith₁ n (fun _ => 1 : Mathlib.Vector ℕ n → ℕ) := Nat.ArithPart₁.one +lemma one {n} : @Arith₁ n (fun _ => 1 : List.Vector ℕ n → ℕ) := Nat.ArithPart₁.one lemma add {n} (i j : Fin n) : @Arith₁ n (fun v => v.get i + v.get j) := Nat.ArithPart₁.add i j @@ -196,11 +196,11 @@ lemma equal {n} (i j : Fin n) : @Arith₁ n (fun v => isEqNat (v.get i) (v.get j lemma lt {n} (i j : Fin n) : @Arith₁ n (fun v => isLtNat (v.get i) (v.get j)) := Nat.ArithPart₁.lt i j -lemma comp {m n f} (g : Fin n → Mathlib.Vector ℕ m → ℕ) (hf : Arith₁ f) (hg : ∀ i, Arith₁ (g i)) : - Arith₁ fun v => f (Mathlib.Vector.ofFn fun i => g i v) := - (Nat.ArithPart₁.comp (fun i => g i : Fin n → Mathlib.Vector ℕ m →. ℕ) hf hg).of_eq <| by simp +lemma comp {m n f} (g : Fin n → List.Vector ℕ m → ℕ) (hf : Arith₁ f) (hg : ∀ i, Arith₁ (g i)) : + Arith₁ fun v => f (List.Vector.ofFn fun i => g i v) := + (Nat.ArithPart₁.comp (fun i => g i : Fin n → List.Vector ℕ m →. ℕ) hf hg).of_eq <| by simp -def Vec {n m} (f : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m) : Prop := ∀ i, Arith₁ fun v => (f v).get i +def Vec {n m} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop := ∀ i, Arith₁ fun v => (f v).get i protected lemma nil {n} : @Vec n 0 (fun _ => nil) := fun i => i.elim0 @@ -239,7 +239,7 @@ lemma or {n} (i j : Fin n) : Arith₁ (fun v => or (v.get i) (v.get j)) := (lt 0 lemma le {n} (i j : Fin n) : @Arith₁ n (fun v => isLeNat (v.get i) (v.get j)) := ((or 0 1).comp₂ _ (lt i j) (equal i j)).of_eq <| by simp[Nat.or_eq, Nat.le_iff_lt_or_eq, isLeNat] -lemma if_pos {n} {f g h : Mathlib.Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : Arith₁ g) (hh : Arith₁ h) : +lemma if_pos {n} {f g h : List.Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : Arith₁ g) (hh : Arith₁ h) : Arith₁ (fun v => if 0 < f v then g v else h v) := by have : Arith₁ (fun v => (f v).pos * (g v) + (f v).inv * (h v)) := (add 0 1).comp₂ _ @@ -248,13 +248,13 @@ lemma if_pos {n} {f g h : Mathlib.Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : exact this.of_eq <| by intro i; by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff] -lemma to_arith₁ {f : Mathlib.Vector ℕ n → ℕ} (h : Arith₁ f) : @ArithPart₁ n (fun x => f x) := h +lemma to_arith₁ {f : List.Vector ℕ n → ℕ} (h : Arith₁ f) : @ArithPart₁ n (fun x => f x) := h end Nat.Arith₁ namespace Nat.ArithPart₁ -lemma rfindPos {n} {f : Mathlib.Vector ℕ (n + 1) → ℕ} (h : Arith₁ f) : +lemma rfindPos {n} {f : List.Vector ℕ (n + 1) → ℕ} (h : Arith₁ f) : ArithPart₁ (fun v => Nat.rfind fun n => Part.some (0 < f (n ::ᵥ v))) := (ArithPart₁.rfind ((Arith₁.inv 0).comp₁ _ ((Arith₁.lt 0 1).comp₂ _ zero h))).of_eq <| by simp @@ -270,10 +270,10 @@ lemma inv_fun {n} (i : Fin n) (f : ℕ → ℕ) (hf : Arith₁ (n := 1) (fun v = ((Arith₁.lt 0 1).comp₂ _ (proj 1) (hf.comp₁ _ $ (Arith₁.succ 0).comp₁ _ $ proj 0)) exact this.of_eq <| by intro v; simp [F] -lemma implicit_fun {n} (i : Fin n) (f : Mathlib.Vector ℕ n → ℕ → ℕ) +lemma implicit_fun {n} (i : Fin n) (f : List.Vector ℕ n → ℕ → ℕ) (hf : Arith₁ (n := n + 1) (fun v => f v.tail v.head)) : ArithPart₁ (fun v => Nat.rfind (fun x => Part.some (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))) := by - let F : Mathlib.Vector ℕ (n + 1) → ℕ := + let F : List.Vector ℕ (n + 1) → ℕ := fun v => (isLeNat (f v.tail v.head) (v.get i.succ)).and (isLtNat (v.get i.succ) (f v.tail (v.head + 1))) have : Arith₁ F := (Arith₁.and 0 1).comp₂ _ @@ -294,14 +294,14 @@ protected lemma sqrt {n} (i : Fin n) : Arith₁ (fun v => sqrt (v.get i)) := by intro v; simp only [Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind, mem_some_iff] constructor · symm; simp; constructor - · exact sqrt_le (Mathlib.Vector.get v i) - · exact lt_succ_sqrt (Mathlib.Vector.get v i) + · exact sqrt_le (List.Vector.get v i) + · exact lt_succ_sqrt (List.Vector.get v i) · intro m hm; symm simp only [Bool.and_eq_false_eq_eq_false_or_eq_false, decide_eq_false_iff_not, not_le, not_lt] right; exact Iff.mp le_sqrt hm lemma sub {n} (i j : Fin n) : Arith₁ (fun v => v.get i - v.get j) := by - let F : Mathlib.Vector ℕ (n + 1) → ℕ := fun v => + let F : List.Vector ℕ (n + 1) → ℕ := fun v => (isEqNat (v.head + v.get j.succ) (v.get i.succ)).or ((isLtNat (v.get i.succ) (v.get j.succ)).and (isEqNat v.head 0)) have : Arith₁ F := @@ -388,11 +388,11 @@ lemma dvd (i j : Fin n) : Arith₁ (fun v => isDvdNat (v.get i) (v.get j)) := by · simp only [hv, ↓reduceIte] exact ⟨v.get j + 1, ⟨by symm; simp, by intro m hm; symm; simp[lt_succ.mp hm]; intro A - have : v.get i ∣ v.get j := by rw[←A]; exact Nat.dvd_mul_left (Mathlib.Vector.get v i) m + have : v.get i ∣ v.get j := by rw[←A]; exact Nat.dvd_mul_left (List.Vector.get v i) m contradiction⟩, by simp [isLeNat]⟩ lemma rem (i j : Fin n) : Arith₁ (fun v => v.get i % v.get j) := by - let F : Mathlib.Vector ℕ (n + 1) → ℕ := fun v => isDvdNat (v.get j.succ) (v.get i.succ - v.head) + let F : List.Vector ℕ (n + 1) → ℕ := fun v => isDvdNat (v.get j.succ) (v.get i.succ - v.head) have : Arith₁ F := (dvd 0 1).comp₂ _ (proj j.succ) ((sub 0 1).comp₂ _ (proj i.succ) head) exact (ArithPart₁.rfindPos this).of_eq <| by @@ -418,9 +418,9 @@ lemma beta (i j : Fin n) : Arith₁ (fun v => Nat.beta (v.get i) (v.get j)) := (rem 0 1).comp₂ _ ((unpair₁ 0).comp₁ (·.unpair.1) (proj i)) ((succ 0).comp₁ _ $ (mul 0 1).comp₂ _ (succ j) ((unpair₂ 0).comp₁ (·.unpair.2) (proj i))) -lemma ball {φ : Mathlib.Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => φ v.tail v.head)) (i) : +lemma ball {φ : List.Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => φ v.tail v.head)) (i) : Arith₁ (fun v => ball (v.get i) (φ v)) := by - let F : Mathlib.Vector ℕ (n + 1) → ℕ := fun v => (φ v.tail v.head).inv.or (isLeNat (v.get i.succ) v.head) + let F : List.Vector ℕ (n + 1) → ℕ := fun v => (φ v.tail v.head).inv.or (isLeNat (v.get i.succ) v.head) have hF : Arith₁ F := (or 0 1).comp₂ _ ((inv 0).comp₁ _ hp) ((le 0 1).comp₂ _ (proj i.succ) head) have : @Arith₁ (n + 1) (fun v => isEqNat v.head (v.get i.succ)) := (equal 0 1).comp₂ _ head (proj i.succ) @@ -434,7 +434,7 @@ lemma ball {φ : Mathlib.Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) ( · exact ⟨v.get i, ⟨by symm; simp, by intro m hm; symm; simp[hm]; exact Nat.not_eq_zero_of_lt (H m hm)⟩, by { simp[isEqNat]; symm; exact ball_pos_iff_eq_one.mpr (by simpa) }⟩ - · have : ∃ x < Mathlib.Vector.get v i, φ v x = 0 ∧ ∀ y < x, φ v y ≠ 0 := by + · have : ∃ x < List.Vector.get v i, φ v x = 0 ∧ ∀ y < x, φ v y ≠ 0 := by simp at H; rcases least_number _ H with ⟨x, hx, hxl⟩ exact ⟨x, hx.1, hx.2, by intro y hy; have : y < v.get i → φ v y ≠ 0 := by simpa using hxl y hy @@ -444,27 +444,27 @@ lemma ball {φ : Mathlib.Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) ( have : isEqNat x (v.get i) = 0 := by simp[isEqNat, imp_false]; exact ne_of_lt hx simp[this]; symm; simp; exact ⟨x, hx, hpx⟩⟩ -def recSequence (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) : List ℕ := +def recSequence (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) : List ℕ := List.ofFn fun i : Fin (z + 1) => Nat.recOn i (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) -lemma beta_unbeta_recSequence_eq (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) +lemma beta_unbeta_recSequence_eq (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) (m : ℕ) (hm : m < z + 1) : Nat.beta (unbeta (recSequence f g z v)) m = m.rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) := by have : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, _⟩ := Nat.beta_unbeta_coe (recSequence f g z v) ⟨m, by simp[recSequence, hm]⟩ rw [this]; simp [List.get_ofFn, recSequence, -List.get_eq_getElem] -lemma beta_unbeta_recSequence_zero (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) : +lemma beta_unbeta_recSequence_zero (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) : Nat.beta (unbeta (recSequence f g z v)) 0 = f v := by simpa using beta_unbeta_recSequence_eq f g z v 0 (inv_iff_ne_zero.mp rfl) -lemma beta_unbeta_recSequence_succ (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) +lemma beta_unbeta_recSequence_succ (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) {m : ℕ} (hm : m < z) : Nat.beta (unbeta (recSequence f g z v)) (m + 1) = g (m ::ᵥ Nat.beta (unbeta (recSequence f g z v)) m ::ᵥ v) := by rw [beta_unbeta_recSequence_eq f g z v m (Nat.lt_add_right 1 hm), beta_unbeta_recSequence_eq f g z v (m + 1) (Nat.add_lt_add_right hm 1)] -lemma beta_eq_rec (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) {z : ℕ} {v} +lemma beta_eq_rec (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) {z : ℕ} {v} (h0 : z.beta 0 = f v) (hs : ∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) : z.beta m = m.rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) := by induction' m with m ih <;> simp[h0] @@ -472,7 +472,7 @@ lemma beta_eq_rec (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n lemma prec {n f g} (hf : @Arith₁ n f) (hg : @Arith₁ (n + 2) g) : @Arith₁ (n + 1) (fun v => v.head.rec (f v.tail) fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) := by - let F : Mathlib.Vector ℕ (n + 2) → ℕ := fun v => + let F : List.Vector ℕ (n + 2) → ℕ := fun v => (isEqNat (Nat.beta v.head 0) (f v.tail.tail)).and (Nat.ball v.tail.head $ fun i => isEqNat (Nat.beta v.head (i + 1)) (g (i ::ᵥ Nat.beta v.head i ::ᵥ v.tail.tail))) have hp : @Arith₁ (n + 3) (fun v => @@ -485,9 +485,9 @@ lemma prec {n f g} (hf : @Arith₁ n f) (hg : @Arith₁ (n + 2) g) : ((equal 0 1).comp₂ _ ((beta 0 1).comp₂ _ head zero) hf.tail.tail) ((@ball (n + 2) (fun v i => isEqNat (Nat.beta v.head (i + 1)) (g (i ::ᵥ Nat.beta v.head i ::ᵥ v.tail.tail))) hp 1).of_eq $ by - simp[Mathlib.Vector.get_one]) + simp[List.Vector.get_one]) have : @Arith₁ (n + 2) (fun v => Nat.beta v.head v.tail.head) := - (beta 0 1).of_eq (by simp [Mathlib.Vector.get_one]) + (beta 0 1).of_eq (by simp [List.Vector.get_one]) exact (ArithPart₁.map (fun v x => Nat.beta x v.head) this (ArithPart₁.rfindPos hF)).of_eq <| by intro v simp only [add_succ_sub_one, head_cons, tail_cons, and_pos_iff, isEqNat_pos_iff, @@ -503,7 +503,7 @@ lemma prec {n f g} (hf : @Arith₁ n f) (hg : @Arith₁ (n + 2) g) : beta_unbeta_recSequence_zero f g v.head v.tail, fun i hi => beta_unbeta_recSequence_succ f g v.head v.tail hi⟩ -lemma of_primrec {f : Mathlib.Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ f := by +lemma of_primrec {f : List.Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ f := by induction hf case zero => exact zero case succ => exact (@succ 1 0).of_eq (by simp) @@ -511,7 +511,7 @@ lemma of_primrec {f : Mathlib.Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ case comp f g _ _ hf hg => exact hf.comp _ hg case prec f g _ _ hf hg => exact hf.prec hg -lemma _root_.Nat.ArithPart₁.of_partrec {f : Mathlib.Vector ℕ n →. ℕ} (hf : Partrec' f) : ArithPart₁ f := by +lemma _root_.Nat.ArithPart₁.of_partrec {f : List.Vector ℕ n →. ℕ} (hf : Partrec' f) : ArithPart₁ f := by induction hf case prim f hf => exact of_primrec hf case comp f g _ _ hf hg => exact hf.comp _ hg @@ -534,7 +534,7 @@ inductive Code : ℕ → Type instance (k) : Inhabited (Code k) := ⟨Code.zero k⟩ -inductive Code.eval : {n : ℕ} → Code n → (Mathlib.Vector ℕ n →. ℕ) → Prop +inductive Code.eval : {n : ℕ} → Code n → (List.Vector ℕ n →. ℕ) → Prop | zero {n} : Code.eval (Code.zero n) (fun _ => 0) | one {n} : Code.eval (Code.one n) (fun _ => 1) | add {n} (i j : Fin n) : Code.eval (Code.add i j) (fun v => ↑(v.get i + v.get j)) @@ -542,13 +542,13 @@ inductive Code.eval : {n : ℕ} → Code n → (Mathlib.Vector ℕ n →. ℕ) | proj {n} (i : Fin n) : Code.eval (Code.proj i) (fun v => v.get i) | equal {n} (i j : Fin n) : Code.eval (Code.equal i j) (fun v => isEqNat (v.get i) (v.get j)) | lt {n} (i j : Fin n) : Code.eval (Code.lt i j) (fun v => isLtNat (v.get i) (v.get j)) - | comp {m n} (c : Code n) (d : Fin n → Code m) (f : Mathlib.Vector ℕ n →. ℕ) (g : Fin n → (Mathlib.Vector ℕ m →. ℕ)) : + | comp {m n} (c : Code n) (d : Fin n → Code m) (f : List.Vector ℕ n →. ℕ) (g : Fin n → (List.Vector ℕ m →. ℕ)) : Code.eval c f → (∀ i, Code.eval (d i) (g i)) → - Code.eval (c.comp d) (fun v => (Mathlib.Vector.mOfFn fun i => g i v) >>= f) - | rfind {n} (c : Code (n + 1)) (f : Mathlib.Vector ℕ (n + 1) → ℕ) : + Code.eval (c.comp d) (fun v => (List.Vector.mOfFn fun i => g i v) >>= f) + | rfind {n} (c : Code (n + 1)) (f : List.Vector ℕ (n + 1) → ℕ) : Code.eval c f → Code.eval c.rfind (fun v => Nat.rfind fun n => Part.some (f (n ::ᵥ v) = 0)) -lemma exists_code : ∀ {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ}, ArithPart₁ f → ∃ c : Code n, c.eval f +lemma exists_code : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, ArithPart₁ f → ∃ c : Code n, c.eval f | n, _, ArithPart₁.zero => ⟨Code.zero n, Code.eval.zero⟩ | n, _, ArithPart₁.one => ⟨Code.one n, Code.eval.one⟩ | _, _, ArithPart₁.add i j => ⟨Code.add i j, Code.eval.add i j⟩ diff --git a/Foundation/Vorspiel/Vorspiel.lean b/Foundation/Vorspiel/Vorspiel.lean index 3549f5b9..d285dc22 100644 --- a/Foundation/Vorspiel/Vorspiel.lean +++ b/Foundation/Vorspiel/Vorspiel.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Vector.Basic import Mathlib.Data.Fin.Basic import Mathlib.Data.Fin.VecNotation import Mathlib.Data.Fintype.Basic @@ -706,11 +707,11 @@ lemma induction_with_singleton end List -namespace Mathlib.Vector +namespace List.Vector variable {α : Type*} -lemma get_mk_eq_get {n} (l : List α) (h : l.length = n) (i : Fin n) : get (⟨l, h⟩ : Vector α n) i = l.get (i.cast h.symm) := rfl +lemma get_mk_eq_get {n} (l : List α) (h : l.length = n) (i : Fin n) : List.Vector.get (⟨l, h⟩ : List.Vector α n) i = l.get (i.cast h.symm) := rfl lemma get_one {α : Type*} {n} (v : Vector α (n + 2)) : v.get 1 = v.tail.head := by rw[←Vector.get_zero, Vector.get_tail_succ]; rfl @@ -719,7 +720,7 @@ lemma ofFn_vecCons (a : α) (v : Fin n → α) : ofFn (a :> v) = a ::ᵥ ofFn v := by ext i; cases i using Fin.cases <;> simp -end Mathlib.Vector +end List.Vector namespace Finset @@ -775,11 +776,11 @@ end Denumerable namespace Part -@[simp] lemma mem_vector_mOfFn : ∀ {n : ℕ} {w : Mathlib.Vector α n} {v : Fin n →. α}, - w ∈ Mathlib.Vector.mOfFn v ↔ ∀ i, w.get i ∈ v i - | 0, _, _ => by simp[Mathlib.Vector.mOfFn, Mathlib.Vector.eq_nil] +@[simp] lemma mem_vector_mOfFn : ∀ {n : ℕ} {w : List.Vector α n} {v : Fin n →. α}, + w ∈ List.Vector.mOfFn v ↔ ∀ i, w.get i ∈ v i + | 0, _, _ => by simp[List.Vector.mOfFn, List.Vector.eq_nil] | n + 1, w, v => by - simp[Mathlib.Vector.mOfFn, @mem_vector_mOfFn _ n] + simp[List.Vector.mOfFn, @mem_vector_mOfFn _ n] exact ⟨by rintro ⟨a, ha, v, hv, rfl⟩ i; cases i using Fin.cases <;> simp[ha, hv], by intro h; exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩⟩ diff --git a/lake-manifest.json b/lake-manifest.json index a3f981f4..9e44fd95 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "af60d5dfe21be6d33cc1592aec1b4a598efdd023", + "rev": "e731cb89e5ac274330026d006b1b067d8e96a00a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", + "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",