D3

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

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

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

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}
 

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,35 +63,35 @@ 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)⟩
 
 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
 
 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₁