From cdf8983eabacb3f2e9fadf174522c064ac2eff4b Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Thu, 25 Jul 2024 13:25:21 +0900
Subject: [PATCH] D1

---
 .../ISigmaOne/Metamath/Coding.lean            | 37 +++++++++++++------
 .../ISigmaOne/Metamath/Proof/Typed.lean       | 10 ++++-
 lake-manifest.json                            |  2 +-
 3 files changed, 36 insertions(+), 13 deletions(-)

diff --git a/Arithmetization/ISigmaOne/Metamath/Coding.lean b/Arithmetization/ISigmaOne/Metamath/Coding.lean
index 7464e13..cd48c69 100644
--- a/Arithmetization/ISigmaOne/Metamath/Coding.lean
+++ b/Arithmetization/ISigmaOne/Metamath/Coding.lean
@@ -503,6 +503,12 @@ open LO.Arith Formalized
   ext; simp [LogicalConnective.bex, imp_eq, Language.TSemiformula.cast,
     Language.TSemiformula.ball, Semiformula.Operator.lt_eq, termBShift_quote]
 
+instance : GoedelQuote (Sentence L) ((L.codeIn V).TFormula) := ⟨fun σ ↦ (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).TSemiformula (0 : ℕ))⟩
+
+lemma quote_semisentence_def' (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).TFormula) = (⌜Rew.embs.hom σ⌝ : (Language.codeIn L V).TSemiformula (0 : ℕ)) := rfl
+
+@[simp] lemma quote_semisentence_val (σ : Sentence L) : (⌜σ⌝ : (L.codeIn V).TFormula).val = ⌜σ⌝ := rfl
+
 end Semiformula
 
 namespace Derivation2
@@ -638,6 +644,9 @@ lemma quote_image_shift (Γ : Finset (SyntacticFormula L)) : (L.codeIn V).setShi
 @[simp] lemma derivationOf_quote {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : (L.codeIn V).DerivationOf ⌜d⌝ ⌜Γ⌝ :=
   ⟨by simp, by simp⟩
 
+lemma derivable_of_quote {Γ : Finset (SyntacticFormula L)} (d : ⊢¹ᶠ Γ) : (L.codeIn V).Derivable ⌜Γ⌝ :=
+  ⟨⌜d⌝, by simp⟩
+
 section
 
 class DefinableSigma₁Theory (T : Theory L) extends LDef.TDef L.lDef where
@@ -670,18 +679,24 @@ lemma mem_coded_theory {σ} (h : σ ∈ T) : ⌜σ⌝ ∈ T.codeIn V := Language
 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 ℒₒᵣ)
-
+/-- D1 -/
+theorem provable_of_provable : T ⊢! σ → (T.codeIn V).Provable ⌜σ⌝ := by
+  intro h
+  rcases provable_iff_derivation2.mp h with ⟨Γ, h, ⟨d⟩⟩
+  refine ⟨⌜Γ⌝, ?_, ?_⟩
+  · intro x hx
+    rcases Sequent.mem_codeIn hx with ⟨p, hp, rfl⟩
+    rcases h p hp with ⟨π, hπ, hπp⟩
+    have : p = ~Rew.embs.hom π := by simp [hπp]
+    rcases this with rfl
+    simp [neg_quote, ←quote_semisentence_def]; exact mem_coded_theory hπ
+  · have : (⌜Γ⌝ : V) ∪ {⌜σ⌝} = insert ⌜σ⌝ ⌜Γ⌝ := mem_ext fun x ↦ by simp; tauto
+    rw [this]
+    simpa [quote_semisentence_def] using derivable_of_quote (V := V) d
 
+theorem tprovable_of_provable : T ⊢! σ → T.codeIn V ⊢! ⌜σ⌝ := fun h ↦ by
+  simpa [Language.Theory.TProvable.iff_provable] using provable_of_provable (V := V) h
 
-end Formalized
+end
 
 end LO.Arith
diff --git a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean
index 723ca26..103949e 100644
--- a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean
+++ b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean
@@ -136,9 +136,17 @@ def Language.Theory.Derivable.toTDerivation {T : L.Theory} (Γ : L.Sequent) (h :
   choose a ha using h; choose d hd using ha.2
   exact ⟨a, ha.1, d, hd⟩
 
-def Language.Theory.TDerivation.toDerivable {T : L.Theory} {Γ : L.Sequent} (d : T ⊢¹ Γ) : T.Derivable Γ.val :=
+lemma Language.Theory.TDerivation.toDerivable {T : L.Theory} {Γ : L.Sequent} (d : T ⊢¹ Γ) : T.Derivable Γ.val :=
   ⟨d.antecedents, d.antecedents_fvFree, d.derivation, d.derivationOf⟩
 
+lemma Language.Theory.TProvable.iff_provable {T : L.Theory} {σ : L.TFormula} :
+    T ⊢! σ ↔ T.Provable σ.val := by
+  constructor
+  · intro b
+    simpa [←singleton_eq_insert] using Language.Theory.TDerivation.toDerivable b.get
+  · intro h
+    exact ⟨Language.Theory.Derivable.toTDerivation _ <| by simpa [←singleton_eq_insert] using h⟩
+
 def Language.Theory.TDerivation.toTProof {T : L.Theory} {p} (d : T ⊢¹ insert p ∅) : T ⊢ p := d
 
 def Language.Theory.TProof.toTDerivation {T : L.Theory} {p} (d : T ⊢ p) : T ⊢¹ insert p ∅ := d
diff --git a/lake-manifest.json b/lake-manifest.json
index dffb586..d6d53b1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4d5b06b24da1c43bb2aa9ec49c594f809786e035",
+   "rev": "c1eb51d2ab8beb826a9f01fc02522b835d4ad9fd",
    "name": "logic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",