From e16aad78433d33f7da056b00f4bf16ef62c389e1 Mon Sep 17 00:00:00 2001 From: palalansouki Date: Fri, 23 Aug 2024 09:13:35 +0900 Subject: [PATCH] D3 --- Arithmetization/Basic/IOpen.lean | 2 + .../ISigmaOne/Metamath/Coding.lean | 190 +++++++++++------- .../Metamath/DerivabilityConditions/D1.lean | 14 +- .../Metamath/DerivabilityConditions/D3.lean | 38 ++-- .../ISigmaOne/Metamath/Formula/Typed.lean | 2 +- .../ISigmaOne/Metamath/Proof/Typed.lean | 42 ++-- .../ISigmaOne/Metamath/Theory/R.lean | 116 +++++------ .../Metamath/Theory/SigmaOneDefinable.lean | 4 +- .../ISigmaOne/Metamath/Theory/Theory.lean | 32 ++- lake-manifest.json | 2 +- 10 files changed, 243 insertions(+), 199 deletions(-) diff --git a/Arithmetization/Basic/IOpen.lean b/Arithmetization/Basic/IOpen.lean index d3c9fe7..596d03e 100644 --- a/Arithmetization/Basic/IOpen.lean +++ b/Arithmetization/Basic/IOpen.lean @@ -846,6 +846,8 @@ lemma nat_cast_pair (n m : ℕ) : (⟪n, m⟫ : ℕ) = ⟪(n : V), (m : V)⟫ := lemma nat_pair_eq (m n : ℕ) : ⟪n, m⟫ = Nat.pair n m := by simp [Arith.pair, Nat.pair]; congr +lemma pair_coe_eq_coe_pair (m n : ℕ) : ⟪n, m⟫ = (Nat.pair n m : V) := by simp [nat_cast_pair, nat_pair_eq] + end end LO.Arith diff --git a/Arithmetization/ISigmaOne/Metamath/Coding.lean b/Arithmetization/ISigmaOne/Metamath/Coding.lean index 4166eff..9053cf0 100644 --- a/Arithmetization/ISigmaOne/Metamath/Coding.lean +++ b/Arithmetization/ISigmaOne/Metamath/Coding.lean @@ -4,9 +4,39 @@ import Mathlib.Combinatorics.Colex namespace LO.FirstOrder -namespace Semiformula.Operator +variable {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] + +variable {ξ : Type*} [Encodable ξ] + +open Encodable + +namespace Semiterm + +lemma encode_eq_toNat (t : Semiterm L ξ n) : Encodable.encode t = toNat t := rfl -variable {L : Language} +lemma toNat_func {k} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : + toNat (func f v) = (Nat.pair 2 <| Nat.pair k <| Nat.pair (encode f) <| Matrix.vecToNat fun i ↦ toNat (v i)) + 1 := rfl + +@[simp] lemma encode_emb (t : Semiterm L Empty n) : Encodable.encode (Rew.emb t : Semiterm L ξ n) = Encodable.encode t := by + simp only [encode_eq_toNat] + induction t + · simp [toNat] + · contradiction + · simp [Rew.func, toNat_func, *] + +end Semiterm + +namespace Semiformula + +lemma encode_eq_toNat (p : Semiformula L ξ n) : Encodable.encode p = toNat p := rfl + +@[simp] lemma encode_emb (p : Semisentence L n) : Encodable.encode (Rew.emb.hom p : Semiformula L ξ n) = Encodable.encode p := by + simp [encode_eq_toNat] + induction p using rec' <;> simp [toNat, Rew.rel, Rew.nrel, *] + +end Semiformula + +namespace Semiformula.Operator lemma lt_eq [L.LT] (t u : Semiterm L ξ n) : LT.lt.operator ![t, u] = Semiformula.rel Language.LT.lt ![t, u] := by simp [operator, LT.sentence_eq, Rew.rel] @@ -73,6 +103,30 @@ lemma quote_matrix_succ (v : Fin (k + 1) → V) : · simp · simp [quote_matrix_succ, ih, cons_absolute] +lemma quote_eq_vecToNat (v : Fin k → ℕ) : ⌜v⌝ = Matrix.vecToNat v := by + induction k + case zero => simp + case succ k ih => + simp [quote_matrix_succ, Matrix.vecToNat, cons, nat_pair_eq, Function.comp, ih] + +section + +variable {α : Type*} [Encodable α] + +instance : GoedelQuote α V := ⟨fun x ↦ Encodable.encode x⟩ + +lemma quote_eq_coe_encode (x : α) : (⌜x⌝ : V) = Encodable.encode x := rfl + +@[simp] lemma quote_nat (n : ℕ) : (⌜n⌝ : V) = n := rfl + +lemma coe_quote (x : α) : ↑(⌜x⌝ : ℕ) = (⌜x⌝ : V) := by simp [quote_eq_coe_encode] + +@[simp] lemma quote_quote (x : α) : (⌜(⌜x⌝ : ℕ)⌝ : V) = ⌜x⌝ := by simp [quote_eq_coe_encode] + +lemma quote_eq_encode (x : α) : (⌜x⌝ : ℕ) = Encodable.encode x := by simp [quote_eq_coe_encode] + +end + end LO.Arith namespace LO.FirstOrder.Semiterm @@ -85,21 +139,17 @@ variable {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Enco variable (V) -def codeIn {n} : SyntacticSemiterm L n → V - | #z => ^#z - | &x => ^&x - | func (arity := k) f v => ^func (k : V) ⌜f⌝ ⌜fun i ↦ (v i).codeIn⌝ - -instance : GoedelQuote (SyntacticSemiterm L n) V := ⟨(·.codeIn V)⟩ +lemma quote_eq_toNat (t : SyntacticSemiterm L n) : (⌜t⌝ : V) = toNat t := rfl -lemma quote_syntacticSemiterm_def (t : SyntacticSemiterm L n) : ⌜t⌝ = t.codeIn V := rfl +lemma quote_bvar (z : Fin n) : ⌜(#z : SyntacticSemiterm L n)⌝ = ^#(z : V) := by + simp [quote_eq_toNat, toNat, qqBvar, ←nat_pair_eq, nat_cast_pair] -lemma quote_bvar (z : Fin n) : ⌜(#z : SyntacticSemiterm L n)⌝ = ^#(z : V) := rfl - -lemma quote_fvar (x : ℕ) : ⌜(&x : SyntacticSemiterm L n)⌝ = ^&(x : V) := rfl +lemma quote_fvar (x : ℕ) : ⌜(&x : SyntacticSemiterm L n)⌝ = ^&(x : V) := by + simp [quote_eq_toNat, toNat, qqFvar, ←nat_pair_eq, nat_cast_pair] 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 + ⌜func f v⌝ = ^func (k : V) ⌜f⌝ ⌜fun i ↦ ⌜v i⌝⌝ := by + simp [quote_eq_toNat, toNat, qqFunc, ←nat_pair_eq, nat_cast_pair, quote_func_def, quote_eq_vecToNat, ←quote_matrix_absolute] @[simp] lemma codeIn_inj {n} {t u : SyntacticSemiterm L n} : (⌜t⌝ : V) = ⌜u⌝ ↔ t = u := by induction t generalizing u @@ -130,6 +180,13 @@ lemma quote_func {k} (f : L.Func k) (v : Fin k → 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, *] +lemma quote_eq_encode (t : SyntacticSemiterm L n) : ⌜t⌝ = Encodable.encode t := by + induction t + case bvar z => simp [encode_eq_toNat, toNat, quote_bvar, qqBvar, nat_pair_eq] + case fvar z => simp [encode_eq_toNat, toNat, quote_fvar, qqFvar, nat_pair_eq] + case func k f v ih => + simp [encode_eq_toNat, toNat, quote_func, qqFunc, nat_pair_eq, quote_func_def, quote_eq_vecToNat, ih] + end LO.FirstOrder.Semiterm namespace LO.Arith @@ -242,32 +299,24 @@ variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] variable {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] -variable (V) - -def codeIn : {n : ℕ} → SyntacticSemiformula L n → V - | _, rel (arity := k) R v => ^rel (k : V) ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ - | _, nrel (arity := k) R v => ^nrel (k : V) ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ - | _, ⊤ => ^⊤ - | _, ⊥ => ^⊥ - | _, p ⋏ q => p.codeIn ^⋏ q.codeIn - | _, p ⋎ q => p.codeIn ^⋎ q.codeIn - | _, ∀' p => ^∀ p.codeIn - | _, ∃' p => ^∃ p.codeIn - -instance : GoedelQuote (SyntacticSemiformula L n) V := ⟨codeIn V⟩ - -lemma quote_syntacticSemiformula_def (p : SyntacticSemiformula L n) : ⌜p⌝ = p.codeIn V := rfl - -lemma quote_rel {k} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : - (⌜rel R v⌝ : V) = ^rel ↑k ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ := rfl -lemma quote_nrel {k} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : - (⌜nrel R v⌝ : V) = ^nrel ↑k ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ := rfl -lemma quote_verum (n : ℕ) : ⌜(⊤ : SyntacticSemiformula L n)⌝ = (^⊤ : V) := rfl -lemma quote_falsum (n : ℕ) : ⌜(⊥ : SyntacticSemiformula L n)⌝ = (^⊥ : V) := rfl -lemma quote_and (p q : SyntacticSemiformula L n) : (⌜p ⋏ q⌝ : V) = ⌜p⌝ ^⋏ ⌜q⌝ := rfl -lemma quote_or (p q : SyntacticSemiformula L n) : (⌜p ⋎ q⌝ : V) = ⌜p⌝ ^⋎ ⌜q⌝ := rfl -lemma quote_all (p : SyntacticSemiformula L (n + 1)) : (⌜∀' p⌝ : V) = ^∀ ⌜p⌝ := rfl -lemma quote_ex (p : SyntacticSemiformula L (n + 1)) : (⌜∃' p⌝ : V) = ^∃ ⌜p⌝ := rfl +lemma quote_eq_toNat (p : SyntacticSemiformula L n) : (⌜p⌝ : V) = toNat p := rfl + +lemma quote_rel {k} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : (⌜rel R v⌝ : V) = ^rel ↑k ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ := by + simp [Semiterm.quote_eq_toNat, quote_eq_toNat, toNat, qqRel, ←nat_pair_eq, nat_cast_pair, quote_rel_def, ←quote_eq_vecToNat]; rfl +lemma quote_nrel {k} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : (⌜nrel R v⌝ : V) = ^nrel ↑k ⌜R⌝ ⌜fun i ↦ ⌜v i⌝⌝ := by + simp [Semiterm.quote_eq_toNat, quote_eq_toNat, toNat, qqRel, ←nat_pair_eq, nat_cast_pair, quote_rel_def, ←quote_eq_vecToNat]; rfl +lemma quote_verum (n : ℕ) : ⌜(⊤ : SyntacticSemiformula L n)⌝ = (^⊤ : V) := by + simp [quote_eq_toNat, toNat, qqVerum, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] +lemma quote_falsum (n : ℕ) : ⌜(⊥ : SyntacticSemiformula L n)⌝ = (^⊥ : V) := by + simp [quote_eq_toNat, toNat, qqFalsum, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] +lemma quote_and (p q : SyntacticSemiformula L n) : (⌜p ⋏ q⌝ : V) = ⌜p⌝ ^⋏ ⌜q⌝ := by + simp [quote_eq_toNat, toNat, qqAnd, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] +lemma quote_or (p q : SyntacticSemiformula L n) : (⌜p ⋎ q⌝ : V) = ⌜p⌝ ^⋎ ⌜q⌝ := by + simp [quote_eq_toNat, toNat, qqOr, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] +lemma quote_all (p : SyntacticSemiformula L (n + 1)) : (⌜∀' p⌝ : V) = ^∀ ⌜p⌝ := by + simp [quote_eq_toNat, toNat, qqAll, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] +lemma quote_ex (p : SyntacticSemiformula L (n + 1)) : (⌜∃' p⌝ : V) = ^∃ ⌜p⌝ := by + simp [quote_eq_toNat, toNat, qqEx, pair_coe_eq_coe_pair, ←pair_coe_eq_coe_pair, nat_cast_pair] @[simp] lemma quote_eq (t u : SyntacticSemiterm ℒₒᵣ n) : (⌜Semiformula.rel Language.Eq.eq ![t, u]⌝ : V) = (⌜t⌝ ^= ⌜u⌝) := by simp [FirstOrder.Semiformula.quote_rel]; rfl @@ -328,27 +377,14 @@ lemma quote_ex (p : SyntacticSemiformula L (n + 1)) : (⌜∃' p⌝ : V) = ^∃ 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 ℒₒᵣ (SyntacticFormula L) := ⟨fun p ↦ Semiterm.Operator.numeral ℒₒᵣ ⌜p⌝⟩ - -instance : Semiterm.Operator.GoedelNumber ℒₒᵣ (Sentence L) := ⟨fun σ ↦ Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝⟩ +@[simp] lemma quote_semisentence_def (p : Semisentence L n) : ⌜(Rew.emb.hom p : SyntacticSemiformula L n)⌝ = (⌜p⌝ : V) := by + simp [quote_eq_coe_encode] lemma sentence_goedelNumber_def (σ : Sentence L) : - (⌜σ⌝ : Semiterm ℒₒᵣ ξ n) = Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝ := rfl + (⌜σ⌝ : Semiterm ℒₒᵣ ξ n) = Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝ := by simp [Arith.goedelNumber'_def, quote_eq_encode] lemma syntacticformula_goedelNumber_def (p : SyntacticFormula L) : - (⌜p⌝ : Semiterm ℒₒᵣ ξ n) = Semiterm.Operator.numeral ℒₒᵣ ⌜p⌝ := rfl + (⌜p⌝ : Semiterm ℒₒᵣ ξ n) = Semiterm.Operator.numeral ℒₒᵣ ⌜p⌝ := by simp [Arith.goedelNumber'_def, quote_eq_encode] end LO.FirstOrder.Semiformula @@ -466,19 +502,18 @@ instance {k n} : GoedelQuote (Fin k → SyntacticSemiterm L n) ((L.codeIn V).Sem @[simp] lemma vCodeIn'_val (v : Fin k → SyntacticSemiterm L n) : (⌜v⌝ : (L.codeIn V).SemitermVec k n).val = ⌜fun i ↦ ⌜v i⌝⌝ := rfl -@[simp] lemma codeIn'_bvar (z : Fin n) : (⌜(#z : SyntacticSemiterm L n)⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).bvar z := rfl -@[simp] lemma codeIn'_fvar (x : ℕ) : (⌜(&x : SyntacticSemiterm L n)⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).fvar x := rfl +@[simp] lemma codeIn'_bvar (z : Fin n) : (⌜(#z : SyntacticSemiterm L n)⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).bvar z := by ext; simp [quote_bvar] +@[simp] lemma codeIn'_fvar (x : ℕ) : (⌜(&x : SyntacticSemiterm L n)⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).fvar x := by ext; simp [quote_fvar] lemma codeIn'_func {k} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) : - (⌜func f v⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).func (k := k) (f := ⌜f⌝) (by simp) ⌜v⌝ := rfl - + (⌜func f v⌝ : (L.codeIn V).Semiterm n) = (L.codeIn V).func (k := k) (f := ⌜f⌝) (by simp) ⌜v⌝ := by ext; simp [quote_func, Language.func] @[simp] lemma codeIn'_zero (n : ℕ) : (⌜(func Language.Zero.zero ![] : SyntacticSemiterm ℒₒᵣ n)⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ↑(0 : V) := by ext; simp @[simp] lemma codeIn'_one (n : ℕ) : (⌜(func Language.One.one ![] : SyntacticSemiterm ℒₒᵣ n)⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ↑(1 : V) := by ext; simp @[simp] lemma codeIn'_add (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜func Language.Add.add v⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ⌜v 0⌝ + ⌜v 1⌝ := by ext; simp; rfl + (⌜func Language.Add.add v⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ⌜v 0⌝ + ⌜v 1⌝ := by ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [quote_add] @[simp] lemma codeIn'_mul (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜func Language.Mul.mul v⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ⌜v 0⌝ * ⌜v 1⌝ := by ext; simp; rfl + (⌜func Language.Mul.mul v⌝ : (Language.codeIn ℒₒᵣ V).Semiterm n) = ⌜v 0⌝ * ⌜v 1⌝ := by ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [quote_add] end Semiterm @@ -490,12 +525,12 @@ instance : GoedelQuote (SyntacticSemiformula L n) ((L.codeIn V).Semiformula n) : @[simp] lemma codeIn'_val (p : SyntacticSemiformula L n) : (⌜p⌝ : (L.codeIn V).Semiformula n).val = ⌜p⌝ := rfl -@[simp] lemma codeIn'_verum (n : ℕ) : (⌜(⊤ : SyntacticSemiformula L n)⌝ : (L.codeIn V).Semiformula n) = ⊤ := rfl -@[simp] lemma codeIn'_falsum (n : ℕ) : (⌜(⊥ : SyntacticSemiformula L n)⌝ : (L.codeIn V).Semiformula n) = ⊥ := rfl -@[simp] lemma codeIn'_and (p q : SyntacticSemiformula L n) : (⌜p ⋏ q⌝ : (L.codeIn V).Semiformula n) = ⌜p⌝ ⋏ ⌜q⌝ := rfl -@[simp] lemma codeIn'_or (p q : SyntacticSemiformula L n) : (⌜p ⋎ q⌝ : (L.codeIn V).Semiformula n) = ⌜p⌝ ⋎ ⌜q⌝ := rfl -@[simp] lemma codeIn'_all (p : SyntacticSemiformula L (n + 1)) : (⌜∀' p⌝ : (L.codeIn V).Semiformula n) = .all (.cast (n := ↑(n + 1)) ⌜p⌝) := rfl -@[simp] lemma codeIn'_ex (p : SyntacticSemiformula L (n + 1)) : (⌜∃' p⌝ : (L.codeIn V).Semiformula n) = .ex (.cast (n := ↑(n + 1)) ⌜p⌝) := rfl +@[simp] lemma codeIn'_verum (n : ℕ) : (⌜(⊤ : SyntacticSemiformula L n)⌝ : (L.codeIn V).Semiformula n) = ⊤ := by ext; simp [quote_verum] +@[simp] lemma codeIn'_falsum (n : ℕ) : (⌜(⊥ : SyntacticSemiformula L n)⌝ : (L.codeIn V).Semiformula n) = ⊥ := by ext; simp [quote_falsum] +@[simp] lemma codeIn'_and (p q : SyntacticSemiformula L n) : (⌜p ⋏ q⌝ : (L.codeIn V).Semiformula n) = ⌜p⌝ ⋏ ⌜q⌝ := by ext; simp [quote_and] +@[simp] lemma codeIn'_or (p q : SyntacticSemiformula L n) : (⌜p ⋎ q⌝ : (L.codeIn V).Semiformula n) = ⌜p⌝ ⋎ ⌜q⌝ := by ext; simp [quote_or] +@[simp] lemma codeIn'_all (p : SyntacticSemiformula L (n + 1)) : (⌜∀' p⌝ : (L.codeIn V).Semiformula n) = .all (.cast (n := ↑(n + 1)) ⌜p⌝) := by ext; simp [quote_all] +@[simp] lemma codeIn'_ex (p : SyntacticSemiformula L (n + 1)) : (⌜∃' p⌝ : (L.codeIn V).Semiformula n) = .ex (.cast (n := ↑(n + 1)) ⌜p⌝) := by ext; simp [quote_ex] @[simp] lemma codeIn'_neg (p : SyntacticSemiformula L n) : (⌜~p⌝ : (L.codeIn V).Semiformula n) = ~⌜p⌝ := by ext; simp [neg_quote] @[simp] lemma codeIn'_imp (p q : SyntacticSemiformula L n) : (⌜p ⟶ q⌝ : (L.codeIn V).Semiformula n) = ⌜p⌝ ⟶ ⌜q⌝ := by @@ -504,13 +539,17 @@ instance : GoedelQuote (SyntacticSemiformula L n) ((L.codeIn V).Semiformula n) : open LO.Arith Formalized @[simp] lemma codeIn'_eq (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜rel Language.Eq.eq v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ =' ⌜v 1⌝) := by ext; simp [Language.Semiterm.equals]; rfl + (⌜rel Language.Eq.eq v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ =' ⌜v 1⌝) := by + ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [Language.Semiterm.equals] @[simp] lemma codeIn'_neq (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜nrel Language.Eq.eq v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ ≠' ⌜v 1⌝) := by ext; simp [Language.Semiterm.notEquals]; rfl + (⌜nrel Language.Eq.eq v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ ≠' ⌜v 1⌝) := by + ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [Language.Semiterm.notEquals] @[simp] lemma codeIn'_lt (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜rel Language.LT.lt v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ <' ⌜v 1⌝) := by ext; simp [Language.Semiterm.lessThan]; rfl + (⌜rel Language.LT.lt v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ <' ⌜v 1⌝) := by + ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [Language.Semiterm.lessThan] @[simp] lemma codeIn'_nlt (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : - (⌜nrel Language.LT.lt v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ ≮' ⌜v 1⌝) := by ext; simp [Language.Semiterm.notLessThan]; rfl + (⌜nrel Language.LT.lt v⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = (⌜v 0⌝ ≮' ⌜v 1⌝) := by + ext; rw [Matrix.fun_eq_vec₂ (v := v)]; simp [Language.Semiterm.notLessThan] @[simp] lemma codeIn'_ball (t : SyntacticSemiterm ℒₒᵣ n) (p : SyntacticSemiformula ℒₒᵣ (n + 1)) : (⌜∀[“#0 < !!(Rew.bShift t)”] p⌝ : (Language.codeIn ℒₒᵣ V).Semiformula n) = Language.Semiformula.ball ⌜t⌝ (.cast (n := ↑(n + 1)) ⌜p⌝) := by ext; simp [LogicalConnective.ball, imp_eq, Language.Semiformula.cast, @@ -520,11 +559,12 @@ open LO.Arith Formalized ext; simp [LogicalConnective.bex, imp_eq, Language.Semiformula.cast, Language.Semiformula.ball, Semiformula.Operator.lt_eq, termBShift_quote] -instance : GoedelQuote (Sentence L) ((L.codeIn V).TFormula) := ⟨fun σ ↦ (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).Semiformula (0 : ℕ))⟩ +instance : GoedelQuote (Sentence L) ((L.codeIn V).Formula) := ⟨fun σ ↦ (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).Semiformula (0 : ℕ))⟩ -lemma quote_sentence_def' (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).TFormula) = (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).Semiformula (0 : ℕ)) := rfl +lemma quote_sentence_def' (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).Formula) = (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).Semiformula (0 : ℕ)) := rfl -@[simp] lemma quote_sentence_val (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).TFormula).val = ⌜σ⌝ := rfl +@[simp] lemma quote_sentence_val (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).Formula).val = ⌜σ⌝ := by + simp [quote_sentence_def', quote_eq_coe_encode] end Semiformula diff --git a/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D1.lean b/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D1.lean index 0f6d17c..80b615f 100644 --- a/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D1.lean +++ b/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D1.lean @@ -98,10 +98,10 @@ variable {T : SyntacticTheory L} [T.Δ₁Definable] open Classical -@[simp] lemma formulaSet_codeIn_finset (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).FormulaSet ⌜Γ⌝ := by +@[simp] lemma formulaSet_codeIn_finset (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).IsFormulaSet ⌜Γ⌝ := by intro x hx rcases Derivation3.Sequent.mem_codeIn hx with ⟨p, _, rfl⟩; - apply semiformula_quote + apply semiformula_quote (n := 0) open Derivation3 @@ -125,20 +125,20 @@ lemma quote_image_shift (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).setShi (by simpa [quote_verum] using (Sequent.mem_codeIn_iff (V := V)).mpr h) case and Δ p q hpq dp dq ihp ihq => apply Language.Theory.Derivation.andIntro - (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr hpq) + (by simpa [quote_and] 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.Theory.Derivation.orIntro - (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr hpq) + (by simpa [quote_or] using (Sequent.mem_codeIn_iff (V := V)).mpr hpq) ⟨by simp [fstidx_quote], ih⟩ case all Δ p h d ih => apply Language.Theory.Derivation.allIntro - (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr h) + (by simpa [quote_all] 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.Theory.Derivation.exIntro - (by simpa using (Sequent.mem_codeIn_iff (V := V)).mpr h) + (by simpa [quote_ex] 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 => @@ -167,7 +167,7 @@ section variable [L.ConstantInhabited] {T : Theory L} [T.Δ₁Definable] theorem provable_of_provable : T ⊢! p → (T.codeIn V).Provable ⌜p⌝ := fun h ↦ by - simpa [quote_semisentence_def] using derivable_of_quote (V := V) (provable_iff_derivable3'.mp h).some + simpa using derivable_of_quote (V := V) (provable_iff_derivable3'.mp h).some /-- Hilbert–Bernays provability condition D1 -/ theorem tprovable_of_provable : T ⊢! σ → T.tCodeIn V ⊢! ⌜σ⌝ := fun h ↦ by diff --git a/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D3.lean b/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D3.lean index 069ecf3..69cfefd 100644 --- a/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D3.lean +++ b/Arithmetization/ISigmaOne/Metamath/DerivabilityConditions/D3.lean @@ -21,11 +21,12 @@ namespace Formalized variable {T : LOR.TTheory (V := V)} [R₀Theory T] -def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).TSemitermVec n 0 := - ⟨⌜fun i ↦ numeral (e i)⌝, by simp, by +def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).SemitermVec n 0 := + ⟨⌜fun i ↦ numeral (e i)⌝, + Language.IsSemitermVec.iff.mpr <| ⟨by simp, by intro i hi rcases eq_fin_of_lt_nat hi with ⟨i, rfl⟩ - simp [quote_nth_fin (fun i ↦ numeral (e i)) i]⟩ + simp [quote_nth_fin (fun i ↦ numeral (e i)) i]⟩⟩ @[simp] lemma toNumVec_nil : (toNumVec (![] : Fin 0 → V)) = .nil _ _ := by ext; simp [toNumVec] @@ -38,26 +39,29 @@ def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).TSemitermVec calc (i : V) < (i : V) + (n - i : V) := by simp _ = (n : V) := by simp +@[simp] lemma len_semitermvec {L : Arith.Language V} {pL} [L.Defined pL] (v : L.SemitermVec k n) : len v.val = k := v.prop.lh + @[simp] lemma cast_substs_numVec (p : Semisentence ℒₒᵣ (n + 1)) : ((.cast (V := V) (n := ↑(n + 1)) (n' := ↑n + 1) ⌜Rew.embs.hom p⌝ (by simp)) ^/[(toNumVec e).q.substs (typedNumeral 0 x).sing]) = ⌜Rew.embs.hom p⌝ ^/[toNumVec (x :> e)] := by have : (toNumVec e).q.substs (typedNumeral 0 x).sing = x ∷ᵗ toNumVec e := by ext; simp apply nth_ext' ((↑n : V) + 1) - (by rw [len_termSubstVec]; simpa using (toNumVec e).prop.qVec) - (by simp [←(toNumVec e).prop.1]) + (by rw [len_termSubstVec]; simpa using (toNumVec e).prop.qVec.isUTerm) + (by simp [(toNumVec e).prop.lh]) intro i hi - rw [nth_termSubstVec (by simpa using (toNumVec e).prop.qVec) hi] + rw [nth_termSubstVec (by simpa using (toNumVec e).prop.qVec.isUTerm) hi] rcases zero_or_succ i with (rfl | ⟨i, rfl⟩) · simp [Language.qVec] - · simp only [Language.qVec, nth_cons_succ, Language.TSemitermVec.prop] + · simp only [Language.qVec, nth_cons_succ, Language.SemitermVec.prop] rcases eq_fin_of_lt_nat (by simpa using hi) with ⟨i, rfl⟩ - rw [nth_termBShiftVec (by simp)] - simp; exact coe_coe_lt (V := V) i + rw [nth_termBShiftVec (by simp), + toNumVec_val_nth, numeral_bShift, + numeral_substs (n := 1) (m := 0) (by simp)] + simp rw [this] ext; simp [toNumVec] - namespace TProof open Language.Theory.TProof System @@ -75,13 +79,13 @@ noncomputable def termEqComplete {n : ℕ} (e : Fin n → V) : Structure.add_eq_of_lang] have ih : T ⊢ (⌜Rew.embs (v 0)⌝^ᵗ/[toNumVec e] + ⌜Rew.embs (v 1)⌝^ᵗ/[toNumVec e]) =' (↑((v 0).valbm V e) + ↑((v 1).valbm V e)) := addExt T _ _ _ _ ⨀ termEqComplete e (v 0) ⨀ termEqComplete e (v 1) - have : T ⊢ ((v 0).valbm V e + (v 1).valbm V e : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑((v 0).valbm V e + (v 1).valbm V e) := addComplete T _ _ + have : T ⊢ ((v 0).valbm V e + (v 1).valbm V e : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑((v 0).valbm V e + (v 1).valbm V e) := addComplete T _ _ exact eqTrans T _ _ _ ⨀ ih ⨀ this | Semiterm.func Language.Mul.mul v => by simp [Rew.func, Semiterm.val_func] have ih : T ⊢ (⌜Rew.embs (v 0)⌝^ᵗ/[toNumVec e] * ⌜Rew.embs (v 1)⌝^ᵗ/[toNumVec e]) =' (↑((v 0).valbm V e) * ↑((v 1).valbm V e)) := mulExt T _ _ _ _ ⨀ termEqComplete e (v 0) ⨀ termEqComplete e (v 1) - have : T ⊢ ((v 0).valbm V e * (v 1).valbm V e : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑((v 0).valbm V e * (v 1).valbm V e) := mulComplete T _ _ + have : T ⊢ ((v 0).valbm V e * (v 1).valbm V e : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑((v 0).valbm V e * (v 1).valbm V e) := mulComplete T _ _ exact eqTrans T _ _ _ ⨀ ih ⨀ this lemma termEq_complete! {n : ℕ} (e : Fin n → V) (t : Semiterm ℒₒᵣ Empty n) : @@ -97,7 +101,7 @@ theorem bold_sigma₁_complete {n} {p : Semisentence ℒₒᵣ n} (hp : Hierarch case hFalsum => intro n simp only [LogicalConnective.HomClass.map_bot, Prop.bot_eq_false, - Semiformula.codeIn'_falsum, Language.TSemiformula.substs_falsum, false_implies, implies_true] + Semiformula.codeIn'_falsum, Language.Semiformula.substs_falsum, false_implies, implies_true] case hEQ => intro n t₁ t₂ e h have : t₁.valbm V e = t₂.valbm V e := by simpa using h @@ -122,15 +126,15 @@ theorem bold_sigma₁_complete {n} {p : Semisentence ℒₒᵣ n} (hp : Hierarch intro n p q hp hq ihp ihq e h have h : Semiformula.Evalbm V e p ∧ Semiformula.Evalbm V e q := by simpa using h simpa only [LogicalConnective.HomClass.map_and, Semiformula.codeIn'_and, - Language.TSemiformula.substs_and] using and_intro! (ihp h.1) (ihq h.2) + Language.Semiformula.substs_and] using and_intro! (ihp h.1) (ihq h.2) case hOr => intro n p q hp hq ihp ihq e h have : Semiformula.Evalbm V e p ∨ Semiformula.Evalbm V e q := by simpa using h rcases this with (h | h) · simpa only [LogicalConnective.HomClass.map_or, Semiformula.codeIn'_or, - Language.TSemiformula.substs_or] using or₁'! (ihp h) + Language.Semiformula.substs_or] using or₁'! (ihp h) · simpa only [LogicalConnective.HomClass.map_or, Semiformula.codeIn'_or, - Language.TSemiformula.substs_or] using or₂'! (ihq h) + Language.Semiformula.substs_or] using or₂'! (ihq h) case hBall => intro n t p hp ihp e h simp only [Rew.ball, Rew.q_emb, Rew.hom_finitary2, Rew.emb_bvar, ← Rew.emb_bShift_term, @@ -145,7 +149,7 @@ theorem bold_sigma₁_complete {n} {p : Semisentence ℒₒᵣ n} (hp : Hierarch exact ihp this case hEx => intro n p hp ihp e h - simp only [Rew.ex, Rew.q_emb, Semiformula.codeIn'_ex, Language.TSemiformula.substs_ex] + simp only [Rew.ex, Rew.q_emb, Semiformula.codeIn'_ex, Language.Semiformula.substs_ex] have : ∃ x, Semiformula.Evalbm V (x :> e) p := by simpa using h rcases this with ⟨x, hx⟩ apply ex! x diff --git a/Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean b/Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean index 04a5c5c..7511964 100644 --- a/Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean +++ b/Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean @@ -37,7 +37,7 @@ structure Language.Semiformula (n : V) where attribute [simp] Language.Semiformula.prop -abbrev Language.TFormula := L.Semiformula 0 +abbrev Language.Formula := L.Semiformula 0 variable {L} diff --git a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean index ad3aeee..c80cd6b 100644 --- a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean +++ b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean @@ -20,9 +20,9 @@ variable {L : Arith.Language V} {pL : LDef} [Arith.Language.Defined L pL] section typed_formula -abbrev Language.Semiformula.substs₁ (p : L.Semiformula (0 + 1)) (t : L.Term) : L.TFormula := p.substs t.sing +abbrev Language.Semiformula.substs₁ (p : L.Semiformula (0 + 1)) (t : L.Term) : L.Formula := p.substs t.sing -abbrev Language.Semiformula.free (p : L.Semiformula (0 + 1)) : L.TFormula := p.shift.substs₁ (L.fvar 0) +abbrev Language.Semiformula.free (p : L.Semiformula (0 + 1)) : L.Formula := p.shift.substs₁ (L.fvar 0) @[simp] lemma Language.Semiformula.val_substs₁ (p : L.Semiformula (0 + 1)) (t : L.Term) : (p.substs₁ t).val = L.substs ?[t.val] p.val := by simp [substs₁, substs] @@ -43,7 +43,7 @@ end typed_formula section typed_theory -abbrev Language.Theory.tmem (p : L.TFormula) (T : L.Theory) : Prop := p.val ∈ T +abbrev Language.Theory.tmem (p : L.Formula) (T : L.Theory) : Prop := p.val ∈ T scoped infix:50 " ∈' " => Language.Theory.tmem @@ -63,13 +63,13 @@ variable {L} instance : EmptyCollection L.Sequent := ⟨⟨∅, by simp⟩⟩ -instance : Singleton L.TFormula L.Sequent := ⟨fun p ↦ ⟨{p.val}, by simp⟩⟩ +instance : Singleton L.Formula L.Sequent := ⟨fun p ↦ ⟨{p.val}, by simp⟩⟩ -instance : Insert L.TFormula L.Sequent := ⟨fun p Γ ↦ ⟨insert p.val Γ.val, by simp⟩⟩ +instance : Insert L.Formula L.Sequent := ⟨fun p Γ ↦ ⟨insert p.val Γ.val, by simp⟩⟩ instance : Union L.Sequent := ⟨fun Γ Δ ↦ ⟨Γ.val ∪ Δ.val, by simp⟩⟩ -instance : Membership L.TFormula L.Sequent := ⟨(·.val ∈ ·.val)⟩ +instance : Membership L.Formula L.Sequent := ⟨(·.val ∈ ·.val)⟩ instance : HasSubset L.Sequent := ⟨(·.val ⊆ ·.val)⟩ @@ -77,7 +77,7 @@ scoped infixr:50 " ⫽ " => Insert.insert namespace Language.Sequent -variable {Γ Δ : L.Sequent} {p q : L.TFormula} +variable {Γ Δ : L.Sequent} {p q : L.Formula} lemma mem_iff : p ∈ Γ ↔ p.val ∈ Γ.val := iff_of_eq rfl @@ -85,13 +85,13 @@ lemma subset_iff : Γ ⊆ Δ ↔ Γ.val ⊆ Δ.val := iff_of_eq rfl @[simp] lemma val_empty : (∅ : L.Sequent).val = ∅ := rfl -@[simp] lemma val_singleton (p : L.TFormula) : ({p} : L.Sequent).val = {p.val} := rfl +@[simp] lemma val_singleton (p : L.Formula) : ({p} : L.Sequent).val = {p.val} := rfl -@[simp] lemma val_insert (p : L.TFormula) (Γ : L.Sequent) : (insert p Γ).val = insert p.val Γ.val := rfl +@[simp] lemma val_insert (p : L.Formula) (Γ : L.Sequent) : (insert p Γ).val = insert p.val Γ.val := rfl @[simp] lemma val_union (Γ Δ : L.Sequent) : (Γ ∪ Δ).val = Γ.val ∪ Δ.val := rfl -@[simp] lemma not_mem_empty (p : L.TFormula) : p ∉ (∅ : L.Sequent) := by simp [mem_iff] +@[simp] lemma not_mem_empty (p : L.Formula) : p ∉ (∅ : L.Sequent) := by simp [mem_iff] @[simp] lemma mem_singleton_iff : p ∈ ({q} : L.Sequent) ↔ p = q := by simp [mem_iff, Language.Semiformula.val_inj] @@ -137,9 +137,9 @@ structure Language.Theory.TDerivation (T : Language.TTheory L) (Γ : L.Sequent) scoped infix:45 " ⊢¹ " => Language.Theory.TDerivation -def Language.Theory.TProof (T : Language.TTheory L) (p : L.TFormula) := T ⊢¹ insert p ∅ +def Language.Theory.TProof (T : Language.TTheory L) (p : L.Formula) := T ⊢¹ insert p ∅ -instance : System L.TFormula L.TTheory := ⟨Language.Theory.TProof⟩ +instance : System L.Formula L.TTheory := ⟨Language.Theory.TProof⟩ variable {T : L.TTheory} @@ -150,7 +150,7 @@ def Language.Theory.Derivable.toTDerivation (Γ : L.Sequent) (h : T.thy.Derivabl lemma Language.Theory.TDerivation.toDerivable {Γ : L.Sequent} (d : T ⊢¹ Γ) : T.thy.Derivable Γ.val := ⟨d.derivation, d.derivationOf⟩ -lemma Language.Theory.TProvable.iff_provable {σ : L.TFormula} : +lemma Language.Theory.TProvable.iff_provable {σ : L.Formula} : T ⊢! σ ↔ T.thy.Provable σ.val := by constructor · intro b @@ -164,7 +164,7 @@ def Language.Theory.TProof.toTDerivation {p} (d : T ⊢ p) : T ⊢¹ insert p namespace Language.Theory.TDerivation -variable {Γ Δ : L.Sequent} {p q p₀ p₁ p₂ p₃ p₄ : L.TFormula} +variable {Γ Δ : L.Sequent} {p q p₀ p₁ p₂ p₃ p₄ : L.Formula} def byAxm (p) (h : p ∈' T.thy) (hΓ : p ∈ Γ) : T ⊢¹ Γ := Language.Theory.Derivable.toTDerivation _ @@ -256,12 +256,12 @@ end Language.Theory.TDerivation namespace Language.Theory.TProof -variable {T : L.TTheory} {p q : L.TFormula} +variable {T : L.TTheory} {p q : L.Formula} /-- Condition D2 -/ def modusPonens (d : T ⊢ p ⟶ q) (b : T ⊢ p) : T ⊢ q := TDerivation.modusPonens d b -def byAxm {p : L.TFormula} (h : p ∈' T.thy) : T ⊢ p := TDerivation.byAxm p h (by simp) +def byAxm {p : L.Formula} (h : p ∈' T.thy) : T ⊢ p := TDerivation.byAxm p h (by simp) instance : System.ModusPonens T := ⟨modusPonens⟩ @@ -379,22 +379,22 @@ def conjOr' (ps : L.SemiformulaVec 0) (q) (ds : ∀ i, (hi : i < len ps.val) → def disj (ps : L.SemiformulaVec 0) {i} (hi : i < len ps.val) (d : T ⊢ ps.nth i hi) : T ⊢ ps.disj := TDerivation.disj ps hi d -def shift {p : L.TFormula} (d : T ⊢ p) : T ⊢ p.shift := by simpa using TDerivation.shift d +def shift {p : L.Formula} (d : T ⊢ p) : T ⊢ p.shift := by simpa using TDerivation.shift d -lemma shift! {p : L.TFormula} (d : T ⊢! p) : T ⊢! p.shift := ⟨by simpa using TDerivation.shift d.get⟩ +lemma shift! {p : L.Formula} (d : T ⊢! p) : T ⊢! p.shift := ⟨by simpa using TDerivation.shift d.get⟩ def all {p : L.Semiformula (0 + 1)} (dp : T ⊢ p.free) : T ⊢ p.all := TDerivation.all (by simpa using dp) lemma all! {p : L.Semiformula (0 + 1)} (dp : T ⊢! p.free) : T ⊢! p.all := ⟨all dp.get⟩ -def generalizeAux {C : L.TFormula} {p : L.Semiformula (0 + 1)} (dp : T ⊢ C.shift ⟶ p.free) : T ⊢ C ⟶ p.all := by +def generalizeAux {C : L.Formula} {p : L.Semiformula (0 + 1)} (dp : T ⊢ C.shift ⟶ p.free) : T ⊢ C ⟶ p.all := by rw [Semiformula.imp_def] at dp ⊢ apply TDerivation.or apply TDerivation.rotate₁ apply TDerivation.all exact TDerivation.wk (TDerivation.orInv dp) (by intro x; simp; tauto) -lemma conj_shift (Γ : List L.TFormula) : (⋀Γ).shift = ⋀(Γ.map .shift) := by +lemma conj_shift (Γ : List L.Formula) : (⋀Γ).shift = ⋀(Γ.map .shift) := by induction Γ using List.induction_with_singleton case hnil => simp case hsingle => simp [List.conj₂] @@ -408,7 +408,7 @@ def generalize {Γ} {p : L.Semiformula (0 + 1)} (d : Γ.map .shift ⊢[T] p.free lemma generalize! {Γ} {p : L.Semiformula (0 + 1)} (d : Γ.map .shift ⊢[T]! p.free) : Γ ⊢[T]! p.all := ⟨generalize d.get⟩ -def specializeWithCtxAux {C : L.TFormula} {p : L.Semiformula (0 + 1)} (d : T ⊢ C ⟶ p.all) (t : L.Term) : T ⊢ C ⟶ p.substs₁ t := by +def specializeWithCtxAux {C : L.Formula} {p : L.Semiformula (0 + 1)} (d : T ⊢ C ⟶ p.all) (t : L.Term) : T ⊢ C ⟶ p.substs₁ t := by rw [Semiformula.imp_def] at d ⊢ apply TDerivation.or apply TDerivation.rotate₁ diff --git a/Arithmetization/ISigmaOne/Metamath/Theory/R.lean b/Arithmetization/ISigmaOne/Metamath/Theory/R.lean index bca9f29..9ee82d4 100644 --- a/Arithmetization/ISigmaOne/Metamath/Theory/R.lean +++ b/Arithmetization/ISigmaOne/Metamath/Theory/R.lean @@ -35,15 +35,15 @@ variable {V} class EQTheory (T : LOR.TTheory (V := V)) where refl : T ⊢ (#'0 =' #'0).all - replace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all + replace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all -abbrev oneAbbrev {n} : ⌜ℒₒᵣ⌝[V].TSemiterm n := (1 : V) +abbrev oneAbbrev {n} : ⌜ℒₒᵣ⌝[V].Semiterm n := (1 : V) scoped notation "^1" => oneAbbrev class R₀Theory (T : LOR.TTheory (V := V)) extends EQTheory T where - add (n m : V) : T ⊢ (n + m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n + m) - mul (n m : V) : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n * m) + add (n m : V) : T ⊢ (n + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n + m) + mul (n m : V) : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n * m) ne {n m : V} : n ≠ m → T ⊢ ↑n ≠' ↑m ltNumeral (n : V) : T ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all /- @@ -65,22 +65,22 @@ section EQTheory variable [EQTheory T] -def eqRefl (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t =' t := by +def eqRefl (t : ⌜ℒₒᵣ⌝.Term) : T ⊢ t =' t := by have : T ⊢ (#'0 =' #'0).all := EQTheory.refl - simpa [Language.TSemiformula.substs₁] using specialize this t + simpa [Language.Semiformula.substs₁] using specialize this t -lemma eq_refl! (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t =' t := ⟨eqRefl T t⟩ +lemma eq_refl! (t : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' t := ⟨eqRefl T t⟩ -noncomputable def replace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : +noncomputable def replace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := by have : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all := EQTheory.replace p have := by simpa using specialize this t - simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁, + simpa [Language.SemitermVec.q_of_pos, Language.Semiformula.substs₁, Language.TSemifromula.substs_substs] using specialize this u -lemma replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := ⟨replace T p t u⟩ +lemma replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := ⟨replace T p t u⟩ -def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₁ := by +def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₁ := by apply deduct' let Γ := [t₁ =' t₂] have e₁ : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm (by simp [Γ]) @@ -89,11 +89,11 @@ def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' simpa using replace T (#'0 =' t₁.bShift) t₁ t₂ exact this ⨀ e₁ ⨀ e₂ -lemma eq_symm! (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₁ := ⟨eqSymm T t₁ t₂⟩ +lemma eq_symm! (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₁ := ⟨eqSymm T t₁ t₂⟩ -lemma eq_symm'! {t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm} (h : T ⊢! t₁ =' t₂) : T ⊢! t₂ =' t₁ := eq_symm! T t₁ t₂ ⨀ h +lemma eq_symm'! {t₁ t₂ : ⌜ℒₒᵣ⌝.Term} (h : T ⊢! t₁ =' t₂) : T ⊢! t₂ =' t₁ := eq_symm! T t₁ t₂ ⨀ h -def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := by +def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := by apply deduct' apply deduct let Γ := [t₂ =' t₃, t₁ =' t₂] @@ -103,9 +103,9 @@ def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t simpa using replace T (t₁.bShift =' #'0) t₂ t₃ exact this ⨀ e₂ ⨀ e₁ -lemma eq_trans! (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := ⟨eqTrans T t₁ t₂ t₃⟩ +lemma eq_trans! (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := ⟨eqTrans T t₁ t₂ t₃⟩ -noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := by +noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := by apply deduct' apply deduct let Γ := [u₁ =' u₂, t₁ =' t₂] @@ -120,9 +120,9 @@ noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t simpa using this exact of (Γ := Γ) this ⨀ bu ⨀ b -lemma add_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := ⟨addExt T t₁ t₂ u₁ u₂⟩ +lemma add_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := ⟨addExt T t₁ t₂ u₁ u₂⟩ -noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := by +noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := by apply deduct' apply deduct let Γ := [u₁ =' u₂, t₁ =' t₂] @@ -137,9 +137,9 @@ noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t simpa using this exact of (Γ := Γ) this ⨀ bu ⨀ b -lemma mul_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := ⟨mulExt T t₁ t₂ u₁ u₂⟩ +lemma mul_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := ⟨mulExt T t₁ t₂ u₁ u₂⟩ -noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ := by +noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ := by apply deduct' apply deduct apply deduct @@ -150,10 +150,10 @@ noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t have e3 : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm (by simp [Γ]) exact (of <| eqTrans T t₂ u₁ u₂) ⨀ ((of <| eqTrans T t₂ t₁ u₁) ⨀ e1 ⨀ e2) ⨀ e3 -lemma eq_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ := +lemma eq_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ := ⟨eqExt T t₁ t₂ u₁ u₂⟩ -noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ := by +noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ := by apply deduct' apply deduct apply deduct @@ -169,10 +169,10 @@ noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t simpa using replace T (t₂.bShift ≠' #'0) u₁ u₂ exact of (Γ := Γ) this ⨀ bu ⨀ b -lemma ne_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ := +lemma ne_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ := ⟨neExt T t₁ t₂ u₁ u₂⟩ -noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := by +noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := by apply deduct' apply deduct apply deduct @@ -189,9 +189,9 @@ noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t simpa using this exact of (Γ := Γ) this ⨀ bu ⨀ b -lemma lt_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := ⟨ltExt T t₁ t₂ u₁ u₂⟩ +lemma lt_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := ⟨ltExt T t₁ t₂ u₁ u₂⟩ -noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := by +noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := by apply deduct' apply deduct apply deduct @@ -208,20 +208,20 @@ noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t simpa using this exact of (Γ := Γ) this ⨀ bu ⨀ b -lemma nlt_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := ⟨nltExt T t₁ t₂ u₁ u₂⟩ +lemma nlt_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := ⟨nltExt T t₁ t₂ u₁ u₂⟩ -noncomputable def ballReplace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : +noncomputable def ballReplace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ t =' u ⟶ p.ball t ⟶ p.ball u := by simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).ball #'0) t u -lemma ball_replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : +lemma ball_replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' u ⟶ p.ball t ⟶ p.ball u := ⟨ballReplace T p t u⟩ -noncomputable def bexReplace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : +noncomputable def bexReplace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ t =' u ⟶ p.bex t ⟶ p.bex u := by simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).bex #'0) t u -lemma bex_replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : +lemma bex_replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' u ⟶ p.bex t ⟶ p.bex u := ⟨bexReplace T p t u⟩ def eqComplete {n m : V} (h : n = m) : T ⊢ ↑n =' ↑m := by @@ -236,20 +236,20 @@ end EQTheory section Q₀ class Q₀Theory (T : LOR.TTheory (V := V)) extends EQTheory T where - add_zero : T ⊢ ((#'0 + ((0 : V) : ⌜ℒₒᵣ⌝[V].TSemiterm (0 + 1)) : ⌜ℒₒᵣ⌝[V].TSemiterm (0 + 1)) =' #'0).all - add_succ : T ⊢ ((#'1 + (#'0 + ((1 : V) : ⌜ℒₒᵣ⌝[V].TSemiterm 2))) =' ((#'1 + #'0) + ((1 : V) : ⌜ℒₒᵣ⌝[V].TSemiterm 2))).all.all - mul : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n * m) + add_zero : T ⊢ ((#'0 + ((0 : V) : ⌜ℒₒᵣ⌝[V].Semiterm (0 + 1)) : ⌜ℒₒᵣ⌝[V].Semiterm (0 + 1)) =' #'0).all + add_succ : T ⊢ ((#'1 + (#'0 + ((1 : V) : ⌜ℒₒᵣ⌝[V].Semiterm 2))) =' ((#'1 + #'0) + ((1 : V) : ⌜ℒₒᵣ⌝[V].Semiterm 2))).all.all + mul : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n * m) ne {n m : V} : n ≠ m → T ⊢ ↑n ≠' ↑m - ltNumeral (n : V) : T ⊢ (#'1 <' (#'0 + ((1 : V) : ⌜ℒₒᵣ⌝[V].TSemiterm 2)) ⟷ #'1 =' #'0 ⋎ #'1 <' #'0).all.all + ltNumeral (n : V) : T ⊢ (#'1 <' (#'0 + ((1 : V) : ⌜ℒₒᵣ⌝[V].Semiterm 2)) ⟷ #'1 =' #'0 ⋎ #'1 <' #'0).all.all variable [Q₀Theory T] -lemma add_zero (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! (t + ((0 : V) : ⌜ℒₒᵣ⌝[V].TSemiterm 0) : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' t := ⟨by +lemma add_zero (t : ⌜ℒₒᵣ⌝.Term) : T ⊢! (t + ((0 : V) : ⌜ℒₒᵣ⌝[V].Semiterm 0) : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' t := ⟨by simpa using specialize (Q₀Theory.add_zero (T := T)) t⟩ -lemma addssss (n m : V) : T ⊢! (n + m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n + m) := by { +lemma addssss (n m : V) : T ⊢! (n + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n + m) := by { revert n m - let d : ∀ n m : V, m ≤ n → T ⊢! ((n - m : V) + m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' n := by { + let d : ∀ n m : V, m ≤ n → T ⊢! ((n - m : V) + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' n := by { intro n m hmn induction m using induction_sigma1 · sorry -- simp [Language.Theory.TProvable.iff_provable]; definability @@ -271,23 +271,23 @@ section R₀ variable [R₀Theory T] -def addComplete (n m : V) : T ⊢ (n + m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n + m) := R₀Theory.add n m +def addComplete (n m : V) : T ⊢ (n + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n + m) := R₀Theory.add n m -lemma add_complete! (n m : V) : T ⊢! (n + m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n + m) := ⟨addComplete T n m⟩ +lemma add_complete! (n m : V) : T ⊢! (n + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n + m) := ⟨addComplete T n m⟩ -def mulComplete (n m : V) : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n * m) := R₀Theory.mul n m +def mulComplete (n m : V) : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n * m) := R₀Theory.mul n m -lemma mul_complete! (n m : V) : T ⊢! (n * m : ⌜ℒₒᵣ⌝[V].TSemiterm 0) =' ↑(n * m) := ⟨mulComplete T n m⟩ +lemma mul_complete! (n m : V) : T ⊢! (n * m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n * m) := ⟨mulComplete T n m⟩ def neComplete {n m : V} (h : n ≠ m) : T ⊢ ↑n ≠' ↑m := R₀Theory.ne h lemma ne_complete! {n m : V} (h : n ≠ m) : T ⊢! ↑n ≠' ↑m := ⟨neComplete T h⟩ -def ltNumeral (t : ⌜ℒₒᵣ⌝.TTerm) (n : V) : T ⊢ t <' ↑n ⟷ (tSubstItr t.sing (#'1 =' #'0) n).disj := by +def ltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t <' ↑n ⟷ (tSubstItr t.sing (#'1 =' #'0) n).disj := by have : T ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := R₀Theory.ltNumeral n - simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t + simpa [Language.SemitermVec.q_of_pos, Language.Semiformula.substs₁] using specialize this t -noncomputable def nltNumeral (t : ⌜ℒₒᵣ⌝.TTerm) (n : V) : T ⊢ t ≮' ↑n ⟷ (tSubstItr t.sing (#'1 ≠' #'0) n).conj := by +noncomputable def nltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t ≮' ↑n ⟷ (tSubstItr t.sing (#'1 ≠' #'0) n).conj := by simpa using negReplaceIff' <| ltNumeral T t n def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by @@ -299,7 +299,7 @@ def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by lemma lt_complete! {n m : V} (h : n < m) : T ⊢! ↑n <' ↑m := ⟨ltComplete T h⟩ noncomputable def nltComplete {n m : V} (h : m ≤ n) : T ⊢ ↑n ≮' ↑m := by - have : T ⊢ ↑n ≮' ↑m ⟷ (tSubstItr (↑n : ⌜ℒₒᵣ⌝.TTerm).sing (#'1 ≠' #'0) m).conj := by + have : T ⊢ ↑n ≮' ↑m ⟷ (tSubstItr (↑n : ⌜ℒₒᵣ⌝.Term).sing (#'1 ≠' #'0) m).conj := by simpa using negReplaceIff' <| ltNumeral T n m refine andRight this ⨀ ?_ apply conj' @@ -310,38 +310,38 @@ noncomputable def nltComplete {n m : V} (h : m ≤ n) : T ⊢ ↑n ≮' ↑m := lemma nlt_complete {n m : V} (h : m ≤ n) : T ⊢! ↑n ≮' ↑m := ⟨nltComplete T h⟩ -noncomputable def ballIntro (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) - (bs : ∀ i < n, T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) : +noncomputable def ballIntro (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) + (bs : ∀ i < n, T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) : T ⊢ p.ball ↑n := by apply all suffices T ⊢ &'0 ≮' ↑n ⋎ p.shift^/[(&'0).sing] by - simpa [Language.TSemiformula.free, Language.TSemiformula.substs₁] + simpa [Language.Semiformula.free, Language.Semiformula.substs₁] have : T ⊢ (tSubstItr (&'0).sing (#'1 ≠' #'0) n).conj ⋎ p.shift^/[(&'0).sing] := by apply conjOr' intro i hi have hi : i < n := by simpa using hi let Γ := [&'0 =' typedNumeral 0 i] suffices Γ ⊢[T] p.shift^/[(&'0).sing] by - simpa [nth_tSubstItr', hi, Language.TSemiformula.imp_def] using deduct' this + simpa [nth_tSubstItr', hi, Language.Semiformula.imp_def] using deduct' this have e : Γ ⊢[T] ↑i =' &'0 := of (eqSymm T &'0 ↑i) ⨀ (FiniteContext.byAxm <| by simp [Γ]) - have : T ⊢ p.shift^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing] := by + have : T ⊢ p.shift^/[(i : ⌜ℒₒᵣ⌝.Term).sing] := by simpa [Language.TSemifromula.shift_substs] using shift (bs i hi) exact of (replace T p.shift ↑i &'0) ⨀ e ⨀ of this exact orReplaceLeft' this (andRight (nltNumeral T (&'0) n)) -lemma ball_intro! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) - (bs : ∀ i < n, T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) : +lemma ball_intro! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) + (bs : ∀ i < n, T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) : T ⊢! p.ball ↑n := ⟨ballIntro T p n fun i hi ↦ (bs i hi).get⟩ -noncomputable def bexIntro (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) {i} - (hi : i < n) (b : T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) : +noncomputable def bexIntro (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i} + (hi : i < n) (b : T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) : T ⊢ p.bex ↑n := by apply ex i - suffices T ⊢ i <' n ⋏ p^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing] by simpa + suffices T ⊢ i <' n ⋏ p^/[(i : ⌜ℒₒᵣ⌝.Term).sing] by simpa exact System.andIntro (ltComplete T hi) b -lemma bex_intro! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) {i} - (hi : i < n) (b : T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) : +lemma bex_intro! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i} + (hi : i < n) (b : T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) : T ⊢! p.bex ↑n := ⟨bexIntro T p n hi b.get⟩ end R₀ diff --git a/Arithmetization/ISigmaOne/Metamath/Theory/SigmaOneDefinable.lean b/Arithmetization/ISigmaOne/Metamath/Theory/SigmaOneDefinable.lean index 30d1277..7d46d79 100644 --- a/Arithmetization/ISigmaOne/Metamath/Theory/SigmaOneDefinable.lean +++ b/Arithmetization/ISigmaOne/Metamath/Theory/SigmaOneDefinable.lean @@ -17,7 +17,7 @@ def _root_.LO.FirstOrder.SyntacticTheory.tDef (T : SyntacticTheory L) [d : T.Δ abbrev _root_.LO.FirstOrder.Theory.tDef (T : Theory L) [d : T.Δ₁Definable] : Arith.LDef.TDef L.lDef := d.toTDef -variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] +variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] variable {T : SyntacticTheory L} [T.Δ₁Definable] @@ -34,7 +34,7 @@ lemma Language.SyntacticTheory.codeIn_iff : x ∈ T.codeIn V ↔ V ⊧/![x] T.tD lemma mem_coded_theory {σ} (h : σ ∈ T) : ⌜σ⌝ ∈ T.codeIn V := Language.SyntacticTheory.codeIn_iff.mpr <| by have := consequence_iff_add_eq.mp (sound! <| SyntacticTheory.Δ₁Definable.mem_iff.mp h) V inferInstance - simpa [models_iff, Semiformula.syntacticformula_goedelNumber_def, numeral_eq_natCast] using this + simpa [models_iff, coe_quote, Semiformula.syntacticformula_goedelNumber_def, numeral_eq_natCast] using this instance tDef_defined : (T.codeIn V).Defined T.tDef where defined := ⟨by diff --git a/Arithmetization/ISigmaOne/Metamath/Theory/Theory.lean b/Arithmetization/ISigmaOne/Metamath/Theory/Theory.lean index e91f32e..92d90eb 100644 --- a/Arithmetization/ISigmaOne/Metamath/Theory/Theory.lean +++ b/Arithmetization/ISigmaOne/Metamath/Theory/Theory.lean @@ -99,7 +99,7 @@ def Language.Theory.singletonDef (p : FirstOrder.SyntacticFormula L) : L.lDef.TD ch := .ofZero (.mkSigma “x | x = ↑⌜p⌝” (by simp)) _ instance const_defined_const (p : FirstOrder.SyntacticFormula L) : (Language.Theory.singleton V L p).Defined (Language.Theory.singletonDef p) where - defined := .of_zero (by intro v; simp [numeral_eq_natCast]) + defined := .of_zero (by intro v; simp [numeral_eq_natCast, coe_quote]) end @@ -142,8 +142,8 @@ instance scheme_defined_scheme (φ : L.Scheme) {ps : pL.SchemeDef} [φ.Defined p (Language.Scheme.Defined.defined (V := V) (φ := φ)).df.iff, eq_comm]⟩ def Language.Craig.toScheme {L : Arith.Language V} {pL : LDef} [Arith.Language.Defined L pL] (c : L.Craig) : L.Scheme where - scheme (x) := c.core x ^⋏ qqVerums 0 x - increasing (x) := le_trans (le_qqVerums 0 x) (le_of_lt <| by simp) + scheme (x) := c.core x ^⋏ qqVerums x + increasing (x) := le_trans (le_qqVerums x) (le_of_lt <| by simp) structure _root_.LO.FirstOrder.Arith.LDef.CraigDef (pL : LDef) where core : 𝚺₁.Semisentence 2 @@ -152,7 +152,7 @@ class Language.Craig.Defined (φ : L.Craig) (ps : outParam pL.CraigDef) : Prop w defined : 𝚺₁-Function₁ φ.core via ps.core def _root_.LO.FirstOrder.Arith.LDef.CraigDef.toSchemeDef {pL : LDef} (c : pL.CraigDef) : pL.SchemeDef where - core := .mkSigma “p x | ∃ p', !c.core p' x ∧ ∃ vs, !qqVerumsDef vs 0 x ∧ !qqAndDef p 0 p' vs” (by simp) + core := .mkSigma “p x | ∃ p', !c.core p' x ∧ ∃ vs, !qqVerumsDef vs x ∧ !qqAndDef p p' vs” (by simp) instance (φ : L.Craig) (c : pL.CraigDef) [φ.Defined c] : φ.toScheme.Defined c.toSchemeDef where defined := by intro v; simp [Language.Craig.toScheme, Arith.LDef.CraigDef.toSchemeDef, (Language.Craig.Defined.defined (φ := φ)).df.iff] @@ -191,22 +191,22 @@ section thEQ def eqRefl : ⌜ℒₒᵣ⌝[V].Theory := Language.Theory.singleton V ℒₒᵣ “∀ x, x = x” def eqReplaceC : ⌜ℒₒᵣ⌝[V].Craig where - core := fun p ↦ if ⌜ℒₒᵣ⌝.Semiformula 1 p then ^∀[0] ^∀[1] (^#1 ^=[2] ^#0 ^→[⌜ℒₒᵣ⌝; 2] ⌜ℒₒᵣ⌝.substs 2 ?[^#1] p ^→[⌜ℒₒᵣ⌝; 2] ⌜ℒₒᵣ⌝.substs 2 ?[^#0] p) else 0 + core := fun p ↦ if ⌜ℒₒᵣ⌝.IsSemiformula 1 p then ^∀ ^∀ (^#1 ^= ^#0 ^→[⌜ℒₒᵣ⌝] ⌜ℒₒᵣ⌝.substs ?[^#1] p ^→[⌜ℒₒᵣ⌝] ⌜ℒₒᵣ⌝.substs ?[^#0] p) else 0 def eqReplaceCDef : p⌜ℒₒᵣ⌝.CraigDef where core := .mkSigma “σ p | ( !p⌜ℒₒᵣ⌝.isSemiformulaDef.pi 1 p → let x0 := qqBvarDef 0; let x1 := qqBvarDef 1; - let eq := qqEQDef 2 x1 x0; + let eq := qqEQDef x1 x0; let v0 := mkVec₁Def x0; let v1 := mkVec₁Def x1; - let p0 := p⌜ℒₒᵣ⌝.substsDef 2 v1 p; - let p1 := p⌜ℒₒᵣ⌝.substsDef 2 v0 p; - let imp0 := p⌜ℒₒᵣ⌝.impDef 2 p0 p1; - let imp1 := p⌜ℒₒᵣ⌝.impDef 2 eq imp0; - let all0 := qqAllDef 1 imp1; - !qqAllDef σ 0all0 ) ∧ + let p0 := p⌜ℒₒᵣ⌝.substsDef v1 p; + let p1 := p⌜ℒₒᵣ⌝.substsDef v0 p; + let imp0 := p⌜ℒₒᵣ⌝.impDef p0 p1; + let imp1 := p⌜ℒₒᵣ⌝.impDef eq imp0; + let all0 := qqAllDef imp1; + !qqAllDef σ all0 ) ∧ ( ¬!p⌜ℒₒᵣ⌝.isSemiformulaDef.sigma 1 p → σ = 0)” (by simp) instance : (eqReplaceC (V := V)).Defined eqReplaceCDef where @@ -214,9 +214,9 @@ instance : (eqReplaceC (V := V)).Defined eqReplaceCDef where intro v simp [eqReplaceC, eqReplaceCDef, HierarchySymbol.Semiformula.val_sigma, - (semiformula_defined (LOR (V := V))).df.iff, (semiformula_defined (LOR (V := V))).proper.iff', - (substs_defined (LOR (V := V))).df.iff, (imp_defined (LOR (V := V))).df.iff] - by_cases h : ⌜ℒₒᵣ⌝.Semiformula 1 (v 1) <;> simp [h] + (Language.isSemiformula_defined (LOR (V := V))).df.iff, (Language.isSemiformula_defined (LOR (V := V))).proper.iff', + (Language.substs_defined (LOR (V := V))).df.iff, (Language.imp_defined (LOR (V := V))).df.iff] + by_cases h : ⌜ℒₒᵣ⌝.IsSemiformula 1 (v 1) <;> simp [h] variable (V) @@ -239,8 +239,6 @@ def TTheory.thEQ.eqRefl : ⌜𝐄𝐐'⌝[V] ⊢ (#'0 =' #'0).all := Language.Th simp [Language.Theory.tmem, TTheory.thEQ, Theory.EQ, FirstOrder.Semiformula.quote_all, FirstOrder.Semiformula.quote_eq, Semiformula.Operator.eq_def, Semiterm.quote_bvar] - - end thEQ /- diff --git a/lake-manifest.json b/lake-manifest.json index 597868a..5089206 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "352b7bd19ddb940b29fb5abb91e94a53317fc5ba", + "rev": "3e8de075c396116e8dc88ae9d919e7d011a11efb", "name": "logic", "manifestFile": "lake-manifest.json", "inputRev": "master",