From dc46bdbb6c422e16500f6929e74b53c71a679821 Mon Sep 17 00:00:00 2001 From: palalansouki Date: Thu, 25 Jul 2024 12:33:13 +0900 Subject: [PATCH] code --- Arithmetization/ISigmaOne/Bit.lean | 3 + .../ISigmaOne/HFS/Supplemental.lean | 2 - .../ISigmaOne/Metamath/Coding.lean | 274 +++++++++++++++++- .../FormalizedSigmaOneCompleteness.lean | 2 - .../ISigmaOne/Metamath/Language.lean | 16 + .../ISigmaOne/Metamath/Proof/Theory.lean | 11 + Arithmetization/Vorspiel/Lemmata.lean | 26 ++ 7 files changed, 321 insertions(+), 13 deletions(-) diff --git a/Arithmetization/ISigmaOne/Bit.lean b/Arithmetization/ISigmaOne/Bit.lean index 58aa9ba..c1e6b0f 100644 --- a/Arithmetization/ISigmaOne/Bit.lean +++ b/Arithmetization/ISigmaOne/Bit.lean @@ -303,6 +303,9 @@ lemma pos_of_nonempty {i a : M} (h : i ∈ a) : 0 < a := by @[simp] lemma mem_insert (i a : M) : i ∈ insert i a := by simp +lemma insert_eq_self_of_mem {i a : M} (h : i ∈ a) : insert i a = a := by + simp [insert_eq, bitInsert, h] + lemma log_mem_of_pos {a : M} (h : 0 < a) : log a ∈ a := mem_iff_mul_exp_add_exp_add.mpr ⟨0, a - exp log a, diff --git a/Arithmetization/ISigmaOne/HFS/Supplemental.lean b/Arithmetization/ISigmaOne/HFS/Supplemental.lean index 0f521a4..fb26675 100644 --- a/Arithmetization/ISigmaOne/HFS/Supplemental.lean +++ b/Arithmetization/ISigmaOne/HFS/Supplemental.lean @@ -112,8 +112,6 @@ instance seqExp_definable : 𝚺₁-Function₂ (seqExp : M → M → M) := Defi @[simp, definability] instance seqExp_definable' (Γ) : (Γ, m + 1)-Function₂ (seqExp : M → M → M) := .of_sigmaOne seqExp_definable _ _ -@[simp] lemma zero_ne_add_one (a : M) : 0 ≠ a + 1 := ne_of_lt (by simp) - lemma mem_seqExp_iff {s a k : M} : s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ (∀ i z, ⟪i, z⟫ ∈ s → z ∈ a) := by induction k using induction_iPiOne generalizing s · suffices 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a diff --git a/Arithmetization/ISigmaOne/Metamath/Coding.lean b/Arithmetization/ISigmaOne/Metamath/Coding.lean index 8863cf5..7464e13 100644 --- a/Arithmetization/ISigmaOne/Metamath/Coding.lean +++ b/Arithmetization/ISigmaOne/Metamath/Coding.lean @@ -1,5 +1,6 @@ import Arithmetization.ISigmaOne.Metamath.Proof.Typed import Arithmetization.Definability.Absoluteness +import Mathlib.Combinatorics.Colex namespace LO.FirstOrder @@ -22,12 +23,6 @@ open FirstOrder FirstOrder.Arith variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] -/-- TOFO: move to PeanoMinus -/ -@[simp] lemma nat_cast_inj {n m : ℕ} : (n : V) = (m : V) ↔ n = m := by - induction' n with n ih - · cases m <;> simp - · cases m <;> simp - lemma nat_cast_empty : ((∅ : ℕ) : V) = ∅ := rfl def finArrowToVec : {k : ℕ} → (Fin k → V) → V @@ -54,6 +49,17 @@ lemma quote_matrix_succ (v : Fin (k + 1) → V) : @[simp] lemma quote_cons (v : Fin k → V) (a : V) : (⌜a :> v⌝ : V) = a ∷ ⌜v⌝ := by simp [quote_matrix_succ] +@[simp] lemma quote_matrix_inj (v w : Fin k → V) : (⌜v⌝ : V) = ⌜w⌝ ↔ v = w := by + induction' k with k ih + · simp [Matrix.empty_eq] + · simp [quote_matrix_succ, ih] + constructor + · rintro ⟨h0, hs⟩ + funext x; cases' x using Fin.cases with x + · exact h0 + · exact congr_fun hs x + · rintro rfl; simp + @[simp] lemma quote_lh (v : Fin k → V) : len (⌜v⌝ : V) = k := by induction' k with k ih <;> simp [quote_matrix_succ, Matrix.empty_eq, *] @@ -62,7 +68,7 @@ lemma quote_matrix_succ (v : Fin (k + 1) → V) : · exact i.elim0 · cases' i using Fin.cases with i <;> simp [ih] -lemma quote_matrix_absolute (v : Fin k → ℕ) : ((⌜v⌝ : ℕ) : V) = ⌜fun i ↦ (v i : V)⌝ := by +@[simp] lemma quote_matrix_absolute (v : Fin k → ℕ) : ((⌜v⌝ : ℕ) : V) = ⌜fun i ↦ (v i : V)⌝ := by induction' k with k ih · simp · simp [quote_matrix_succ, ih, cons_absolute] @@ -95,6 +101,17 @@ lemma quote_fvar (x : ℕ) : ⌜(&x : SyntacticSemiterm L n)⌝ = ^&(x : V) := r lemma quote_func {k} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) : ⌜func f v⌝ = ^func (k : V) ⌜f⌝ ⌜fun i ↦ ⌜v i⌝⌝ := rfl +@[simp] lemma codeIn_inj {n} {t u : SyntacticSemiterm L n} : (⌜t⌝ : V) = ⌜u⌝ ↔ t = u := by + induction t generalizing u + case bvar z => rcases u <;> simp [quote_bvar, quote_fvar, quote_func, qqBvar, qqFvar, qqFunc, Fin.val_inj] + case fvar x => rcases u <;> simp [quote_bvar, quote_fvar, quote_func, qqBvar, qqFvar, qqFunc] + case func k f v ih => + rcases u <;> simp [quote_bvar, quote_fvar, quote_func, qqBvar, qqFvar, qqFunc] + rintro rfl; simp; rintro rfl + constructor + · intro h; funext i; exact (ih i).mp (congr_fun h i) + · rintro rfl; rfl + @[simp] lemma quote_zero (n) : (⌜(Semiterm.func Language.Zero.zero ![] : SyntacticSemiterm ℒₒᵣ n)⌝ : V) = 𝟎 := by simp [FirstOrder.Semiterm.quote_func, Formalized.zero, Formalized.qqFunc_absolute]; rfl @@ -109,6 +126,10 @@ lemma quote_func {k} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) : @[simp] lemma quote_mul (t u : SyntacticSemiterm ℒₒᵣ n) : (⌜Semiterm.func Language.Mul.mul ![t, u]⌝ : V) = (⌜t⌝ ^* ⌜u⌝) := by simp [FirstOrder.Semiterm.quote_func]; rfl +@[simp] lemma quote_absolute (t : SyntacticSemiterm L n) : + ((⌜t⌝ : ℕ) : V) = ⌜t⌝ := by + induction t <;> simp [quote_bvar, quote_fvar, quote_func, qqBvar, qqFvar, qqFunc, Fin.val_inj, nat_cast_pair, *] + end LO.FirstOrder.Semiterm namespace LO.Arith @@ -251,6 +272,70 @@ lemma quote_ex (p : SyntacticSemiformula L (n + 1)) : ⌜∃' p⌝ = ^∃[(n : V @[simp] lemma quote_nlt (t u : SyntacticSemiterm ℒₒᵣ n) : (⌜Semiformula.nrel Language.LT.lt ![t, u]⌝ : V) = (⌜t⌝ ^≮[(n : V)] ⌜u⌝) := by simp [FirstOrder.Semiformula.quote_nrel]; rfl +@[simp] lemma codeIn_inj {n} {p q : SyntacticSemiformula L n} : (⌜p⌝ : V) = ⌜q⌝ ↔ p = q := by + induction p using rec' + case hrel => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rintro rfl; simp; rintro rfl; + constructor + · intro h; funext i; simpa using congr_fun h i + · rintro rfl; rfl + case hnrel => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rintro rfl; simp; rintro rfl; + constructor + · intro h; funext i; simpa using congr_fun h i + · rintro rfl; rfl + case hverum => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + case hfalsum => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + case hand n p q ihp ihq => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rw [ihp, ihq] + case hor n p q ihp ihq => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rw [ihp, ihq] + case hall n p ih => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rw [ih] + case hex n p ih => + cases q using cases' <;> + simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx] + rw [ih] + +@[simp] lemma quote_absolute (p : SyntacticSemiformula L n) : + ((⌜p⌝ : ℕ) : V) = ⌜p⌝ := by + induction p using rec' <;> simp [quote_rel, quote_nrel, quote_verum, quote_falsum, quote_and, quote_or, quote_all, quote_ex, + qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx, nat_cast_pair, *] + +instance : GoedelQuote (Semisentence L n) V := ⟨fun σ ↦ ⌜(Rew.emb.hom σ : SyntacticSemiformula L n)⌝⟩ + +lemma quote_semisentence_def (p : Semisentence L n) : (⌜p⌝ : V) = ⌜(Rew.emb.hom p : SyntacticSemiformula L n)⌝ := rfl + +@[simp] lemma quote_semisentence_absolute (p : Semisentence L n) : ((⌜p⌝ : ℕ) : V) = ⌜p⌝ := by + simp [quote_semisentence_def] + +instance : Semiterm.Operator.GoedelNumber ℒₒᵣ (Sentence L) := ⟨fun σ ↦ Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝⟩ + +lemma sentence_goedelNumber_def (σ : Sentence L) : + (⌜σ⌝ : Semiterm ℒₒᵣ ξ n) = Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝ := rfl + end LO.FirstOrder.Semiformula namespace LO.Arith @@ -309,6 +394,11 @@ lemma substs_quote {n m} (w : Fin n → SyntacticSemiterm L m) (p : SyntacticSem case hall p ih => simp [←ih, qVec_quote, Semiterm.quote_bvar] case hex p ih => simp [←ih, qVec_quote, Semiterm.quote_bvar] +lemma free_quote (p : SyntacticSemiformula L 1) : + (L.codeIn V).free ⌜p⌝ = ⌜Rew.free.hom p⌝ := by + rw [←Rew.hom_substs_mbar_zero_comp_shift_eq_free, ←substs_quote, ←shift_quote] + simp [Language.free, Language.substs₁, Semiterm.quote_fvar] + end LO.Arith @@ -415,6 +505,70 @@ open LO.Arith Formalized end Semiformula +namespace Derivation2 + +def Sequent.codeIn (Γ : Finset (SyntacticFormula L)) : V := ∑ p ∈ Γ, exp (⌜p⌝ : V) + +instance : GoedelQuote (Finset (SyntacticFormula L)) V := ⟨Sequent.codeIn V⟩ + +lemma Sequent.codeIn_def (Γ : Finset (SyntacticFormula L)) : ⌜Γ⌝ = ∑ p ∈ Γ, exp (⌜p⌝ : V) := rfl + +variable {V} + +open Classical + +@[simp] lemma Sequent.codeIn_empty : (⌜(∅ : Finset (SyntacticFormula L))⌝ : V) = ∅ := by + simp [Sequent.codeIn_def, emptyset_def] + +lemma Sequent.mem_codeIn_iff {Γ : Finset (SyntacticFormula L)} {p} : ⌜p⌝ ∈ (⌜Γ⌝ : V) ↔ p ∈ Γ := by + induction Γ using Finset.induction generalizing p + case empty => simp [Sequent.codeIn_def] + case insert a Γ ha ih => + have : exp ⌜a⌝ + ∑ p ∈ Γ, exp (⌜p⌝ : V) = insert (⌜a⌝ : V) (⌜Γ⌝ : V) := by + simp [insert, bitInsert, (not_iff_not.mpr ih.symm).mp ha, add_comm] + rw [Sequent.codeIn_def] + simp [ha, Sequent.codeIn_def] + rw [this] + simp [←ih] + +@[simp] lemma Sequent.codeIn_insert (Γ : Finset (SyntacticFormula L)) (p) : (⌜(insert p Γ)⌝ : V) = insert ⌜p⌝ ⌜Γ⌝ := by + by_cases hp : p ∈ Γ + · simp [Sequent.mem_codeIn_iff, hp, insert_eq_self_of_mem] + · have : (⌜insert p Γ⌝ : V) = exp ⌜p⌝ + ⌜Γ⌝ := by simp [Sequent.codeIn_def, hp] + simp [Sequent.mem_codeIn_iff, this, insert_eq, bitInsert, hp, add_comm] + +lemma Sequent.mem_codeIn {Γ : Finset (SyntacticFormula L)} (hx : x ∈ (⌜Γ⌝ : V)) : ∃ p ∈ Γ, x = ⌜p⌝ := by + induction Γ using Finset.induction + case empty => simp at hx + case insert a Γ _ ih => + have : x = ⌜a⌝ ∨ x ∈ (⌜Γ⌝ : V) := by simpa using hx + rcases this with (rfl | hx) + · exact ⟨a, by simp⟩ + · rcases ih hx with ⟨p, hx, rfl⟩ + exact ⟨p, by simp [*]⟩ + +variable (V) + +def codeIn : {Γ : Finset (SyntacticFormula L)} → ⊢¹ᶠ Γ → V + | _, axL (Δ := Δ) p _ _ => Arith.axL ⌜Δ⌝ ⌜p⌝ + | _, verum (Δ := Δ) _ => Arith.verumIntro ⌜Δ⌝ + | _, and (Δ := Δ) _ (p := p) (q := q) bp bq => Arith.andIntro ⌜Δ⌝ ⌜p⌝ ⌜q⌝ bp.codeIn bq.codeIn + | _, or (Δ := Δ) (p := p) (q := q) _ d => Arith.orIntro ⌜Δ⌝ ⌜p⌝ ⌜q⌝ d.codeIn + | _, all (Δ := Δ) (p := p) _ d => Arith.allIntro ⌜Δ⌝ ⌜p⌝ d.codeIn + | _, ex (Δ := Δ) (p := p) _ t d => Arith.exIntro ⌜Δ⌝ ⌜p⌝ ⌜t⌝ d.codeIn + | _, wk (Γ := Γ) d _ => Arith.wkRule ⌜Γ⌝ d.codeIn + | _, shift (Δ := Δ) d => Arith.shiftRule ⌜Δ.image Rew.shift.hom⌝ d.codeIn + | _, cut (Δ := Δ) (p := p) d dn => Arith.cutRule ⌜Δ⌝ ⌜p⌝ d.codeIn dn.codeIn + +instance (Γ : Finset (SyntacticFormula L)) : GoedelQuote (⊢¹ᶠ Γ) V := ⟨codeIn V⟩ + +lemma quote_derivation_def {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : (⌜d⌝ : V) = d.codeIn V := rfl + +@[simp] lemma fstidx_quote {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : fstIdx (⌜d⌝ : V) = ⌜Γ⌝ := by + induction d <;> simp [quote_derivation_def, codeIn] + +end Derivation2 + end LO.FirstOrder namespace LO.Arith @@ -425,7 +579,109 @@ variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺 variable {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] - - +open Classical + +@[simp] lemma formulaSet_codeIn_finset (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).FormulaSet ⌜Γ⌝ := by + intro x hx + rcases Derivation2.Sequent.mem_codeIn hx with ⟨p, _, rfl⟩; + apply semiformula_quote + +open Derivation2 + +lemma quote_image_shift (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).setShift (⌜Γ⌝ : V) = ⌜Γ.image Rew.shift.hom⌝ := by + induction Γ using Finset.induction + case empty => simp + case insert p Γ _ ih => simp [shift_quote, ih] + +@[simp] lemma derivation_quote {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : (L.codeIn V).Derivation ⌜d⌝ := by + induction d + case axL p hp hn => + exact Language.Derivation.axL (by simp) + (by simp [Sequent.mem_codeIn_iff, hp]) + (by simp [Sequent.mem_codeIn_iff, neg_quote, hn]) + case verum Δ h => + exact Language.Derivation.verumIntro (by simp) + (by simpa [quote_verum] using (Sequent.mem_codeIn_iff (V := V)).mpr h) + case and Δ p q hpq dp dq ihp ihq => + apply Language.Derivation.andIntro + (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr hpq) + ⟨by simp [fstidx_quote], ihp⟩ + ⟨by simp [fstidx_quote], ihq⟩ + case or Δ p q hpq d ih => + apply Language.Derivation.orIntro + (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr hpq) + ⟨by simp [fstidx_quote], ih⟩ + case all Δ p h d ih => + apply Language.Derivation.allIntro + (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr h) + ⟨by simp [fstidx_quote, quote_image_shift, free_quote], ih⟩ + case ex Δ p h t d ih => + apply Language.Derivation.exIntro + (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr h) + (semiterm_codeIn t) + ⟨by simp [fstidx_quote, ←substs_quote, Language.substs₁], ih⟩ + case wk Δ Γ d h ih => + apply Language.Derivation.wkRule (s' := ⌜Δ⌝) + (by simp) + (by intro x hx; rcases Sequent.mem_codeIn hx with ⟨p, hp, rfl⟩ + simp [Sequent.mem_codeIn_iff, h hp]) + ⟨by simp [fstidx_quote], ih⟩ + case shift Δ d ih => + simp [quote_derivation_def, Derivation2.codeIn, ←quote_image_shift] + apply Language.Derivation.shiftRule + ⟨by simp [fstidx_quote], ih⟩ + case cut Δ p d dn ih ihn => + apply Language.Derivation.cutRule + ⟨by simp [fstidx_quote], ih⟩ + ⟨by simp [fstidx_quote, neg_quote], ihn⟩ + +@[simp] lemma derivationOf_quote {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : (L.codeIn V).DerivationOf ⌜d⌝ ⌜Γ⌝ := + ⟨by simp, by simp⟩ + +section + +class DefinableSigma₁Theory (T : Theory L) extends LDef.TDef L.lDef where + mem_iff {σ} : σ ∈ T ↔ 𝐈𝚺₁ ⊢₌! ch.val/[⌜σ⌝] + fvfree : 𝐈𝚺₁ ⊢₌! “∀ σ, !ch σ → !L.lDef.isFVFreeDef σ” + +def _root_.LO.FirstOrder.Theory.tDef (T : Theory L) [d : DefinableSigma₁Theory T] : LDef.TDef L.lDef := d.toTDef + +variable {T : Theory L} [DefinableSigma₁Theory T] + +variable (T V) + +def _root_.LO.FirstOrder.Theory.codeIn : (L.codeIn V).Theory where + set := {x | V ⊧/![x] T.tDef.ch.val} + set_fvFree := by + intro x hx + have : ∀ x, V ⊧/![x] T.tDef.ch.val → (L.codeIn V).IsFVFree x := by + simpa [models_iff, (isFVFree_defined (V := V) (L.codeIn V)).df.iff] using + consequence_iff_add_eq.mp (sound! <| DefinableSigma₁Theory.fvfree (T := T)) V inferInstance + exact this x hx + +variable {T V} + +lemma Language.Theory.codeIn_iff : x ∈ T.codeIn V ↔ V ⊧/![x] T.tDef.ch.val := iff_of_eq rfl + +lemma mem_coded_theory {σ} (h : σ ∈ T) : ⌜σ⌝ ∈ T.codeIn V := Language.Theory.codeIn_iff.mpr <| by + have := consequence_iff_add_eq.mp (sound! <| DefinableSigma₁Theory.mem_iff.mp h) V inferInstance + simpa [models_iff, Semiformula.sentence_goedelNumber_def, numeral_eq_natCast] using this + +instance : (T.codeIn V).Defined T.tDef where + defined := by intro v; simp [Theory.codeIn, ←Matrix.constant_eq_singleton'] + +theorem D1 : T ⊢! σ → (T.codeIn V).Provable ⌜σ⌝ := by { + provable_iff_derivation2 + } + +end + +namespace Formalized + +variable (T : Theory ℒₒᵣ) + + + +end Formalized end LO.Arith diff --git a/Arithmetization/ISigmaOne/Metamath/FormalizedSigmaOneCompleteness.lean b/Arithmetization/ISigmaOne/Metamath/FormalizedSigmaOneCompleteness.lean index bada601..ceb8d84 100644 --- a/Arithmetization/ISigmaOne/Metamath/FormalizedSigmaOneCompleteness.lean +++ b/Arithmetization/ISigmaOne/Metamath/FormalizedSigmaOneCompleteness.lean @@ -34,8 +34,6 @@ open FirstOrder FirstOrder.Arith variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] -variable {L : Arith.Language V} {pL : LDef} [Arith.Language.Defined L pL] - namespace Formalized variable {T : LOR.Theory V} {pT : (Language.lDef ℒₒᵣ).TDef} [T.Defined pT] [EQTheory T] [R₀Theory T] diff --git a/Arithmetization/ISigmaOne/Metamath/Language.lean b/Arithmetization/ISigmaOne/Metamath/Language.lean index 5da1b7d..a5a508e 100644 --- a/Arithmetization/ISigmaOne/Metamath/Language.lean +++ b/Arithmetization/ISigmaOne/Metamath/Language.lean @@ -108,6 +108,18 @@ lemma quote_rel_def (R : L.Rel k) : (⌜R⌝ : V) = ↑(Encodable.encode R) := r consequence_iff_add_eq.mp (sound! <| DefinableLanguage.rel_iff.mp ⟨r, rfl⟩) V (models_of_subtheory (T := 𝐏𝐀⁻) inferInstance) +@[simp] lemma quote_func_inj (f₁ f₂ : L.Func k) : (⌜f₁⌝ : V) = (⌜f₂⌝ : V) ↔ f₁ = f₂ := by + simp [quote_func_def] + +@[simp] lemma quote_rel_inj (R₁ R₂ : L.Rel k) : (⌜R₁⌝ : V) = (⌜R₂⌝ : V) ↔ R₁ = R₂ := by + simp [quote_rel_def] + +@[simp] lemma coe_quote_func_nat (f : L.Func k) : ((⌜f⌝ : ℕ) : V) = (⌜f⌝ : V) := by + simp [quote_func_def] + +@[simp] lemma coe_quote_rel_nat (R : L.Rel k) : ((⌜R⌝ : ℕ) : V) = (⌜R⌝ : V) := by + simp [quote_rel_def] + end /-- TODO: move to Basic/Syntax/Language.lean-/ @@ -158,8 +170,12 @@ variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺 abbrev LOR : Arith.Language V := Language.codeIn ℒₒᵣ V +abbrev LOR.code : LDef := Language.lDef ℒₒᵣ + notation "⌜ℒₒᵣ⌝" => LOR +notation "p⌜ℒₒᵣ⌝" => LOR.code + variable (V) instance LOR.defined : (⌜ℒₒᵣ⌝ : Arith.Language V).Defined (Language.lDef ℒₒᵣ) := inferInstance diff --git a/Arithmetization/ISigmaOne/Metamath/Proof/Theory.lean b/Arithmetization/ISigmaOne/Metamath/Proof/Theory.lean index 6e3ed01..3834cda 100644 --- a/Arithmetization/ISigmaOne/Metamath/Proof/Theory.lean +++ b/Arithmetization/ISigmaOne/Metamath/Proof/Theory.lean @@ -25,6 +25,17 @@ def Language.IsFVFreeSemiterm (n t : V) : Prop := L.termShift n t = t def Language.IsFVFree (p : V) : Prop := L.Formula p ∧ L.shift p = p +section + +def _root_.LO.FirstOrder.Arith.LDef.isFVFreeDef (pL : LDef) : 𝚺₁-Semisentence 1 := + .mkSigma “p | !pL.isSemiformulaDef.sigma 0 p ∧ !pL.shiftDef p p” (by simp) + +lemma isFVFree_defined : 𝚺₁-Predicate (L.IsFVFree : V → Prop) via pL.isFVFreeDef := by + intro v; simp [LDef.isFVFreeDef, HSemiformula.val_sigma, (semiformula_defined L).df.iff, (shift_defined L).df.iff] + simp [Language.IsFVFree, eq_comm] + +end + variable {L} @[simp] lemma neg_iff : L.IsFVFree (L.neg p) ↔ L.IsFVFree p := by diff --git a/Arithmetization/Vorspiel/Lemmata.lean b/Arithmetization/Vorspiel/Lemmata.lean index 5972fa4..60531a1 100644 --- a/Arithmetization/Vorspiel/Lemmata.lean +++ b/Arithmetization/Vorspiel/Lemmata.lean @@ -243,6 +243,32 @@ instance : Structure.Monotone ℒₒᵣ M := ⟨ | 2, Language.Add.add => add_le_add (h 0) (h 1) | 2, Language.Mul.mul => mul_le_mul (h 0) (h 1) (by simp) (by simp)⟩ +@[simp] lemma zero_ne_add_one (x : M) : 0 ≠ x + (1 : M) := ne_of_lt (by simp) + +@[simp] lemma nat_cast_inj {n m : ℕ} : (n : M) = (m : M) ↔ n = m := by + induction' n with n ih + · cases m <;> simp + · cases m <;> simp + +@[simp] lemma coe_coe_lt {n m : ℕ} : (n : M) < (m : M) ↔ n < m := by + induction' n with n ih + · cases m <;> simp + · cases m <;> simp + +/-- TODO: move-/ +lemma coe_succ (x : ℕ) : ((x + 1 : ℕ) : M) = (x : M) + 1 := by simp + +variable (M) + +abbrev natCast : NatCast M := inferInstance + +variable {M} + +@[simp] lemma natCast_nat (n : ℕ) : @Nat.cast ℕ (natCast ℕ) n = n := by + induction n + · rfl + · unfold natCast; rw [coe_succ]; simp [*] + end end Arith