Tidied files up, changed messy prop.agda into a beautiful Readme.agda

ListUtil.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --prop #-}
+
+module ListUtil where
+
+  open import Data.List using (List; _∷_; []) public
+
+  private
+    variable
+      T : Set₀
+      L : List T
+      L' : List T
+      A : T
+      B : T
+
+
+  -- Definition of sublists
+  -- Similar definition : {L L' : List T} → L ⊆ L' ++ L
+  data _⊆_ : List T → List T → Prop where
+    zero⊆ : L ⊆ L
+    next⊆ : L ⊆ L' → L ⊆ (A ∷ L')
+
+  -- One useful lemma
+  retro⊆ : {L L' : List T} → {A : T} → (A ∷ L) ⊆ L' → L ⊆ L'
+  retro⊆ {L' = []} () -- Impossible to have «A∷L ⊆ []»
+  retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆
+  retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h)
+

Normalization.agda

@@ -1,135 +0,0 @@
-{-# OPTIONS --prop #-}
-
-module Normalization (PV : Set) where
-
-  open import PropUtil
-  open import PropositionalLogic PV
-  open import PropositionalKripke PV
-
-  private
-    variable
-      A  : Form
-      B  : Form
-      F  : Form
-      G  : Form
-      Γ  : Con
-      Γ' : Con
-      x  : PV
-
-  -- ⊢⁰ are neutral forms
-  -- ⊢* are normal forms
-  mutual
-    data _⊢⁰_ : Con → Form → Prop where
-      zero : (A ∷ Γ) ⊢⁰ A
-      next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A
-      app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
-    data _⊢*_ : Con → Form → Prop where
-      neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x
-      lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B)
-
-  ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F
-  ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F
-  ⊢⁰→⊢ zero = zero
-  ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h)
-  ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x)
-  ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x
-  ⊢*→⊢ (lam h) = lam (⊢*→⊢ h)
-
-  private
-    data _⊆_ : Con → Con → Prop where
-       zero⊆ : Γ ⊆ Γ
-       next⊆ : Γ ⊆ Γ' → Γ ⊆ (A ∷ Γ')
-    retro⊆ : {Γ Γ' : Con} → {A : Form} → (A ∷ Γ) ⊆ Γ' → Γ ⊆ Γ'
-    retro⊆ {Γ' = []} () -- Impossible to have «A∷Γ ⊆ []»
-    retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆
-    retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h)
-
-
-  -- Extension of ⊢⁰ to contexts
-  _⊢⁺⁰_ : Con → Con → Prop
-  Γ ⊢⁺⁰ [] = ⊤
-  Γ ⊢⁺⁰ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁺⁰ Γ')
-  infix 5 _⊢⁺⁰_
-  
-  -- This relation is reflexive
-  private -- Lemma showing that the relation respects ⊆
-    mon⊆≤⁰ : Γ' ⊆ Γ → Γ ⊢⁺⁰ Γ'
-    mon⊆≤⁰ {[]} sub = tt
-    mon⊆≤⁰ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩
-    mon⊆≤⁰ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆≤⁰ sub)) ) , mon⊆≤⁰ (next⊆ (retro⊆ sub)) ⟩
-
-  refl⊢⁺⁰ : Γ ⊢⁺⁰ Γ
-  refl⊢⁺⁰ {[]} = tt
-  refl⊢⁺⁰ {x ∷ Γ} = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩
-
-  -- A useful lemma, that we can add hypotheses 
-  addhyp⊢⁺⁰ : Γ ⊢⁺⁰ Γ' → (A ∷ Γ) ⊢⁺⁰ Γ'
-  addhyp⊢⁺⁰ {Γ' = []} h = tt
-  addhyp⊢⁺⁰ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺⁰ (proj₂ h) ⟩
-
-
-  {- We use a slightly different Universal Kripke Model -}
-  module UniversalKripke⁰ where
-    Worlds = Con
-    _≤_ : Con → Con → Prop
-    Γ ≤ Η = Η ⊢⁺⁰ Γ
-    _⊩_ : Con → PV → Prop
-    Γ ⊩ x = Γ ⊢⁰ Var x
-
-    refl≤ = refl⊢⁺⁰
-
-    -- Proving transitivity
-    halftran≤* : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢* F → Γ ⊢* F
-    halftran≤⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F
-    halftran≤* h⁺ (neu⁰ x) = neu⁰ (halftran≤⁰ h⁺ x)
-    halftran≤* h⁺ (lam h) = lam (halftran≤* ⟨ zero , addhyp⊢⁺⁰ h⁺ ⟩ h)
-    halftran≤⁰ h⁺ zero = proj₁ h⁺
-    halftran≤⁰ h⁺ (next h) = halftran≤⁰ (proj₂ h⁺) h
-    halftran≤⁰ h⁺ (app h h') = app (halftran≤⁰ h⁺ h) (halftran≤* h⁺ h')
-    tran≤ : {Γ Γ' Γ'' : Con} → Γ ≤ Γ' → Γ' ≤ Γ'' → Γ ≤ Γ''
-    tran≤ {[]} h h' = tt
-    tran≤ {x ∷ Γ} h h' = ⟨ halftran≤⁰ h' (proj₁ h) , tran≤ (proj₂ h) h' ⟩
-
-    mon⊩ : {w w' : Con} → w ≤ w' → {x : PV} → w ⊩ x → w' ⊩ x
-    mon⊩ h h' = halftran≤⁰ h h'
-
-  
-  ⊢*Var : Γ ⊢* Var x → Γ ⊢⁰ Var x
-  ⊢*Var (neu⁰ x) = x
-
-  UK⁰ : Kripke
-  UK⁰ = record {UniversalKripke⁰}
-  open Kripke UK⁰
-  open UniversalKripke⁰ using (halftran≤⁰)
-
-  -- 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))
-  ⊩ᶠ→⊢ {Var x} h = neu⁰ h
-  ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺⁰ refl⊢⁺⁰) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
-
-  
---⊩ᶠ→⊢ {F ⇒ G} {Γ} h =  lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
-  
-  {-
-  ⊩ᶠ→⊢ {F} zero = neu⁰ zero
-  ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next {!!})
-  ⊩ᶠ→⊢ {F ⇒ G} (next h) = neu⁰ (next {!!})
-  ⊩ᶠ→⊢ {F ⇒ G} (lam h) = lam (⊩ᶠ→⊢ h)
-  ⊩ᶠ→⊢ {Var x} (app h h₁) = neu⁰ (app {!⊩ᶠ→⊢ h!} (⊩ᶠ→⊢ h₁))
-  ⊩ᶠ→⊢ {F ⇒ G} (app h h₁) = neu⁰ (app {!!} (⊩ᶠ→⊢ h₁))
-  -}
-
-  {-
-  ⊩ᶠ→⊢ {Var x} zero = neu⁰ zero
-  ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next (⊢*Var (⊩ᶠ→⊢ {Var x} h)))
-  ⊩ᶠ→⊢ {Var x} (app {A = A} h h₁) = {!!}
-  -- neu⁰ (app {A = A} {!!} (⊩ᶠ→⊢ (CompletenessProof.⊢→⊩ᶠ h₁)))
-  ⊩ᶠ→⊢ {F ⇒ G} {Γ} h = lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
-  -}
-
-

PropositionalKripke.agda

@@ -2,6 +2,7 @@
 
 module PropositionalKripke (PV : Set) where
 
+  open import ListUtil
   open import PropUtil
   open import PropositionalLogic PV
 
@@ -37,7 +38,7 @@ module PropositionalKripke (PV : Set) where
     _⊩ᶠ_ : Worlds → Form → Prop
     w ⊩ᶠ Var x = w ⊩ x
     w ⊩ᶠ (fp ⇒ fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq
-
+    
     _⊩ᶜ_ : Worlds → Con → Prop
     w ⊩ᶜ [] = ⊤
     w ⊩ᶜ (p ∷ c) = (w ⊩ᶠ p) ∧ (w ⊩ᶜ c)
@@ -66,43 +67,56 @@ module PropositionalKripke (PV : Set) where
 
 
   
-  {- Universal Kripke -}
-
-  module UniversalKripke where
-    Worlds = Con
-    _≤_ : Con → Con → Prop
-    Γ ≤ Η = Η ⊢⁺ Γ
-    _⊩_ : Con → PV → Prop
-    Γ ⊩ x = Γ ⊢ Var x
-
-    refl≤ = refl⊢⁺
-
-    -- Proving transitivity
-    halftran≤ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F
-    halftran≤ h⁺ zero = proj₁ h⁺
-    halftran≤ h⁺ (next h) = halftran≤ (proj₂ h⁺) h
-    halftran≤ h⁺ (lam h) = lam (halftran≤ ⟨ zero , addhyp⊢⁺ h⁺ ⟩ h)
-    halftran≤ h⁺ (app h h') = app (halftran≤ h⁺ h) (halftran≤ h⁺ h')
-    tran≤ : {Γ Γ' Γ'' : Con} → Γ ≤ Γ' → Γ' ≤ Γ'' → Γ ≤ Γ''
-    tran≤ {[]} h h' = tt
-    tran≤ {x ∷ Γ} h h' = ⟨ halftran≤ h' (proj₁ h) , tran≤ (proj₂ h) h' ⟩
-
-    mon⊩ : {w w' : Con} → w ≤ w' → {x : PV} → w ⊩ x → w' ⊩ x
-    mon⊩ h h' = halftran≤ h h' 
-
-  UK : Kripke
-  UK = record {UniversalKripke}
 
   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
-    open UniversalKripke using (halftran≤)
 
+    -- 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⊢⁺ iq) h) zero)) (⊩ᶠ→⊢ hF))
+    ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ iq) h) zero)) (⊩ᶠ→⊢ hF))
     ⊩ᶠ→⊢ {Var x} h = h
     ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
 
+    -- 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))
+    ⊩ᶠ→⊢ {Var x} h = neu⁰ h
+    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))

PropositionalLogic.agda

@@ -3,17 +3,14 @@
 module PropositionalLogic (PV : Set) where
 
   open import PropUtil
-  open import Data.List using (List; _∷_; []) public
+  open import ListUtil
-
+  
   data Form : Set where
     Var : PV → Form
     _⇒_ : Form → Form → Form
   
   infixr 8 _⇒_
 
-  data _≡_ : {A : Set} → A → A → Prop where
-    refl : {A : Set} → {x : A} → x ≡ x
-
   {- Contexts -}
   Con = List Form
 
@@ -24,20 +21,15 @@ module PropositionalLogic (PV : Set) where
       B   : Form
       B'  : Form
       C   : Form
+      F   : Form
+      G   : Form
       Γ   : Con
       Γ'  : Con
+      x   : PV
 
-  -- Definition of subcontexts (directly included)
-  -- Similar definition : {Γ' : Con} → Γ ⊆ Γ' ++ Γ
-  private
-    data _⊆_ : Con → Con → Prop where
-       zero⊆ : Γ ⊆ Γ
-       next⊆ : Γ ⊆ Γ' → Γ ⊆ (A ∷ Γ')
-    retro⊆ : {Γ Γ' : Con} → {A : Form} → (A ∷ Γ) ⊆ Γ' → Γ ⊆ Γ'
-    retro⊆ {Γ' = []} () -- Impossible to have «A∷Γ ⊆ []»
-    retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆
-    retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h)
 
+
+  {--- DEFINITION OF ⊢ ---}
   
   data _⊢_ : Con → Form → Prop where
     zero : (A ∷ Γ) ⊢ A
@@ -52,23 +44,101 @@ module PropositionalLogic (PV : Set) where
   Γ ⊢⁺ [] = ⊤
   Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ')
   infix 5 _⊢⁺_
-  
-  -- This relation is reflexive
-  private -- Lemma showing that the relation respects ⊆
-    mon⊆≤ : Γ' ⊆ Γ → Γ ⊢⁺ Γ'
-    mon⊆≤ {[]} sub = tt
-    mon⊆≤ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩
-    mon⊆≤ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆≤ sub)) ) , mon⊆≤ (next⊆ (retro⊆ sub)) ⟩
 
+  -- The relation respects ⊆
+  mon⊆⊢⁺ : Γ' ⊆ Γ → Γ ⊢⁺ Γ'
+  mon⊆⊢⁺ {[]} sub = tt
+  mon⊆⊢⁺ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆⊢⁺ (next⊆ zero⊆) ⟩
+  mon⊆⊢⁺ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆⊢⁺ sub)) ) , mon⊆⊢⁺ (next⊆ (retro⊆ sub)) ⟩
+
+  -- The relation is reflexive
   refl⊢⁺ : Γ ⊢⁺ Γ
   refl⊢⁺ {[]} = tt
-  refl⊢⁺ {x ∷ Γ} = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩
+  refl⊢⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁺ (next⊆ zero⊆) ⟩
 
-  -- A useful lemma, that we can add hypotheses 
+  -- We can add hypotheses to the left 
   addhyp⊢⁺ : Γ ⊢⁺ Γ' → (A ∷ Γ) ⊢⁺ Γ'
   addhyp⊢⁺ {Γ' = []} h = tt
   addhyp⊢⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺ (proj₂ h) ⟩
-    
+
+  -- The relation respects ⊢
+  halftran⊢⁺ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F
+  halftran⊢⁺ h⁺ zero = proj₁ h⁺
+  halftran⊢⁺ h⁺ (next h) = halftran⊢⁺ (proj₂ h⁺) h
+  halftran⊢⁺ h⁺ (lam h) = lam (halftran⊢⁺ ⟨ zero , addhyp⊢⁺ h⁺ ⟩ h)
+  halftran⊢⁺ h⁺ (app h h') = app (halftran⊢⁺ h⁺ h) (halftran⊢⁺ h⁺ h')
+
+  -- The relation is transitive
+  tran⊢⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁺ Γ' → Γ' ⊢⁺ Γ'' → Γ ⊢⁺ Γ''
+  tran⊢⁺ {Γ'' = []} h h' = tt
+  tran⊢⁺ {Γ'' = x ∷ Γ*} h h' = ⟨ halftran⊢⁺ h (proj₁ h') , tran⊢⁺ h (proj₂ h') ⟩
+
+  
+
+  {--- DEFINITIONS OF ⊢⁰ and ⊢* ---}
+
+  -- ⊢⁰ are neutral forms
+  -- ⊢* are normal forms
+  mutual
+    data _⊢⁰_ : Con → Form → Prop where
+      zero : (A ∷ Γ) ⊢⁰ A
+      next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A
+      app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
+    data _⊢*_ : Con → Form → Prop where
+      neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x
+      lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B)
+  infix 5 _⊢⁰_
+  infix 5 _⊢*_
+
+  -- Both are tighter than ⊢
+  ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F
+  ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F
+  ⊢⁰→⊢ zero = zero
+  ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h)
+  ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x)
+  ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x
+  ⊢*→⊢ (lam h) = lam (⊢*→⊢ h)
+
+  -- Extension of ⊢⁰ to contexts
+  -- i.e. there is a neutral proof for any element
+  _⊢⁰⁺_ : Con → Con → Prop
+  Γ ⊢⁰⁺ [] = ⊤
+  Γ ⊢⁰⁺ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁰⁺ Γ')
+  infix 5 _⊢⁰⁺_
+  
+  -- The relation respects ⊆
+  mon⊆⊢⁰⁺ : Γ' ⊆ Γ → Γ ⊢⁰⁺ Γ'
+  mon⊆⊢⁰⁺ {[]} sub = tt
+  mon⊆⊢⁰⁺ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩
+  mon⊆⊢⁰⁺ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆⊢⁰⁺ sub)) ) , mon⊆⊢⁰⁺ (next⊆ (retro⊆ sub)) ⟩
+
+  -- This relation is reflexive
+  refl⊢⁰⁺ : Γ ⊢⁰⁺ Γ
+  refl⊢⁰⁺ {[]} = tt
+  refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩
+
+  -- A useful lemma, that we can add hypotheses 
+  addhyp⊢⁰⁺ : Γ ⊢⁰⁺ Γ' → (A ∷ Γ) ⊢⁰⁺ Γ'
+  addhyp⊢⁰⁺ {Γ' = []} h = tt
+  addhyp⊢⁰⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁰⁺ (proj₂ h) ⟩
+
+  -- The relation preserves ⊢⁰ and ⊢*
+  halftran⊢⁰⁺* : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢* F → Γ ⊢* F
+  halftran⊢⁰⁺⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F
+  halftran⊢⁰⁺* h⁺ (neu⁰ x) = neu⁰ (halftran⊢⁰⁺⁰ h⁺ x)
+  halftran⊢⁰⁺* h⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero , addhyp⊢⁰⁺ h⁺ ⟩ h)
+  halftran⊢⁰⁺⁰ h⁺ zero = proj₁ h⁺
+  halftran⊢⁰⁺⁰ h⁺ (next h) = halftran⊢⁰⁺⁰ (proj₂ h⁺) h
+  halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h')
+
+  -- The relation is transitive
+  tran⊢⁰⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰⁺ Γ'' → Γ ⊢⁰⁺ Γ''
+  tran⊢⁰⁺ {Γ'' = []} h h' = tt
+  tran⊢⁰⁺ {Γ'' = x ∷ Γ} h h' = ⟨ halftran⊢⁰⁺⁰ h (proj₁ h') , tran⊢⁰⁺ h (proj₂ h') ⟩
+
+
+
+
   {--- Simple translation with in an Environment ---}
 
   Env = PV → Prop
@@ -88,6 +158,9 @@ module PropositionalLogic (PV : Set) where
   ⟦ app th₁ th₂ ⟧ᵈ = λ p → ⟦ th₁ ⟧ᵈ p (⟦ th₂ ⟧ᵈ p)
 
 
+
+
+
   {--- Combinatory Logic ---}
 
   data ⊢sk : Form → Prop where

Readme.agda

@@ -0,0 +1,129 @@
+{-# OPTIONS --prop #-}
+module Readme where
+
+-- We will use String as propositional variables
+open import Agda.Builtin.String using (String)
+open import ListUtil
+open import PropUtil
+
+-- We can use the basic propositional logic
+open import PropositionalLogic String
+
+-- Here is an example of a propositional formula and its proof
+-- The formula is (Q → R) → (P → Q) → P → R
+d-C : [] ⊢ ((Var "Q") ⇒ (Var "R")) ⇒ ((Var "P") ⇒ (Var "Q")) ⇒ (Var "P") ⇒ (Var "R")
+d-C = lam (lam (lam (app (next (next zero)) (app (next zero) zero))))
+
+-- We can with the basic interpretation ⟦_⟧ prove that some formulæ are not provable
+-- For example, we can disprove (P → Q) → P 's provability as we can construct an
+-- environnement where the statement doesn't hold
+
+ρ₀ : Env
+ρ₀ "P" = ⊥
+ρ₀ "Q" = ⊤
+ρ₀ _ = ⊥
+
+cex-d : ([] ⊢ (((Var "P") ⇒ (Var "Q")) ⇒ (Var "P"))) → ⊥
+cex-d h = ⟦ h ⟧ᵈ {ρ₀} tt λ x → tt
+
+-- But this is not enough to show the non-provability of every non-provable statement.
+-- Let's take as an example Pierce formula : ((P → Q) → P) → P
+-- This statement is equivalent to the law of excluded middle (Tertium Non Datur)
+-- We show that fact in Agda's proposition system
+
+Pierce = {P Q : Prop} → ((P → Q) → P) → P
+TND : Prop → Prop
+TND P = P ∨ (¬ P)
+
+-- Lemma: The double negation of the TND is always true
+-- (You cannot show that having neither a proposition nor its negation is impossible
+nnTND : {P : Prop} → ¬ (¬ (P ∨ ¬ P))
+nnTND ntnd = ntnd (inj₂ λ p → ntnd (inj₁ p))
+P→TND : Pierce → {P : Prop} → TND P
+P→TND pierce {P} = pierce {TND P} {⊥} (λ p → case⊥ (nnTND p))
+TND→P : ({P : Prop} → TND P) → Pierce
+TND→P tnd {P} {Q} pqp = dis (tnd {P}) (λ p → p) (λ np → pqp (λ p → case⊥ (np p)))
+
+
+-- So we have to use a model that is more powerful : Kripke models
+-- With those models, one can describe a frame in which the pierce formula doesn't hold
+-- As we have that any proven formula is *true* in a kripke model, this shows
+-- that the Pierce formula cannot be proven
+
+-- We import the general definition of Kripke models
+open import PropositionalKripke String
+
+-- We will now create a specific Kripke model in which Pierce formula doesn't hold
+
+module PierceDisproof where
+  
+  module PierceWorld where
+    data Worlds : Set where
+      w₁ w₂ : Worlds
+    data _≤_ : Worlds → Worlds → Prop where
+      w₁₁ : w₁ ≤ w₁
+      w₁₂ : w₁ ≤ w₂
+      w₂₂ : w₂ ≤ w₂
+    data _⊩_ : Worlds → String → Prop where
+      w₂A : w₂ ⊩ "A"
+  
+    refl≤ : {w : Worlds} → w ≤ w
+    refl≤ {w₁} = w₁₁
+    refl≤ {w₂} = w₂₂
+    tran≤ : {w w' w'' : Worlds} → w ≤ w' → w' ≤ w'' → w ≤ w''
+    tran≤ w₁₁ z = z
+    tran≤ w₁₂ w₂₂ = w₁₂
+    tran≤ w₂₂ w₂₂ = w₂₂
+    mon⊩ : {a b : Worlds} → a ≤ b → {p : String} → a ⊩ p → b ⊩ p
+    mon⊩ w₂₂ w₂A = w₂A
+    
+  PierceW : Kripke
+  PierceW = record {PierceWorld}
+  open Kripke PierceW
+  open PierceWorld using (w₁ ; w₂ ; w₁₁ ; w₁₂ ; w₂₂ ; w₂A)
+  
+  -- Now we can write the «instance» of the Pierce formula which doesn't hold in our world
+  PierceF : Form 
+  PierceF = (((Var "A" ⇒ Var "B") ⇒ Var "A") ⇒ Var "A")
+  
+  -- Now we show that it does not hold in w₁ but holds in w₂
+  Pierce⊥w₁ : ¬(w₁ ⊩ᶠ PierceF)
+  Pierce⊤w₂ : w₂ ⊩ᶠ PierceF
+  
+  -- A does not hold in w₁
+  NotAw₁ : ¬(w₁ ⊩ᶠ (Var "A"))
+  NotAw₁ ()
+  -- B does not hold in w₂ while A holds
+  NotBw₂ : ¬(w₂ ⊩ᶠ (Var "B"))
+  NotBw₂ ()
+  -- Therefore, (A → B) does not hold in w₁
+  NotABw₁ : ¬(w₁ ⊩ᶠ (Var "A" ⇒ Var "B"))
+  NotABw₁ h = NotBw₂ (h w₁₂ w₂A)
+  -- So the hypothesis of the pierce formula does hold in w₁
+  -- as its premice does not hold in w₁ and its conclusion does hold in w₂
+  PierceHypw₁ : w₁ ⊩ᶠ ((Var "A" ⇒ Var "B") ⇒ Var "A")
+  PierceHypw₁ w₁₁ x = case⊥ (NotABw₁ x)
+  PierceHypw₁ w₁₂ x = w₂A
+  -- So, as the conclusion of the pierce formula does not hold in w₁, the pierce formula doesn't hold.
+  Pierce⊥w₁ h = case⊥ (NotAw₁ (h w₁₁ PierceHypw₁))
+  -- Finally, the formula holds in w₂ as its conclusion is true
+  Pierce⊤w₂ w₂₂ h₂ = w₂A
+
+  -- So, if pierce formula would be provable, it would hold in w₁, which it doesn't
+  -- therefore it is not provable CQFD
+  PierceNotProvable : ¬([] ⊢ PierceF)
+  PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt)
+  
+  
+
+
+
+
+
+
+
+
+
+
+
+

prop.agda

@@ -1,99 +0,0 @@
-{-# OPTIONS --prop #-}
-module prop where
-
-
-open import Agda.Builtin.String using (String)
-open import Data.String.Properties using (_==_)
-open import Data.List using (List; _∷_; [])
-
-
-
-d-C : [] ⊢ ((Var "Q") [⇒] (Var "R")) [⇒] ((Var "P") [⇒] (Var "Q")) [⇒] (Var "P") [⇒] (Var "R")
-d-C = lam (lam (lam (app (succ (succ zero)) (app (succ zero) zero))))
-
-
-ρ₀ : Env
-ρ₀ "P" = ⊥
-ρ₀ "Q" = ⊤
-ρ₀ _ = ⊥
-
-cex-d : ([] ⊢ (((Var "P") [⇒] (Var "Q")) [⇒] (Var "P"))) → ⊥
-cex-d h = ⟦ h ⟧d {ρ₀} tt λ x → tt
-
-
-
-Pierce = {P Q : Prop} → ((P → Q) → P) → P
-TND : Prop → Prop
-TND P = P ∨ (¬ P)
-
-P→TND : Pierce → {P : Prop} → TND P
-nnTND : {P : Prop} → ¬ (¬ (P ∨ ¬ P))
-nnTND ntnd = ntnd (inj₂ λ p → ntnd (inj₁ p))
-P→TND pierce {P} = pierce {TND P} {⊥} (λ p → case⊥ (nnTND p))
-
-
-
-{- Kripke Models -}
-
-
-{- Pierce is not provable -}
-
-module PierceWorld where
-  data Worlds : Set where
-    w₁ w₂ : Worlds
-  data _≤_ : Worlds → Worlds → Prop where
-    w₁₁ : w₁ ≤ w₁
-    w₁₂ : w₁ ≤ w₂
-    w₂₂ : w₂ ≤ w₂
-  data _⊩_ : Worlds → String → Prop where
-    w₂A : w₂ ⊩ "A"
-
-  refl≤ : {w : Worlds} → w ≤ w
-  refl≤ {w₁} = w₁₁
-  refl≤ {w₂} = w₂₂
-  tran≤ : {w w' w'' : Worlds} → w ≤ w' → w' ≤ w'' → w ≤ w''
-  tran≤ w₁₁ z = z
-  tran≤ w₁₂ w₂₂ = w₁₂
-  tran≤ w₂₂ w₂₂ = w₂₂
-  mon⊩ : {a b : Worlds} → a ≤ b → {p : String} → a ⊩ p → b ⊩ p
-  mon⊩ w₂₂ w₂A = w₂A
-  
-PierceW : Kripke
-PierceW = record {PierceWorld}
-
-FaultyPierce : Form 
-FaultyPierce = (((Var "A" [⇒] Var "B") [⇒] Var "A") [⇒] Var "A")
-
-{- Pierce formula is false in world 1 -}
-Pierce⊥w₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ FaultyPierce)
-PierceHypw₁ : Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ ((Var "A" [⇒] Var "B") [⇒] Var "A")
-NotAw₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ (Var "A"))
-NotAw₁ ()
-NotBw₂ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₂ (Var "B"))
-NotBw₂ ()
-NotABw₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ (Var "A" [⇒] Var "B"))
-NotABw₁ h = NotBw₂ (h PierceWorld.w₁₂ PierceWorld.w₂A)
-PierceHypw₁ PierceWorld.w₁₁ x = case⊥ (NotABw₁ x)
-PierceHypw₁ PierceWorld.w₁₂ x = PierceWorld.w₂A
-Pierce⊥w₁ h = case⊥ (NotAw₁ (h PierceWorld.w₁₁ PierceHypw₁))
-{- Pierce formula is true in world 2 -}
-Pierce⊤w₂ : Kripke._⊩ᶠ_ PierceW PierceWorld.w₂ FaultyPierce
-Pierce⊤w₂ PierceWorld.w₂₂ h₂ = PierceWorld.w₂A
-PierceImpliesw₁ : ([] ⊢ FaultyPierce) → (Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ FaultyPierce)
-PierceImpliesw₁ h = Kripke.⟦_⟧ PierceW h {PierceWorld.w₁} tt
-NotProvable : ¬([] ⊢ FaultyPierce)
-NotProvable h = Pierce⊥w₁ (PierceImpliesw₁ h)
-
-
-
-
-
-
-
-
-
-
-
-
-
-