Removed older proofs in order to avoid having to rewrite them every time

PropositionalKripke.agda

@@ -67,107 +67,3 @@ module PropositionalKripke (PV : Set) where
     ⟦ andi p₁ p₂ ⟧ wΓ = ⟨ (⟦ p₁ ⟧ wΓ) , (⟦ p₂ ⟧ wΓ) ⟩
     ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ
     ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ
-
-
-
-  
-
-  module CompletenessProof where
-  
-    -- First, we define the Universal Kripke Model with (⊢⁺)⁻¹ as world order
-    UK : Kripke
-    UK = record {
-      Worlds = Con;
-      _≤_ = λ x y → y ⊢⁺ x;
-      refl≤ = refl⊢⁺;
-      tran≤ = λ ΓΓ' Γ'Γ'' → tran⊢⁺ Γ'Γ'' ΓΓ';
-      _⊩_ = λ Γ x → Γ ⊢ Var x;
-      mon⊩ = λ ba bx → halftran⊢⁺ ba bx
-      }
-    open Kripke UK
-  
-    -- Now we can prove that ⊩ᶠ and ⊢ act in the same way
-    ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢ F
-    ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F
-    ⊢→⊩ᶠ {Var x} h = h
-    ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF))
-    ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩
-    ⊩ᶠ→⊢ {Var x} h = h
-    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
-    ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG)
-
-    -- Finally, we can deduce completeness of the Kripke model
-    completeness : {F : Form} → [] ⊫ F → [] ⊢ F
-    completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt)
-
-  module NormalizationProof where
-    
-    -- First we define the Universal model with (⊢⁰⁺)⁻¹ as world order
-    -- It is slightly different from the last Model, but proofs are the same
-    UK⁰ : Kripke
-    UK⁰ = record {
-      Worlds = Con;
-      _≤_ = λ x y → y ⊢⁰⁺ x;
-      refl≤ = refl⊢⁰⁺;
-      tran≤ = λ ΓΓ' Γ'Γ'' → tran⊢⁰⁺ Γ'Γ'' ΓΓ';
-      _⊩_ = λ Γ x → Γ ⊢⁰ Var x;
-      mon⊩ = λ ba bx → halftran⊢⁰⁺⁰ ba bx
-      }
-    open Kripke UK⁰
-
-    -- We can now prove the normalization, i.e. the quote and function exists
-    -- The mutual proofs are exactly the same as the ones used in completeness
-    -- quote
-    ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F
-    -- unquote
-    ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F
-  
-    ⊢→⊩ᶠ {Var x} h = h
-    ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF))
-    ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩
-    ⊩ᶠ→⊢ {Var x} h = neu⁰ h
-    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
-    ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ =  andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG)
-
-  module OtherProofs where
-
-    -- We will try to define the Kripke models using the following embeddings
-
-    -- Strongest is using the ⊢⁺ relation directly
-
-    -- -> See module CompletenessProof
-
-    -- We can also use the relation ⊢⁰⁺, which is compatible with ⊢⁰ and ⊢*
-
-    -- -> See module NormalizationProof
-  
-    
-  
-    {- Renamings : ∈* -}
-    UK∈* : Kripke
-    UK∈* = record {
-      Worlds = Con;
-      _≤_ = _∈*_;
-      refl≤ = refl∈*;
-      tran≤ = tran∈*;
-      _⊩_ = λ Γ x → Γ ⊢ Var x;
-      mon⊩ = λ x x₁ → addhyp⊢ x x₁
-      }
-    {-
-    {- Weakening anywhere, order preserving, duplication authorized : ⊂⁺ -}
-    UK⊂⁺ : Kripke
-    UK⊂⁺ = record {
-      Worlds = Con;
-      _≤_ = _⊂⁺_;
-      refl≤ = refl⊂⁺;
-      tran≤ = tran⊂⁺;
-      _⊩_ = λ Γ x → Γ ⊢ Var x;
-      mon⊩ = λ x x₁ → addhyp⊢ x x₁
-      }
-    -}
-    {- Weakening anywhere, no duplication, order preserving : ⊂ -}
-    
-
-    {- Weakening at the end : ⊆-}
-
-    -- This is exactly our relation ⊆ 

Readme.agda

@@ -116,23 +116,19 @@ module PierceDisproof where
   
   
 module CompletenessAndNormalization where
+
   -- With Kripke models, we can even prove completeness
   -- Using the Universal Kripke Model
-
+  
-  completenessQuote = CompletenessProof.⊩ᶠ→⊢
-  completenessUnquote = CompletenessProof.⊢→⊩ᶠ
-
   -- With a slightly different universal model (using normal and neutral forms),
   -- we can make a normalization proof
-  normalizationQuote = NormalizationProof.⊩ᶠ→⊢
+  
-  normalizationUnquote = NormalizationProof.⊢→⊩ᶠ
+  -- This normalization proof has first been made in the biggest Kripke model possible
-
-  -- This normalization proof has been made in the biggest Kripke model possible
   -- that is, the one using the relation ⊢⁰⁺
   -- But we can also prove it with tighter relations: ∈*, ⊂⁺, ⊂, ⊆
 
   -- As all those proofs are really similar, we created a NormalizationFrame structure
-  -- that computes most of the proof with only a few lemmas
+  -- that computes most of the proofs with only a few lemmas
   open import PropositionalKripkeGeneral String
 
   -- We now have access to quote and unquote functions with this