add R

Arithmetization/ISigmaOne/HFS/Coding.lean

@@ -0,0 +1,45 @@
+import Arithmetization.ISigmaOne.HFS.Vec
+
+/-!
+
+# Vec
+
+-/
+
+noncomputable section
+
+namespace LO.Arith
+
+open FirstOrder FirstOrder.Arith
+
+variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁]
+
+def finsetArithmetizeAux : List V → V
+  | []      => ∅
+  | x :: xs => insert x (finsetArithmetizeAux xs)
+
+@[simp] lemma finsetArithmetizeAux_nil : finsetArithmetizeAux ([] : List V) = ∅ := rfl
+
+@[simp] lemma finsetArithmetizeAux_cons (x : V) (xs) :
+    finsetArithmetizeAux (x :: xs) = insert x (finsetArithmetizeAux xs) := rfl
+
+@[simp] lemma mem_finsetArithmetizeAux_iff {x : V} {s : List V} :
+    x ∈ finsetArithmetizeAux s ↔ x ∈ s := by induction s <;> simp [*]
+
+def _root_.Finset.arithmetize (s : Finset V) : V := finsetArithmetizeAux s.toList
+
+@[simp] lemma mem_finsetArithmetize_iff {x : V} {s : Finset V} :
+    x ∈ s.arithmetize ↔ x ∈ s := by
+  simp [Finset.arithmetize]
+
+@[simp] lemma finset_empty_arithmetize : (∅ : Finset V).arithmetize = ∅ := by
+  simp [Finset.arithmetize]
+
+@[simp] lemma finset_insert_arithmetize (a : V) (s : Finset V) :
+    (insert a s).arithmetize = insert a s.arithmetize := mem_ext <| by
+  intro x; simp
+
+
+end LO.Arith
+
+end

Arithmetization/ISigmaOne/HFS/Vec.lean

@@ -590,6 +590,9 @@ lemma nth_ext {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : ∀ i < len v₁,
     have hv : v₁ = v₂ := ih (by simpa using hl) (by intro i hi; simpa using H (i + 1) (by simpa using hi))
     simp [hx, hv]
 
+lemma nth_ext' (l : V) {v₁ v₂ : V} (hl₁ : len v₁ = l) (hl₂ : len v₂ = l) (H : ∀ i < l, v₁.[i] = v₂.[i]) : v₁ = v₂ := by
+  rcases hl₂; exact nth_ext hl₁ (by simpa [hl₁] using H)
+
 lemma le_of_nth_le_nth {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : ∀ i < len v₁, v₁.[i] ≤ v₂.[i]) : v₁ ≤ v₂ := by
   induction v₁ using cons_induction_pi₁ generalizing v₂
   · definability

Arithmetization/ISigmaOne/Metamath/Coding.lean

@@ -1,4 +1,4 @@
-import Arithmetization.ISigmaOne.Metamath.Formula.Functions
+import Arithmetization.ISigmaOne.Metamath.Proof.Typed
 import Arithmetization.Definability.Absoluteness
 
 noncomputable section
@@ -272,4 +272,17 @@ lemma substs_quote {n m} (w : Fin n → SyntacticSemiterm L m) (p : SyntacticSem
 
 end LO.Arith
 
-end
+namespace LO.FirstOrder.Derivation2
+
+open LO.Arith FirstOrder.Arith
+
+variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁]
+
+variable {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)]
+  [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L]
+
+variable (V)
+
+-- def codeIn : {Γ : Finset (SyntacticFormula L)} → Derivation2 Γ → V
+
+end LO.FirstOrder.Derivation2

Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean

@@ -292,20 +292,6 @@ end shift
 
 section substs
 
-variable (L)
-
-def Language.qVec (k n w : V) : V := ^#0 ∷ L.termBShiftVec k n w
-
-variable {L}
-
-lemma Language.SemitermVec.qVec {k n w : V} (h : L.SemitermVec k n w) : L.SemitermVec (k + 1) (n + 1) (L.qVec k n w) :=
-  ⟨by simp [Language.qVec, ←h.termBShiftVec.lh], by
-      intro i hi
-      rcases zero_or_succ i with (rfl | ⟨i, rfl⟩)
-      · simp [Language.qVec]
-      · simpa [Language.qVec, nth_termBShiftVec h (by simpa using hi)] using
-          h.prop (by simpa using hi) |>.termBShift⟩
-
 section
 
 variable (L)
@@ -520,6 +506,24 @@ lemma semiformula_subst_induction {P : V → V → V → V → V → Prop} (hP :
 lemma substs_not_uformula {m w x} (h : ¬L.UFormula x) :
     L.substs m w x = 0 := (construction L).result_prop_not _ h
 
+lemma substs_neg {p} (hp : L.Semiformula n p) :
+    L.SemitermVec n m w → L.substs m w (L.neg p) = L.neg (L.substs m w p) := by
+  revert m w
+  apply Language.Semiformula.induction_pi₁ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ _ _ hp
+  · definability
+  · intros; simp [*]
+  · intros; simp [*]
+  · intros; simp [*]
+  · intros; simp [*]
+  · intro n p q hp hq ihp ihq m w hw
+    simp [hp, hq, hw, hp.substs, hq.substs, ihp hw, ihq hw]
+  · intro n p q hp hq ihp ihq m w hw
+    simp [hp, hq, hw, hp.substs, hq.substs, ihp hw, ihq hw]
+  · intro n p hp ih m w hw
+    simp [hp, hw, hp.substs hw.qVec, ih hw.qVec]
+  · intro n p hp ih m w hw
+    simp [hp, hw, hp.substs hw.qVec, ih hw.qVec]
+
 end substs
 
 namespace Formalized
@@ -534,12 +538,20 @@ def qqNLT (n x y : V) : V := ^nrel n 2 (ltIndex : V) ?[x, y]
 
 notation:75 x:75 " ^=[" n "] " y:76 => qqEQ n x y
 
+notation:75 x:75 " ^= " y:76 => qqEQ 0 x y
+
 notation:75 x:75 " ^≠[" n "] " y:76 => qqNEQ n x y
 
+notation:75 x:75 " ^≠ " y:76 => qqNEQ 0 x y
+
 notation:78 x:78 " ^<[" n "] " y:79 => qqLT n x y
 
+notation:78 x:78 " ^< " y:79 => qqLT 0 x y
+
 notation:78 x:78 " ^≮[" n "] " y:79 => qqNLT n x y
 
+notation:78 x:78 " ^≮ " y:79 => qqNLT 0 x y
+
 end Formalized
 
 end LO.Arith

Arithmetization/ISigmaOne/Metamath/Formula/Iteration.lean

@@ -139,6 +139,41 @@ lemma qqDisj_semiformula {n ps : V} :
 
 end qqDisj
 
+section qqBvarVec
+
+namespace QQBverVec
+
+def blueprint : PR.Blueprint 0 where
+  zero := .mkSigma “y | y = 0” (by simp)
+  succ := .mkSigma “y ih k | ∃ t, !qqBvarDef t k ∧ !consDef y t ih” (by simp)
+
+def construction : PR.Construction V blueprint where
+  zero _ := 0
+  succ _ k ih := ^#k ∷ ih
+  zero_defined := by intro _; simp [blueprint]
+  succ_defined := by intro _; simp [blueprint]
+
+end QQBverVec
+
+end qqBvarVec
+
+namespace Formalized
+
+section fList
+
+namespace FList
+
+def blueprint : PR.Blueprint 2 where
+  zero := .mkSigma “y n p | y = 0” (by simp)
+  succ := .mkSigma “y ih k n p | ∃ numeral, !numeralDef numeral k ∧ ∃ w, !consDef w numeral 0 ∧
+    ∃ sp, !(Language.lDef ℒₒᵣ).substsDef sp 0 w p ∧ !consDef y p ih” (by simp)
+
+end FList
+
+end fList
+
+end Formalized
+
 end LO.Arith
 
 end

Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean

@@ -109,11 +109,18 @@ def substs (p : L.TSemiformula n) (w : L.TSemitermVec n m) : L.TSemiformula m :=
 @[simp] lemma substs_or (w : L.TSemitermVec n m) (p q : L.TSemiformula n) :
     (p ⋎ q).substs w = p.substs w ⋎ q.substs w := by ext; simp [substs]
 @[simp] lemma substs_all (w : L.TSemitermVec n m) (p : L.TSemiformula (n + 1)) :
-    p.all.substs w = (p.substs (L.bvar (0 : V) (by simp) ∷ᵗ w.bShift)).all := by
-  ext; simp [substs, Language.bvar, Language.qVec, Language.TSemitermVec.bShift]
+    p.all.substs w = (p.substs w.q).all := by
+  ext; simp [substs, Language.bvar, Language.qVec, Language.TSemitermVec.bShift, Language.TSemitermVec.q]
 @[simp] lemma substs_ex (w : L.TSemitermVec n m) (p : L.TSemiformula (n + 1)) :
-    p.ex.substs w = (p.substs (L.bvar (0 : V) (by simp) ∷ᵗ w.bShift)).ex := by
-  ext; simp [substs, Language.bvar, Language.qVec, Language.TSemitermVec.bShift]
+    p.ex.substs w = (p.substs w.q).ex := by
+  ext; simp [substs, Language.bvar, Language.qVec, Language.TSemitermVec.bShift, Language.TSemitermVec.q]
+
+@[simp] lemma substs_neg (w : L.TSemitermVec n m) (p : L.TSemiformula n) : (~p).substs w = ~(p.substs w) := by
+  ext; simp only [substs, val_neg, TSemitermVec.prop, Arith.substs_neg p.prop]
+@[simp] lemma substs_imp (w : L.TSemitermVec n m) (p q : L.TSemiformula n) : (p ⟶ q).substs w = p.substs w ⟶ q.substs w := by
+  simp [imp_def]
+@[simp] lemma substs_imply (w : L.TSemitermVec n m) (p q : L.TSemiformula n) : (p ⟷ q).substs w = p.substs w ⟷ q.substs w := by
+  simp [LogicalConnective.iff]
 
 end Language.TSemiformula
 
@@ -156,9 +163,9 @@ scoped infix:75 " =' " => equals
 
 scoped infix:75 " ≠' " => notEquals
 
-scoped infix:75 " ≺ " => lessThan
+scoped infix:75 " <' " => lessThan
 
-scoped infix:75 " ⊀ " => notLessThan
+scoped infix:75 " ≮' " => notLessThan
 
 variable {n m : V}
 
@@ -171,11 +178,11 @@ variable {n m : V}
   ext; simp [notEquals, Language.TSemiterm.shift, Language.TSemiformula.shift, qqNEQ]
 
 @[simp] lemma shift_lessThan (t₁ t₂ : ⌜ℒₒᵣ⌝.TSemiterm n) :
-    (t₁ ≺ t₂).shift = (t₁.shift ≺ t₂.shift) := by
+    (t₁ <' t₂).shift = (t₁.shift <' t₂.shift) := by
   ext; simp [lessThan, Language.TSemiterm.shift, Language.TSemiformula.shift, qqLT]
 
 @[simp] lemma shift_notLessThan (t₁ t₂ : ⌜ℒₒᵣ⌝.TSemiterm n) :
-    (t₁ ⊀ t₂).shift = (t₁.shift ⊀ t₂.shift) := by
+    (t₁ ≮' t₂).shift = (t₁.shift ≮' t₂.shift) := by
   ext; simp [notLessThan, Language.TSemiterm.shift, Language.TSemiformula.shift, qqNLT]
 
 @[simp] lemma substs_equals (w : ⌜ℒₒᵣ⌝.TSemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.TSemiterm n) :
@@ -187,11 +194,11 @@ variable {n m : V}
   ext; simp [notEquals, Language.TSemiterm.substs, Language.TSemiformula.substs, qqNEQ]
 
 @[simp] lemma substs_lessThan (w : ⌜ℒₒᵣ⌝.TSemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.TSemiterm n) :
-    (t₁ ≺ t₂).substs w = (t₁.substs w ≺ t₂.substs w) := by
+    (t₁ <' t₂).substs w = (t₁.substs w <' t₂.substs w) := by
   ext; simp [lessThan, Language.TSemiterm.substs, Language.TSemiformula.substs, qqLT]
 
 @[simp] lemma substs_notLessThan (w : ⌜ℒₒᵣ⌝.TSemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.TSemiterm n) :
-    (t₁ ⊀ t₂).substs w = (t₁.substs w ⊀ t₂.substs w) := by
+    (t₁ ≮' t₂).substs w = (t₁.substs w ≮' t₂.substs w) := by
   ext; simp [notLessThan, Language.TSemiterm.substs, Language.TSemiformula.substs, qqNLT]
 
 end Formalized

Arithmetization/ISigmaOne/Metamath/Language.lean

@@ -160,6 +160,12 @@ abbrev LOR : Arith.Language V := Language.codeIn ℒₒᵣ V
 
 notation "⌜ℒₒᵣ⌝" => LOR
 
+variable (V)
+
+instance LOR.defined : (⌜ℒₒᵣ⌝ : Arith.Language V).Defined (Language.lDef ℒₒᵣ) := inferInstance
+
+variable {V}
+
 def zeroIndex : ℕ := Encodable.encode (Language.Zero.zero : (ℒₒᵣ : FirstOrder.Language).Func 0)
 
 def oneIndex : ℕ := Encodable.encode (Language.One.one : (ℒₒᵣ : FirstOrder.Language).Func 0)

Arithmetization/ISigmaOne/Metamath/Proof/R.lean

@@ -0,0 +1,93 @@
+import Arithmetization.ISigmaOne.Metamath.Proof.Typed
+
+/-!
+
+# Theory $\mathsf{R}$
+
+-/
+
+noncomputable section
+
+namespace LO.Arith
+
+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 (V)
+
+abbrev LOR.Theory := @Language.Theory V _ _ _ _ _ _ ⌜ℒₒᵣ⌝ (Language.lDef ℒₒᵣ) _
+
+variable {V}
+
+abbrev bv {n : V} (x : V) (h : x < n := by simp) : ⌜ℒₒᵣ⌝.TSemiterm n := ⌜ℒₒᵣ⌝.bvar x h
+
+scoped prefix:max "#'" => bv
+
+/-- TODO: move -/
+@[simp] lemma two_lt_three : (2 : V) < (1 + 1 + 1 : V) := by simp [←one_add_one_eq_two]
+@[simp] lemma two_lt_four : (2 : V) < (1 + 1 + 1 + 1 : V) := by simp [←one_add_one_eq_two]
+@[simp] lemma three_lt_four : (3 : V) < (1 + 1 + 1 + 1 : V) := by simp [←two_add_one_eq_three, ←one_add_one_eq_two]
+@[simp] lemma two_sub_one_eq_one : (2 : V) - 1 = 1 := by simp [←one_add_one_eq_two]
+@[simp] lemma three_sub_one_eq_two : (3 : V) - 1 = 2 := by simp [←two_add_one_eq_three]
+
+class EQTheory (T : LOR.Theory V) where
+  refl : (#'0 =' #'0).all ∈' T
+  symm : (#'1 =' #'0 ⟶ #'0 =' #'1).all.all ∈' T
+  trans : (#'2 =' #'1 ⟶ #'1 =' #'0 ⟶ #'2 =' #'0).all.all.all ∈' T
+  addExt : (#'3 =' #'2 ⟶ #'1 =' #'0 ⟶ (#'3 + #'1) =' (#'2 + #'0)).all.all.all.all ∈' T
+  mulExt : (#'3 =' #'2 ⟶ #'1 =' #'0 ⟶ (#'3 * #'1) =' (#'2 * #'0)).all.all.all.all ∈' T
+
+class R'Theory (T : LOR.Theory V) where
+  add (n m : V) : (↑n + ↑m) =' ↑(n + m) ∈' T
+  mul (n m : V) : (↑n * ↑m) =' ↑(n * m) ∈' T
+  ne {n m : V} : n ≠ m → ↑n ≠' ↑m ∈' T
+  lt {n m : V} : n < m → ↑n <' ↑m ∈' T
+  nlt {n m : V} : ¬n < m → ↑n ≮' ↑m ∈' T
+  bound (n : V) : (#'0 <' ↑n ⟷ #'0 <' ↑n).all ∈' T
+
+
+/--/
+variable {T : LOR.Theory V} [EQTheory T]
+
+open Language.Theory.TProof
+
+def eqRefl (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t =' t := by
+  have : T ⊢ (#'0 =' #'0).all := byAxm EQTheory.refl
+  simpa [Language.TSemiformula.substs₁] using specialize this t
+
+def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₁ := by
+  have : T ⊢ (#'1 =' #'0 ⟶ #'0 =' #'1).all.all := byAxm EQTheory.symm
+  have := by simpa using specialize this t₁
+  simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t₂
+
+def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := by
+  have : T ⊢ (#'2 =' #'1 ⟶ #'1 =' #'0 ⟶ #'2 =' #'0).all.all.all := byAxm EQTheory.trans
+  have := by simpa using specialize this t₁
+  have := by simpa using specialize this t₂
+  simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t₃
+
+def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := by
+  have : T ⊢ (#'3 =' #'2 ⟶ #'1 =' #'0 ⟶ (#'3 + #'1) =' (#'2 + #'0)).all.all.all.all := byAxm EQTheory.addExt
+  have := by simpa using specialize this t₁
+  have := by simpa using specialize this t₂
+  have := by simpa using specialize this u₁
+  simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this u₂
+
+def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := by
+  have : T ⊢ (#'3 =' #'2 ⟶ #'1 =' #'0 ⟶ (#'3 * #'1) =' (#'2 * #'0)).all.all.all.all := byAxm EQTheory.mulExt
+  have := by simpa using specialize this t₁
+  have := by simpa using specialize this t₂
+  have := by simpa using specialize this u₁
+  simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this u₂
+
+end Formalized
+
+end LO.Arith
+
+end