From 6087167486ee621bac227b1aa47373d8931313ad Mon Sep 17 00:00:00 2001 From: palalansouki Date: Fri, 29 Mar 2024 22:01:33 +0900 Subject: [PATCH] instance definability --- Arithmetization/Basic/IOpen.lean | 12 ++++++------ Arithmetization/IDeltaZero/Exponential/Exp.lean | 6 +++--- Arithmetization/IDeltaZero/Exponential/Log.lean | 8 ++++---- Arithmetization/IDeltaZero/Exponential/PPow2.lean | 2 +- Arithmetization/IDeltaZero/Exponential/Pow2.lean | 4 ++-- Arithmetization/ISigmaOne/Bit.lean | 6 +++--- Arithmetization/OmegaOne/Basic.lean | 2 +- Arithmetization/OmegaOne/Nuon.lean | 6 +++--- 8 files changed, 23 insertions(+), 23 deletions(-) diff --git a/Arithmetization/Basic/IOpen.lean b/Arithmetization/Basic/IOpen.lean index 40e749f..19f08cc 100644 --- a/Arithmetization/Basic/IOpen.lean +++ b/Arithmetization/Basic/IOpen.lean @@ -184,7 +184,7 @@ lemma div_mul (a b c : M) : a / (b * c) = a / b / c := by instance div_polybounded : PolyBounded₂ ℒₒᵣ ((· / ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩ -instance div_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν ((· / ·) : M → M → M) := defined_to_with_param₀ _ div_defined +instance div_definable : DefinableFunction₂ ℒₒᵣ Σ 0 ((· / ·) : M → M → M) := defined_to_with_param _ div_defined @[simp] lemma div_mul_le (a b : M) : a / b * b ≤ a := by rw [mul_comm]; exact mul_div_le _ _ @@ -299,7 +299,7 @@ lemma rem_defined : Δ₀-Function₂ ((· % ·) : M → M → M) via remDef := intro v; simp [Matrix.vecHead, Matrix.vecTail, remDef, rem_graph, Semiformula.eval_substs, div_defined.pval, sub_defined.pval, le_iff_lt_succ] -instance rem_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν ((· % ·) : M → M → M) := defined_to_with_param₀ _ rem_defined +instance rem_definable : DefinableFunction₂ ℒₒᵣ Σ 0 ((· % ·) : M → M → M) := defined_to_with_param _ rem_defined lemma div_add_mod (a b : M) : b * (a / b) + (a % b) = a := add_tsub_self_of_le (mul_div_le a b) @@ -459,7 +459,7 @@ def sqrtdef : Δ₀Sentence 2 := lemma sqrt_defined : Δ₀-Function₁ (λ a : M ↦ √a) via sqrtdef := by intro v; simp[sqrt_graph, sqrtdef, Matrix.vecHead, Matrix.vecTail] -instance sqrt_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν ((√·) : M → M) := defined_to_with_param₀ _ sqrt_defined +instance sqrt_definable : DefinableFunction₁ ℒₒᵣ Σ 0 ((√·) : M → M) := defined_to_with_param₀ _ sqrt_defined lemma eq_sqrt (x a : M) : x * x ≤ a ∧ a < (x + 1) * (x + 1) → x = √a := Classical.choose_uniq (sqrt_exists_unique a) @@ -550,7 +550,7 @@ def pairDef : Δ₀Sentence 3 := ⟨“(#1 < #2 ∧ #0 = #2 * #2 + #1) ∨ (#2 lemma pair_defined : Δ₀-Function₂ (λ a b : M ↦ ⟪a, b⟫) via pairDef := by intro v; simp [pair_graph, pairDef] -instance pair_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (pair : M → M → M) := defined_to_with_param₀ _ pair_defined +instance pair_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (pair : M → M → M) := defined_to_with_param₀ _ pair_defined instance : PolyBounded₂ ℒₒᵣ (pair : M → M → M) := ⟨ᵀ“(#1 * #1 + #0) + (#0 * #0 + #0 + #1)”, by intro v; simp [pair]; split_ifs <;> try simp [pair, *]⟩ @@ -610,7 +610,7 @@ lemma pi₁_defined : Δ₀-Function₁ (pi₁ : M → M) via pi₁Def := by · intro h; exact ⟨π₂ v 1, by simp [←le_iff_lt_succ], by simp [h]⟩ · rintro ⟨a, _, e⟩; simp [e] -instance pi₁_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (pi₁ : M → M) := defined_to_with_param₀ _ pi₁_defined +instance pi₁_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (pi₁ : M → M) := defined_to_with_param₀ _ pi₁_defined lemma pi₂_defined : Δ₀-Function₁ (pi₂ : M → M) via pi₂Def := by intro v; simp [pi₂Def, pair_defined.pval] @@ -618,7 +618,7 @@ lemma pi₂_defined : Δ₀-Function₁ (pi₂ : M → M) via pi₂Def := by · intro h; exact ⟨π₁ v 1, by simp [←le_iff_lt_succ], by simp [h]⟩ · rintro ⟨a, _, e⟩; simp [e] -instance pi₂_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (pi₂ : M → M) := defined_to_with_param₀ _ pi₂_defined +instance pi₂_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (pi₂ : M → M) := defined_to_with_param₀ _ pi₂_defined end pair diff --git a/Arithmetization/IDeltaZero/Exponential/Exp.lean b/Arithmetization/IDeltaZero/Exponential/Exp.lean index b49feb5..87ccfda 100644 --- a/Arithmetization/IDeltaZero/Exponential/Exp.lean +++ b/Arithmetization/IDeltaZero/Exponential/Exp.lean @@ -28,7 +28,7 @@ lemma ext_defined : Δ₀-Function₂ (λ a b : M ↦ ext a b) via extDef := by intro v; simp [Matrix.vecHead, Matrix.vecTail, extDef, ext_graph, Semiformula.eval_substs, div_defined.pval, rem_defined.pval, le_iff_lt_succ] -instance ext_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (ext : M → M → M) := defined_to_with_param₀ _ ext_defined +instance ext_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (ext : M → M → M) := defined_to_with_param _ ext_defined @[simp] lemma ext_le_add (u z : M) : ext u z ≤ z := le_trans (mod_le (z / u) u) (by simp [add_comm]) @@ -112,7 +112,7 @@ def Exp.def : Δ₀Sentence 2 := ⟨ lemma Exp.defined : Δ₀-Relation (Exp : M → M → Prop) via Exp.def := by intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval, Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq] -instance exp_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν (Exp : M → M → Prop) := defined_to_with_param₀ _ Exp.defined +instance exp_definable : DefinableRel ℒₒᵣ Σ 0 (Exp : M → M → Prop) := defined_to_with_param _ Exp.defined namespace Exp @@ -717,7 +717,7 @@ def expdef : Δ₀Sentence 2 := ⟨“!Exp.def [#1, #0]”, by simp⟩ lemma exp_defined : Δ₀-Function₁ (exponential : M → M) via expdef := by intro v; simp [expdef, exponential_graph, Exp.defined.pval] -instance exponential_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (exponential : M → M) := defined_to_with_param₀ _ exp_defined +instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (exponential : M → M) := defined_to_with_param _ exp_defined lemma exponential_of_exp {a b : M} (h : Exp a b) : exp a = b := Eq.symm <| exponential_graph.mpr h diff --git a/Arithmetization/IDeltaZero/Exponential/Log.lean b/Arithmetization/IDeltaZero/Exponential/Log.lean index cf7a9c8..704a97b 100644 --- a/Arithmetization/IDeltaZero/Exponential/Log.lean +++ b/Arithmetization/IDeltaZero/Exponential/Log.lean @@ -72,7 +72,7 @@ def logDef : Δ₀Sentence 2 := ⟨“(#1 = 0 → #0 = 0) ∧ (0 < #1 → #0 < # lemma log_defined : Δ₀-Function₁ (log : M → M) via logDef := by intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ] -instance log_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (log : M → M) := defined_to_with_param₀ _ log_defined +instance log_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (log : M → M) := defined_to_with_param _ log_defined instance : PolyBounded₁ ℒₒᵣ (log : M → M) := ⟨#0, λ _ ↦ by simp⟩ @@ -163,7 +163,7 @@ def lengthDef : Δ₀Sentence 2 := ⟨“(0 < #1 → ∃[#0 < #2 + 1] (!logDef [ lemma length_defined : Δ₀-Function₁ (‖·‖ : M → M) via lengthDef := by intro v; simp [lengthDef, length_graph, log_defined.pval, ←le_iff_lt_succ] -instance length_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (‖·‖ : M → M) := defined_to_with_param₀ _ length_defined +instance length_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (‖·‖ : M → M) := defined_to_with_param _ length_defined instance : PolyBounded₁ ℒₒᵣ (‖·‖ : M → M) := ⟨#0, λ _ ↦ by simp⟩ @@ -334,7 +334,7 @@ def bexpDef : Δ₀Sentence 3 := ⟨“∃[#0 < #2 + 1] (!lengthDef [#0, #2] ∧ lemma bexp_defined : Δ₀-Function₂ (bexp : M → M → M) via bexpDef := by intro v; simp [bexpDef, bexp_graph, Exp.defined.pval, length_defined.pval, ←le_iff_lt_succ] -instance bexp_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (bexp : M → M → M) := defined_to_with_param₀ _ bexp_defined +instance bexp_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (bexp : M → M → M) := defined_to_with_param _ bexp_defined instance : PolyBounded₂ ℒₒᵣ (bexp : M → M → M) := ⟨#0, λ _ ↦ by simp⟩ @@ -413,7 +413,7 @@ lemma fbit_defined : Δ₀-Function₂ (fbit : M → M → M) via fbitDef := by · intro h; exact ⟨bexp (v 1) (v 2), by simp, rfl, _, by simp, rfl, h⟩ · rintro ⟨_, _, rfl, _, _, rfl, h⟩; exact h -instance fbit_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (fbit : M → M → M) := defined_to_with_param₀ _ fbit_defined +instance fbit_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (fbit : M → M → M) := defined_to_with_param _ fbit_defined instance : PolyBounded₂ ℒₒᵣ (fbit : M → M → M) := ⟨ᵀ“1”, λ _ ↦ by simp⟩ diff --git a/Arithmetization/IDeltaZero/Exponential/PPow2.lean b/Arithmetization/IDeltaZero/Exponential/PPow2.lean index 3f96da7..fab29a9 100644 --- a/Arithmetization/IDeltaZero/Exponential/PPow2.lean +++ b/Arithmetization/IDeltaZero/Exponential/PPow2.lean @@ -38,7 +38,7 @@ def ppow2Def : Δ₀Sentence 1 := lemma ppow2_defined : Δ₀-Predicate (PPow2 : M → Prop) via ppow2Def := by intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval] -instance ppow2_definable (Γ ν) : DefinablePred ℒₒᵣ Γ ν (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined +instance ppow2_definable : DefinablePred ℒₒᵣ Σ 0 (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined namespace SPPow2 diff --git a/Arithmetization/IDeltaZero/Exponential/Pow2.lean b/Arithmetization/IDeltaZero/Exponential/Pow2.lean index ced3f91..8454283 100644 --- a/Arithmetization/IDeltaZero/Exponential/Pow2.lean +++ b/Arithmetization/IDeltaZero/Exponential/Pow2.lean @@ -24,7 +24,7 @@ lemma pow2_defined : Δ₀-Predicate (Pow2 : M → Prop) via pow2Def := by simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton, Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval] -instance pow2_definable (Γ ν) : DefinablePred ℒₒᵣ Γ ν (Pow2 : M → Prop) := defined_to_with_param₀ _ pow2_defined +instance pow2_definable : DefinablePred ℒₒᵣ Σ 0 (Pow2 : M → Prop) := defined_to_with_param _ pow2_defined lemma Pow2.pos {a : M} (h : Pow2 a) : 0 < a := h.1 @@ -119,7 +119,7 @@ lemma lenbit_defined : Δ₀-Relation (LenBit : M → M → Prop) via lenbitDef · intro h; exact ⟨v 1 / v 0, by simp, rfl, h⟩ · rintro ⟨z, hz, rfl, h⟩; exact h -instance lenbit_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν (LenBit : M → M → Prop) := defined_to_with_param₀ _ lenbit_defined +instance lenbit_definable : DefinableRel ℒₒᵣ Σ 0 (LenBit : M → M → Prop) := defined_to_with_param _ lenbit_defined lemma LenBit.le {i a : M} (h : LenBit i a) : i ≤ a := by by_contra A; simp [LenBit, show a < i from by simpa using A] at h diff --git a/Arithmetization/ISigmaOne/Bit.lean b/Arithmetization/ISigmaOne/Bit.lean index 5cbda33..e816515 100644 --- a/Arithmetization/ISigmaOne/Bit.lean +++ b/Arithmetization/ISigmaOne/Bit.lean @@ -27,7 +27,7 @@ lemma bit_defined : Δ₀-Relation ((· ∈ ·) : M → M → Prop) via bitDef : · intro h; exact ⟨exp (v 0), by simp [h.le], rfl, h⟩ · rintro ⟨_, _, rfl, h⟩; exact h -instance mem_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν ((· ∈ ·) : M → M → Prop) := defined_to_with_param₀ _ bit_defined +instance mem_definable : DefinableRel ℒₒᵣ Σ 0 ((· ∈ ·) : M → M → Prop) := defined_to_with_param _ bit_defined open Classical in noncomputable def bitInsert (i a : M) : M := if i ∈ a then a else a + exp i @@ -137,7 +137,7 @@ lemma bitSubset_defined : Δ₀-Relation ((· ⊆ ·) : M → M → Prop) via bi intro v; simp [bitSubsetDef, bit_defined.pval] exact ⟨by intro h x _ hx; exact h hx, by intro h x hx; exact h x (lt_of_mem hx) hx⟩ -instance bitSubset_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν ((· ⊆ ·) : M → M → Prop) := defined_to_with_param₀ _ bitSubset_defined +instance bitSubset_definable : DefinableRel ℒₒᵣ Σ 0 ((· ⊆ ·) : M → M → Prop) := defined_to_with_param₀ _ bitSubset_defined lemma mem_exp_add_succ_sub_one (i j : M) : i ∈ exp (i + j + 1) - 1 := by have : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1) := calc @@ -215,7 +215,7 @@ theorem finset_comprehension {P : M → Prop} (hP : Γ(ν)-Predicate P) (n : M) have : (Γ.alt)(ν)-Predicate (fun s ↦ ∀ i < n, P i → i ∈ s) := by apply Definable.ball_lt; simp; apply Definable.imp definability - simp [mem_definable] + apply @Definable.of_sigma_zero M ℒₒᵣ _ _ _ _ mem_definable have : ∃ t, (∀ i < n, P i → i ∈ t) ∧ ∀ t' < t, ∃ x, P x ∧ x < n ∧ x ∉ t' := by simpa using least_number_h (L := ℒₒᵣ) Γ.alt ν this hs rcases this with ⟨t, ht, t_minimal⟩ diff --git a/Arithmetization/OmegaOne/Basic.lean b/Arithmetization/OmegaOne/Basic.lean index 624b53e..c41066b 100644 --- a/Arithmetization/OmegaOne/Basic.lean +++ b/Arithmetization/OmegaOne/Basic.lean @@ -67,7 +67,7 @@ lemma hash_defined : Δ₀-Function₂ (Hash.hash : M → M → M) via hashDef : · intro h; exact ⟨‖v 1‖, by simp, ‖v 2‖, by simp, rfl, rfl, by rw [h]; exact exp_hash _ _⟩ · rintro ⟨_, _, _, _, rfl, rfl, h⟩; exact h.uniq (exp_hash (v 1) (v 2)) -instance hash_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (Hash.hash : M → M → M) := defined_to_with_param₀ _ hash_defined +instance hash_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (Hash.hash : M → M → M) := defined_to_with_param _ hash_defined @[simp] lemma hash_pow2 (a b : M) : Pow2 (a # b) := (exp_hash a b).range_pow2 diff --git a/Arithmetization/OmegaOne/Nuon.lean b/Arithmetization/OmegaOne/Nuon.lean index e80882d..ea86d0b 100644 --- a/Arithmetization/OmegaOne/Nuon.lean +++ b/Arithmetization/OmegaOne/Nuon.lean @@ -82,7 +82,7 @@ def extDef : Δ₀Sentence 4 := lemma ext_defined : Δ₀-Function₃ (ext : M → M → M → M) via extDef := by intro v; simp [extDef, length_defined.pval, Exp.defined.pval, div_defined.pval, rem_defined.pval, lt_succ_iff_le, ext_graph] -instance ext_Definable (Γ ν) : DefinableFunction₃ ℒₒᵣ Γ ν (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined +instance ext_Definable : DefinableFunction₃ ℒₒᵣ Σ 0 (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩ @@ -565,7 +565,7 @@ lemma nuonAux_defined : Δ₀-Relation₃ (NuonAux : M → M → M → Prop) via length_defined.pval, sqrt_defined.pval, bexp_defined.pval, seriesSegmentDef_defined.pval, lt_succ_iff_le] rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]; simp -instance nuonAux_definable (Γ ν) : DefinableRel₃ ℒₒᵣ Γ ν (NuonAux : M → M → M → Prop) := defined_to_with_param₀ _ nuonAux_defined +instance nuonAux_definable : DefinableRel₃ ℒₒᵣ Σ 0 (NuonAux : M → M → M → Prop) := defined_to_with_param _ nuonAux_defined instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩ @@ -679,7 +679,7 @@ lemma nuon_defined : Δ₀-Function₁ (nuon : M → M) via nuonDef := by length_defined.pval, Nuon.nuonAux_defined.pval, lt_succ_iff_le] rw [Nuon.bex_eq_le_iff]; simp -instance nuon_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (nuon : M → M) := defined_to_with_param₀ _ nuon_defined +instance nuon_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (nuon : M → M) := defined_to_with_param _ nuon_defined end Model