From 975c36bc7b0e691569a56425fe5bfc61bfc8164a Mon Sep 17 00:00:00 2001 From: palalansouki Date: Thu, 12 Dec 2024 18:36:23 +0900 Subject: [PATCH] update --- .../FirstOrder/Arith/Representation.lean | 56 ++++----- Foundation/IntFO/Translation.lean | 4 +- Foundation/IntProp/Dialectica/Basic.lean | 24 ++-- Foundation/Vorspiel/Arith.lean | 114 +++++++++--------- lake-manifest.json | 84 ++++++------- lean-toolchain | 2 +- 6 files changed, 142 insertions(+), 142 deletions(-) diff --git a/Foundation/FirstOrder/Arith/Representation.lean b/Foundation/FirstOrder/Arith/Representation.lean index c64bb1f8..b10f73b5 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.Vector +namespace Mathlib.Mathlib.Vector variable {α : Type*} -lemma cons_get (a : α) (v : Vector α k) : (a ::ᵥ v).get = a :> v.get := by +lemma cons_get (a : α) (v : Mathlib.Vector α k) : (a ::ᵥ v).get = a :> v.get := by ext i; cases i using Fin.cases <;> simp -end Mathlib.Vector +end Mathlib.Mathlib.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 : Vector ℕ k ↦ t.valm ℕ v.get f) +lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Mathlib.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 : Ve 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 : Vector ℕ k ↦ Semiformula.Evalm ℕ v.get ε φ := by + RePred fun v : Mathlib.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 : Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : Mathlib.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 : Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : Mathlib.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 : Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : Mathlib.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 : Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩ + <| ⟨fun v : Mathlib.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 : Vector ℕ n →. Unit := fun v ↦ + let g : Mathlib.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 [Vector.cons_get] using h k (by simp))⟩ + (H (k ::ᵥ v)).mp (by simpa [Mathlib.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 [Vector.cons_get] using (H (x ::ᵥ v)).mpr hd + · simpa [Mathlib.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 : Vector ℕ n × ℕ ↦ Semiformula.Evalm ℕ (vx.2 :> vx.1.get) ε φ := by - simpa [Vector.cons_get] using ih.comp (Primrec.to_comp <| Primrec.vector_cons.comp .snd .fst) + 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) 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 : Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : - Semiformula.Evalfm ℕ (y :> v) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y := by +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 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 : Vector ℕ k →. ℕ} (hc : c.ev simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons'] constructor · rintro ⟨e, hf, hg⟩ - have hf : f (Vector.ofFn e) = Part.some y := (ihf _ _).mp hf - have hg : ∀ i, g i (Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i) + 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) simp [hg, hf] · intro h - have : ∃ w, (∀ i, Vector.get w i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w := by + have : ∃ w, (∀ i, Mathlib.Vector.get w i ∈ g i (Mathlib.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, Vector.ofFn_vecCons] + simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Mathlib.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 : Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : - Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by +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 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 : Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1) := - code <| Classical.epsilon (fun c ↦ ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn 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)) -lemma codeOfPartrec'_spec {k} {f : Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} : - ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (Vector.ofFn v) := by - have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by +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 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 : Vector ℕ 1 ↦ (f (v.get 0)).map fun _ ↦ 0 := by + have : Partrec fun v : Mathlib.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/IntFO/Translation.lean b/Foundation/IntFO/Translation.lean index a93042b5..c60cacd9 100644 --- a/Foundation/IntFO/Translation.lean +++ b/Foundation/IntFO/Translation.lean @@ -72,8 +72,8 @@ open Rewriting System System.FiniteContext HilbertProofᵢ noncomputable def negDoubleNegation : (φ : SyntacticFormula L) → 𝐌𝐢𝐧¹ ⊢ ∼φᴺ ⭤ (∼φ)ᴺ - | .rel r v => System.tneIff (φ := .rel r v) - | .nrel r v => System.iffId (φ := ∼∼(.rel r v)) + | .rel r v => System.tneIff (φ := Semiformulaᵢ.rel r v) + | .nrel r v => System.iffId (φ := ∼∼(Semiformulaᵢ.rel r v)) | ⊤ => System.falsumDN | ⊥ => System.iffId (φ := ∼⊥) | φ ⋏ ψ => diff --git a/Foundation/IntProp/Dialectica/Basic.lean b/Foundation/IntProp/Dialectica/Basic.lean index 41b7d16a..95000192 100644 --- a/Foundation/IntProp/Dialectica/Basic.lean +++ b/Foundation/IntProp/Dialectica/Basic.lean @@ -44,11 +44,11 @@ def Interpret (V : α → Prop) : (φ : Formula α) → Witness φ → Counter | ∼φ, f, θ => ¬Interpret V φ θ (f θ) | φ ➝ ψ, ⟨f, g⟩, ⟨θ, π⟩ => Interpret V φ θ (g θ π) → Interpret V ψ (f θ) π -scoped notation "⟦" w " | " c "⟧ ⊩[" V "] " φ:46 => Interpret V φ w c +scoped notation:80 "⟦" w " | " c "⟧⊩[" V "] " φ:46 => Interpret V φ w c -def Valid (φ : Formula α) : Prop := ∃ w, ∀ V c, ⟦w | c⟧ ⊩[V] φ +def Valid (φ : Formula α) : Prop := ∃ w, ∀ V c, ⟦w | c⟧⊩[V] φ -def NotValid (φ : Formula α) : Prop := ∀ w, ∃ V c, ¬⟦w | c⟧ ⊩[V] φ +def NotValid (φ : Formula α) : Prop := ∀ w, ∃ V c, ¬⟦w | c⟧⊩[V] φ scoped notation "⊩ " φ => Valid φ @@ -57,29 +57,29 @@ scoped notation "⊮ " φ => NotValid φ lemma not_valid_iff_notValid {φ : Formula α} : (¬⊩ φ) ↔ (⊮ φ) := by simp [Valid, NotValid] -@[simp] lemma interpret_verum {w c V} : ⟦w | c⟧ ⊩[V] (⊤ : Formula α) := trivial +@[simp] lemma interpret_verum {w c V} : ⟦w | c⟧⊩[V] (⊤ : Formula α) := trivial -@[simp] lemma interpret_falsum {w c V} : ¬⟦w | c⟧ ⊩[V] (⊥ : Formula α) := id +@[simp] lemma interpret_falsum {w c V} : ¬⟦w | c⟧⊩[V] (⊥ : Formula α) := id -@[simp] lemma interpret_atom {w c V} {a : α} : (⟦w | c⟧ ⊩[V] .atom a) ↔ V a := Eq.to_iff rfl +@[simp] lemma interpret_atom {w c V} {a : α} : (⟦w | c⟧⊩[V] .atom a) ↔ V a := Eq.to_iff rfl @[simp] lemma interpret_and_left {φ ψ : Formula α} {V θ π} : - ⟦θ | .inl π⟧ ⊩[V] φ ⋏ ψ ↔ ⟦θ.1 | π⟧ ⊩[V] φ := Eq.to_iff rfl + ⟦θ | .inl π⟧⊩[V] φ ⋏ ψ ↔ ⟦θ.1 | π⟧⊩[V] φ := Eq.to_iff rfl @[simp] lemma interpret_and_right {φ ψ : Formula α} {V θ π} : - ⟦θ | .inr π⟧ ⊩[V] φ ⋏ ψ ↔ ⟦θ.2 | π⟧ ⊩[V] ψ := Eq.to_iff rfl + ⟦θ | .inr π⟧⊩[V] φ ⋏ ψ ↔ ⟦θ.2 | π⟧⊩[V] ψ := Eq.to_iff rfl @[simp] lemma interpret_or_left {φ ψ : Formula α} {V θ π} : - ⟦.inl θ | π⟧ ⊩[V] φ ⋎ ψ ↔ ⟦θ | π.1⟧ ⊩[V] φ := Eq.to_iff rfl + ⟦.inl θ | π⟧⊩[V] φ ⋎ ψ ↔ ⟦θ | π.1⟧⊩[V] φ := Eq.to_iff rfl @[simp] lemma interpret_or_right {φ ψ : Formula α} {V θ π} : - ⟦.inr θ | π⟧ ⊩[V] φ ⋎ ψ ↔ ⟦θ | π.2⟧ ⊩[V] ψ := Eq.to_iff rfl + ⟦.inr θ | π⟧⊩[V] φ ⋎ ψ ↔ ⟦θ | π.2⟧⊩[V] ψ := Eq.to_iff rfl @[simp] lemma interpret_not {φ : Formula α} {V θ f} : - ⟦f | θ⟧ ⊩[V] ∼φ ↔ ¬⟦θ | f θ⟧ ⊩[V] φ := Eq.to_iff rfl + ⟦f | θ⟧⊩[V] ∼φ ↔ ¬⟦θ | f θ⟧⊩[V] φ := Eq.to_iff rfl @[simp] lemma interpret_imply {φ ψ : Formula α} {V f π} : - ⟦f | π⟧ ⊩[V] φ ➝ ψ ↔ (⟦π.1 | f.2 π.1 π.2⟧ ⊩[V] φ → ⟦f.1 π.1 | π.2⟧ ⊩[V] ψ) := Eq.to_iff rfl + ⟦f | π⟧⊩[V] φ ➝ ψ ↔ (⟦π.1 | f.2 π.1 π.2⟧⊩[V] φ → ⟦f.1 π.1 | π.2⟧⊩[V] ψ) := Eq.to_iff rfl protected lemma Valid.refl (φ : Formula α) : ⊩ φ ➝ φ := ⟨⟨id, fun _ π ↦ π⟩, by rintro V ⟨θ, π⟩; simp⟩ diff --git a/Foundation/Vorspiel/Arith.lean b/Foundation/Vorspiel/Arith.lean index 4e52309f..2f21143d 100644 --- a/Foundation/Vorspiel/Arith.lean +++ b/Foundation/Vorspiel/Arith.lean @@ -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}, (Vector ℕ n →. ℕ) → Prop +inductive ArithPart₁ : ∀ {n}, (Mathlib.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 : Vector ℕ n → ℕ) - | mul {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i * v.get j : Vector ℕ n → ℕ) - | proj {n} (i : Fin n) : @ArithPart₁ n (fun v => v.get i : Vector ℕ n → ℕ) - | equal {n} (i j : Fin n) : @ArithPart₁ n (fun v => isEqNat (v.get i) (v.get j) : Vector ℕ n → ℕ) - | lt {n} (i j : Fin n) : @ArithPart₁ n (fun v => isLtNat (v.get i) (v.get j) : Vector ℕ n → ℕ) - | comp {m n f} (g : Fin n → Vector ℕ m →. ℕ) : - ArithPart₁ f → (∀ i, ArithPart₁ (g i)) → ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f - | rfind {n} {f : Vector ℕ (n + 1) → ℕ} : - ArithPart₁ (n := n + 1) f → ArithPart₁ (fun v => rfind fun n => some (f (n ::ᵥ v) = 0)) - -def Arith₁ (f : Vector ℕ n → ℕ) := ArithPart₁ (n := n) f + | 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) → ℕ} : + 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 end Nat @@ -96,7 +96,7 @@ namespace Nat.ArithPart₁ open Primrec -lemma to_partrec' {n} {f : Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partrec' f := by +lemma to_partrec' {n} {f : Mathlib.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 : Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partre 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 : Vector ℕ n) => if v.get i = v.get j then 1 else 0) := + have : Primrec (fun (v : Mathlib.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 : Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partre (_root_.Primrec.const 0) exact Partrec'.of_part this.to_comp.partrec case lt n i j => - have : Primrec (fun (v : Vector ℕ n) => if v.get i < v.get j then 1 else 0) := + have : Primrec (fun (v : Mathlib.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 : Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partre case rfind f _ hf => exact Partrec'.rfind hf -lemma of_eq {n} {f g : Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (H : ∀ i, f i = g i) : ArithPart₁ g := +lemma of_eq {n} {f g : Mathlib.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (H : ∀ i, f i = g i) : ArithPart₁ g := (funext H : f = g) ▸ hf -lemma bind (f : Vector ℕ n → ℕ →. ℕ) (hf : @ArithPart₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : +lemma bind (f : Mathlib.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, mOfFn] + · simp[hgv, Mathlib.Vector.mOfFn] · simp[hgv, Matrix.comp_vecCons'] - have : mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (Vector.ofFn (x :> fun j => v.get j)) := by + 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 funext i; cases i using Fin.cases <;> simp[hgv] simp[this]) -lemma map (f : Vector ℕ n → ℕ → ℕ) (hf : @Arith₁ (n + 1) fun v => f v.tail v.head) {g} (hg : @ArithPart₁ n g) : +lemma map (f : Mathlib.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 → Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by + have : (fun j => (![↑g, h] : Fin 2 → Mathlib.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 : ℕ → Vector ℕ n → ℕ} (h : Arith₁ (n := n + 1) (fun v => f v.head v.tail)) : +lemma rfind' {n} {f : ℕ → Mathlib.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 : Vector ℕ n → ℕ} (hf : Arith₁ f) (H : ∀ i, f i = g i) : Arith₁ g := +lemma of_eq {n} {f g : Mathlib.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 : Vector ℕ n → ℕ) := Nat.ArithPart₁.zero +lemma zero {n} : @Arith₁ n (fun _ => 0 : Mathlib.Vector ℕ n → ℕ) := Nat.ArithPart₁.zero -lemma one {n} : @Arith₁ n (fun _ => 1 : Vector ℕ n → ℕ) := Nat.ArithPart₁.one +lemma one {n} : @Arith₁ n (fun _ => 1 : Mathlib.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 → Vector ℕ m → ℕ) (hf : Arith₁ f) (hg : ∀ i, Arith₁ (g i)) : - Arith₁ fun v => f (Vector.ofFn fun i => g i v) := - (Nat.ArithPart₁.comp (fun i => g i : Fin n → Vector ℕ m →. ℕ) hf hg).of_eq <| by simp +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 -def Vec {n m} (f : Vector ℕ n → Vector ℕ m) : Prop := ∀ i, Arith₁ fun v => (f v).get i +def Vec {n m} (f : Mathlib.Vector ℕ n → Mathlib.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 : Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : Arith₁ g) (hh : Arith₁ h) : +lemma if_pos {n} {f g h : Mathlib.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 : Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : Arith₁ exact this.of_eq <| by intro i; by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff] -lemma to_arith₁ {f : Vector ℕ n → ℕ} (h : Arith₁ f) : @ArithPart₁ n (fun x => f x) := h +lemma to_arith₁ {f : Mathlib.Vector ℕ n → ℕ} (h : Arith₁ f) : @ArithPart₁ n (fun x => f x) := h end Nat.Arith₁ namespace Nat.ArithPart₁ -lemma rfindPos {n} {f : Vector ℕ (n + 1) → ℕ} (h : Arith₁ f) : +lemma rfindPos {n} {f : Mathlib.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 : Vector ℕ n → ℕ → ℕ) +lemma implicit_fun {n} (i : Fin n) (f : Mathlib.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 : Vector ℕ (n + 1) → ℕ := + let F : Mathlib.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 (Vector.get v i) - · exact lt_succ_sqrt (Vector.get v i) + · exact sqrt_le (Mathlib.Vector.get v i) + · exact lt_succ_sqrt (Mathlib.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 : Vector ℕ (n + 1) → ℕ := fun v => + let F : Mathlib.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 (Vector.get v i) m + have : v.get i ∣ v.get j := by rw[←A]; exact Nat.dvd_mul_left (Mathlib.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 : Vector ℕ (n + 1) → ℕ := fun v => isDvdNat (v.get j.succ) (v.get i.succ - v.head) + let F : Mathlib.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 {φ : Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => φ v.tail v.head)) (i) : +lemma ball {φ : Mathlib.Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => φ v.tail v.head)) (i) : Arith₁ (fun v => ball (v.get i) (φ v)) := by - let F : Vector ℕ (n + 1) → ℕ := fun v => (φ v.tail v.head).inv.or (isLeNat (v.get i.succ) v.head) + let F : Mathlib.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 {φ : Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => · 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 < Vector.get v i, φ v x = 0 ∧ ∀ y < x, φ v y ≠ 0 := by + · have : ∃ x < Mathlib.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 {φ : Vector ℕ n → ℕ → ℕ} (hp : @Arith₁ (n + 1) (fun v => 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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Vector ℕ n) : List ℕ := +def recSequence (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Vector ℕ n) +lemma beta_unbeta_recSequence_eq (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Vector ℕ n) : +lemma beta_unbeta_recSequence_zero (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Vector ℕ n) +lemma beta_unbeta_recSequence_succ (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) {z : ℕ} {v} +lemma beta_eq_rec (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.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 : Vector ℕ n → ℕ) (g : Vector ℕ (n + 2) → ℕ) {z 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 : Vector ℕ (n + 2) → ℕ := fun v => + let F : Mathlib.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[Vector.get_one]) + simp[Mathlib.Vector.get_one]) have : @Arith₁ (n + 2) (fun v => Nat.beta v.head v.tail.head) := - (beta 0 1).of_eq (by simp [Vector.get_one]) + (beta 0 1).of_eq (by simp [Mathlib.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 : Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ f := by +lemma of_primrec {f : Mathlib.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 : Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ f := by 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 : Vector ℕ n →. ℕ} (hf : Partrec' f) : ArithPart₁ f := by +lemma _root_.Nat.ArithPart₁.of_partrec {f : Mathlib.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 → (Vector ℕ n →. ℕ) → Prop +inductive Code.eval : {n : ℕ} → Code n → (Mathlib.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 → (Vector ℕ n →. ℕ) → Prop | 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 : Vector ℕ n →. ℕ) (g : Fin n → (Vector ℕ m →. ℕ)) : + | comp {m n} (c : Code n) (d : Fin n → Code m) (f : Mathlib.Vector ℕ n →. ℕ) (g : Fin n → (Mathlib.Vector ℕ m →. ℕ)) : Code.eval c f → (∀ i, Code.eval (d i) (g i)) → - Code.eval (c.comp d) (fun v => (mOfFn fun i => g i v) >>= f) - | rfind {n} (c : Code (n + 1)) (f : Vector ℕ (n + 1) → ℕ) : + 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 f → Code.eval c.rfind (fun v => Nat.rfind fun n => Part.some (f (n ::ᵥ v) = 0)) -lemma exists_code : ∀ {n : ℕ} {f : Vector ℕ n →. ℕ}, ArithPart₁ f → ∃ c : Code n, c.eval f +lemma exists_code : ∀ {n : ℕ} {f : Mathlib.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/lake-manifest.json b/lake-manifest.json index 2a84c9e2..ccf9d8ca 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,95 +1,95 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", - "name": "batteries", + "rev": "b18b0c87025ebd469227afa91b78f861cac466b8", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", - "name": "aesop", + "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "68280daef58803f68368eb2e53046dabcd270c9d", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.47", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", + "scope": "leanprover-community", + "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", - "name": "importGraph", + "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "v4.14.0", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", - "name": "LeanSearchClient", + "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", - "name": "plausible", + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "dde4f2ecaec222a1c7db638d7536f0b195d8e953", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.toml"}], "name": "foundation", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 401bc146..cf25a981 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 \ No newline at end of file +leanprover/lean4:v4.15.0-rc1