Merge branch 'master' into adding-conjunction

Incomplete proofs of theorems with \and\and

ListUtil.agda

@@ -9,11 +9,25 @@ module ListUtil where
       T : Set₀
       L : List T
       L' : List T
+      L'' : List T
       A : T
       B : T
 
 
-  -- Definition of sublists
+  -- Definition of list appartenance
+  -- The definition uses reflexivity and never any kind of equality
+  infix 3 _∈_
+  data _∈_ : T → List T → Prop where
+    zero∈ : A ∈ A ∷ L
+    next∈ : A ∈ L → A ∈ B ∷ L
+
+  {- RELATIONS BETWEEN LISTS -}
+
+  -- We have the following relations
+  --        ↗ ⊂⁰ ↘
+  -- ⊆ → ⊂ → ⊂⁺ → ∈*
+  infix 4 _⊆_ _⊂_ _⊂⁺_ _⊂⁰_ _∈*_
+  {- ⊆ : We can remove elements but only from the head of the list -}
   -- Similar definition : {L L' : List T} → L ⊆ L' ++ L
   data _⊆_ : List T → List T → Prop where
     zero⊆ : L ⊆ L
@@ -25,3 +39,102 @@ module ListUtil where
   retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆
   retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h)
 
+  refl⊆ : L ⊆ L
+  refl⊆ = zero⊆
+
+  tran⊆ : L ⊆ L' → L' ⊆ L'' → L ⊆ L''
+  tran⊆ zero⊆ h2 = h2
+  tran⊆ (next⊆ h1) h2 = tran⊆ h1 (retro⊆ h2)
+  
+  {- ⊂ : We can remove elements anywhere on the list, no duplicates, no reordering -}
+  data _⊂_ : List T → List T → Prop where
+    zero⊂ : [] ⊂ L
+    both⊂ : L ⊂ L' → (A ∷ L) ⊂ (A ∷ L')
+    next⊂ : L ⊂ L' → L ⊂ (A ∷ L')
+
+  ⊆→⊂ : L ⊆ L' → L ⊂ L'
+  refl⊂ : L ⊂ L
+  ⊆→⊂ {L = []} h = zero⊂
+  ⊆→⊂ {L = x ∷ L} zero⊆ = both⊂ (refl⊂)
+  ⊆→⊂ {L = x ∷ L} (next⊆ h) = next⊂ (⊆→⊂ h)
+  refl⊂ = ⊆→⊂ refl⊆
+
+  tran⊂ : L ⊂ L' → L' ⊂ L'' → L ⊂ L''
+  tran⊂ zero⊂ h2 = zero⊂
+  tran⊂ (both⊂ h1) (both⊂ h2) = both⊂ (tran⊂ h1 h2)
+  tran⊂ (both⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (both⊂ h1) h2)
+  tran⊂ (next⊂ h1) (both⊂ h2) = next⊂ (tran⊂ h1 h2)
+  tran⊂ (next⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (next⊂ h1) h2)
+  
+  {- ⊂⁰ : We can remove elements and reorder the list, as long as we don't duplicate the elements -}
+  -----> We do not have unicity of derivation ([A,A] ⊂⁰ [A,A] can be prove by identity or by swapping its two elements
+  --> We could do with some counting function, but ... it would not be nice, would it ?
+  data _⊂⁰_ : List T → List T → Prop where
+    zero⊂⁰ : _⊂⁰_ {T} [] []
+    next⊂⁰ : L ⊂⁰ L' → L ⊂⁰ A ∷ L'
+    both⊂⁰ : L ⊂⁰ L' → A ∷ L ⊂⁰ A ∷ L'
+    swap⊂⁰ : L ⊂⁰ A ∷ B ∷ L' → L ⊂⁰ B ∷ A ∷ L'
+    error  : L ⊂⁰ L'
+    -- TODOTODOTODOTODO Fix this definition
+  {- ⊂⁺ : We can remove and duplicate elements, as long as we don't change the order -}
+  data _⊂⁺_ : List T → List T → Prop where
+    zero⊂⁺ : _⊂⁺_ {T} [] []
+    next⊂⁺ : L ⊂⁺ L' → L ⊂⁺ A ∷ L'
+    dup⊂⁺ : L ⊂⁺ A ∷ L' → A ∷ L ⊂⁺ A ∷ L'
+
+  ⊂→⊂⁺ : L ⊂ L' → L ⊂⁺ L'
+  ⊂→⊂⁺ {L' = []} zero⊂ = zero⊂⁺
+  ⊂→⊂⁺ {L' = x ∷ L'} zero⊂ = next⊂⁺ (⊂→⊂⁺ zero⊂)
+  ⊂→⊂⁺ (both⊂ h) = dup⊂⁺ (next⊂⁺ (⊂→⊂⁺ h))
+  ⊂→⊂⁺ (next⊂ h) = next⊂⁺ (⊂→⊂⁺ h)
+  refl⊂⁺ : L ⊂⁺ L
+  refl⊂⁺ = ⊂→⊂⁺ refl⊂
+  tran⊂⁺ : L ⊂⁺ L' → L' ⊂⁺ L'' → L ⊂⁺ L''
+  tran⊂⁺ zero⊂⁺ zero⊂⁺ = zero⊂⁺
+  tran⊂⁺ zero⊂⁺ (next⊂⁺ h2) = next⊂⁺ h2
+  tran⊂⁺ (next⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (next⊂⁺ h1) h2)
+  tran⊂⁺ (next⊂⁺ h1) (dup⊂⁺ h2) = tran⊂⁺ h1 h2
+  tran⊂⁺ (dup⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (dup⊂⁺ h1) h2)
+  tran⊂⁺ (dup⊂⁺ h1) (dup⊂⁺ h2) = dup⊂⁺ (tran⊂⁺ h1 (dup⊂⁺ h2))
+
+  retro⊂⁺ : A ∷ L ⊂⁺ L' → L ⊂⁺ L'
+  retro⊂⁺ (next⊂⁺ h) = next⊂⁺ (retro⊂⁺ h)
+  retro⊂⁺ (dup⊂⁺ h) = h
+  
+  {- ∈* : We can remove or duplicate elements and we can change their order -}
+  -- The weakest of all relations on lists
+  -- L ∈* L' if all elements of L exists in L' (no consideration for order nor duplication)
+  data _∈*_ : List T → List T → Prop where
+    zero∈* : [] ∈* L
+    next∈* : A ∈ L → L' ∈* L → (A ∷ L') ∈* L
+
+  -- Founding principle
+  mon∈∈* : A ∈ L → L ∈* L' → A ∈ L'
+  mon∈∈* zero∈ (next∈* x hl) = x
+  mon∈∈* (next∈ ha) (next∈* x hl) = mon∈∈* ha hl
+
+  -- We show that the relation is reflexive and is implied by ⊆
+  refl∈* : L ∈* L
+  ⊂⁺→∈* : L ⊂⁺ L' → L ∈* L'
+  refl∈* {L = []} = zero∈*
+  refl∈* {L = x ∷ L} = next∈* zero∈ (⊂⁺→∈* (next⊂⁺ refl⊂⁺))
+  ⊂⁺→∈* zero⊂⁺ = refl∈*
+  ⊂⁺→∈* {L = []} (next⊂⁺ h) = zero∈*
+  ⊂⁺→∈* {L = x ∷ L} (next⊂⁺ h) = next∈* (next∈ (mon∈∈* zero∈ (⊂⁺→∈* h))) (⊂⁺→∈* (retro⊂⁺ (next⊂⁺ h)))
+  ⊂⁺→∈* (dup⊂⁺ h) = next∈* zero∈ (⊂⁺→∈* h)
+
+  -- Allows to grow ∈* to the right
+  right∈* : L ∈* L' → L ∈* (A ∷ L')
+  right∈* zero∈* = zero∈*
+  right∈* (next∈* x h) = next∈* (next∈ x) (right∈* h)
+
+  both∈* : L ∈* L' → (A ∷ L) ∈* (A ∷ L')
+  both∈* zero∈* = next∈* zero∈ zero∈*
+  both∈* (next∈* x h) = next∈* zero∈ (next∈* (next∈ x) (right∈* h))
+
+  tran∈* : L ∈* L' → L' ∈* L'' → L ∈* L''
+  tran∈* {L = []} = λ x x₁ → zero∈*
+  tran∈* {L = x ∷ L} (next∈* x₁ h1) h2 = next∈* (mon∈∈* x₁ h2) (tran∈* h1 h2)
+
+  ⊆→∈* : L ⊆ L' → L ∈* L'
+  ⊆→∈* h = ⊂⁺→∈* (⊂→⊂⁺ (⊆→⊂ h))

Prop.agda

@@ -1,46 +0,0 @@
-{-# OPTIONS --prop #-}
-
-module Prop where
-
-  -- ⊥ is a data with no constructor
-  -- ⊤ is a record with one always-available constructor
-  data ⊥ : Prop where
-  record ⊤ : Prop where
-    constructor tt
-
-
-  data _∨_ : Prop → Prop → Prop where
-    inj₁ : {P Q : Prop} → P → P ∨ Q
-    inj₂ : {P Q : Prop} → Q → P ∨ Q
-  record _∧_ (P Q : Prop) : Prop where
-    constructor ⟨_,_⟩
-    field
-      p : P
-      q : Q
-      
-  infixr 10 _∧_
-  infixr 11 _∨_
-
-  -- ∧ elimination
-  proj₁ : {P Q : Prop} → P ∧ Q → P
-  proj₁ pq = _∧_.p pq
-  proj₂ : {P Q : Prop} → P ∧ Q → Q
-  proj₂ pq = _∧_.q pq
-
-  -- ¬ is a shorthand for « → ⊥ »
-  ¬ : Prop → Prop
-  ¬ P = P → ⊥
-
-  -- ⊥ elimination
-  case⊥ : {P : Prop} → ⊥ → P
-  case⊥ ()
-  
-  -- ∨ elimination
-  dis : {P Q S : Prop} → (P ∨ Q) → (P → S) → (Q → S) → S
-  dis (inj₁ p) ps qs = ps p
-  dis (inj₂ q) ps qs = qs q
-
-
-  -- ⇔ shorthand
-  _⇔_ : Prop → Prop → Prop
-  P ⇔ Q = (P → Q) ∧ (Q → P)

PropUtil.agda

@@ -44,3 +44,9 @@ module PropUtil where
   -- ⇔ shorthand
   _⇔_ : Prop → Prop → Prop
   P ⇔ Q = (P → Q) ∧ (Q → P)
+
+
+  -- Syntactic sugar for writing applications
+  infixr 200 _$_
+  _$_ : {T U : Prop} → (T → U) → T → U
+  h $ t = h t

PropositionalKripke.agda

@@ -60,11 +60,13 @@ module PropositionalKripke (PV : Set) where
 
     {- Soundness -}
     ⟦_⟧ : Γ ⊢ F → Γ ⊫ F
-    ⟦ zero ⟧ = proj₁
+    ⟦ zero zero∈ ⟧ wΓ = proj₁ wΓ
-    ⟦ next p ⟧ = λ x → ⟦ p ⟧ (proj₂ x)
+    ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ)
     ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩
     ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ)
-
+    ⟦ andi p₁ p₂ ⟧ = {!!}
+    ⟦ ande₁ p ⟧ = {!!}
+    ⟦ ande₂ p ⟧ = {!!}
 
 
 
@@ -88,10 +90,10 @@ module PropositionalKripke (PV : Set) where
     ⊩ᶠ→⊢ : {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⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF))
     ⊢→⊩ᶠ {F ∧∧ G} h = {!!}
     ⊩ᶠ→⊢ {Var x} h = h
-    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
     ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = {!!}
 
     -- Finally, we can deduce completeness of the Kripke model
@@ -122,5 +124,50 @@ module PropositionalKripke (PV : Set) where
   
     ⊢→⊩ᶠ {Var x} h = h
     ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF))
+    ⊢→⊩ᶠ {F ∧∧ G} h = ?
     ⊩ᶠ→⊢ {Var x} h = neu⁰ h
-    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
+    ⊩ᶠ→⊢ {F ∧∧ G} h = {!!}
+
+  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 ⊆ 

PropositionalKripkeGeneral.agda

@@ -0,0 +1,157 @@
+{-# OPTIONS --prop #-}
+
+module PropositionalKripkeGeneral (PV : Set) where
+
+  open import ListUtil
+  open import PropUtil
+  open import PropositionalLogic PV using (Form; Var; _⇒_; Con)
+
+  open import PropositionalKripke PV using (Kripke)
+
+  record Preorder (T : Set₀) : Set₁ where
+    constructor order
+    field
+      _≤_ : T → T → Prop
+      refl≤ : {a : T} → a ≤ a
+      tran≤ : {a b c : T} → a ≤ b → b ≤ c → a ≤ c
+
+  [_]ᵒᵖ : {T : Set₀} → Preorder T → Preorder T
+  [_]ᵒᵖ o = order (λ a b → (Preorder._≤_ o) b a) (Preorder.refl≤ o) (λ h₁ h₂ → (Preorder.tran≤ o) h₂ h₁)
+
+  record NormalAndNeutral : Set₁ where
+    field
+      _⊢⁰_ : Con → Form → Prop
+      _⊢*_ : Con → Form → Prop
+      zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F
+      app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G
+      neu⁰ : {Γ : Con} → {x : PV} → Γ ⊢⁰ Var x → Γ ⊢* Var x
+      lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G)
+
+  record NormalizationFrame : Set₁ where
+    field
+      o : Preorder Con
+      nn : NormalAndNeutral
+      retro : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (Preorder._≤_ o) Γ (F ∷ Δ)
+      ⊢tran : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (NormalAndNeutral._⊢⁰_ nn) Γ F → (NormalAndNeutral._⊢⁰_ nn) Δ F
+
+    open Preorder o
+    open NormalAndNeutral nn
+
+    all : Con → PV → Prop
+    all Γ x = ⊤
+  
+    UK : Kripke
+    UK = record {
+       Worlds = Con;
+       _≤_ = _≤_;
+       refl≤ = refl≤;
+       tran≤ = tran≤;
+       _⊩_ = λ Γ x → Γ ⊢⁰ Var x;
+       mon⊩ = λ Γ h → ⊢tran Γ h
+       }
+
+    open Kripke UK
+    
+    -- q is quote, u is unquote
+    q : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F
+    u : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F
+  
+    u {Var x} h = h
+    u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF))
+    q {Var x} h = neu⁰ h
+    q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero)))
+
+
+
+
+  module NormalizationTests where
+
+    {- Now using our records -}
+    open import PropositionalLogic PV hiding (Form; Var; _⇒_; Con)
+
+
+    ClassicNN : NormalAndNeutral
+    ClassicNN = record
+      {
+      _⊢⁰_ = _⊢⁰_ ;
+      _⊢*_ = _⊢*_ ;
+      zero = zero zero∈ ;
+      app = app ;
+      neu⁰ = neu⁰ ;
+      lam = lam
+      }
+
+    BiggestNN : NormalAndNeutral
+    BiggestNN = record
+      {
+      _⊢⁰_ = _⊢_ ;
+      _⊢*_ = _⊢_ ;
+      zero = zero zero∈ ;
+      app = app ;
+      neu⁰ = λ x → x ;
+      lam = lam
+      }
+
+    PO⊢⁺  = [ order {Con} _⊢⁺_  refl⊢⁺  tran⊢⁺  ]ᵒᵖ
+    PO⊢⁰⁺ = [ order {Con} _⊢⁰⁺_ refl⊢⁰⁺ tran⊢⁰⁺ ]ᵒᵖ
+    PO∈*  = order {Con} _∈*_  refl∈*  tran∈*
+    PO⊂⁺  = order {Con} _⊂⁺_  refl⊂⁺  tran⊂⁺
+    PO⊂   = order {Con} _⊂_   refl⊂   tran⊂
+    PO⊆   = order {Con} _⊆_   refl⊆   tran⊆
+    
+    -- Completeness Proofs
+    Frame⊢ : NormalizationFrame
+    Frame⊢ = record
+      {
+      o = PO⊢⁺ ;
+      nn = BiggestNN ;
+      retro = λ s → addhyp⊢⁺ (right∈* refl∈*) s ;
+      ⊢tran = halftran⊢⁺
+      }
+
+    Frame⊢⁰ : NormalizationFrame
+    Frame⊢⁰ = record
+      {
+      o = PO⊢⁰⁺ ;
+      nn = ClassicNN ;
+      retro = λ s → addhyp⊢⁰⁺ (right∈* refl∈*) s ;
+      ⊢tran = halftran⊢⁰⁺⁰
+      }
+
+    Frame∈* : NormalizationFrame
+    Frame∈* = record
+      {
+      o = PO∈* ;
+      nn = ClassicNN ;
+      retro = right∈* ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ s) h
+      }
+
+    Frame⊂⁺ : NormalizationFrame
+    Frame⊂⁺ = record
+      {
+      o = PO⊂⁺ ;
+      nn = ClassicNN ;
+      retro = next⊂⁺ ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* s) h
+      }
+
+    Frame⊂ : NormalizationFrame
+    Frame⊂ = record
+      {
+      o = PO⊂ ;
+      nn = ClassicNN ;
+      retro = next⊂ ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ s) h
+      }
+
+    Frame⊆ : NormalizationFrame
+    Frame⊆ = record
+      {
+      o = PO⊆ ;
+      nn = ClassicNN ;
+      retro = next⊆ ;
+      ⊢tran =  λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ $ ⊆→⊂ s) h
+      }
+
+    

PropositionalLogic.agda

@@ -27,6 +27,7 @@ module PropositionalLogic (PV : Set) where
       G   : Form
       Γ   : Con
       Γ'  : Con
+      Γ'' : Con
       x   : PV
 
 
@@ -34,8 +35,7 @@ module PropositionalLogic (PV : Set) where
   {--- DEFINITION OF ⊢ ---}
   
   data _⊢_ : Con → Form → Prop where
-    zero : (A ∷ Γ) ⊢ A
+    zero : A ∈ Γ → Γ ⊢ A
-    next : Γ ⊢ A → (B ∷ Γ) ⊢ A
     lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B)
     app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B
     andi : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧∧ B
@@ -44,34 +44,52 @@ module PropositionalLogic (PV : Set) where
 
   infix 5 _⊢_
   
+  zero⊢ : (A ∷ Γ) ⊢ A
+  zero⊢ = zero zero∈
+  one⊢ : (B ∷ A ∷ Γ) ⊢ A
+  one⊢ = zero (next∈ zero∈)
+
+  -- We can add hypotheses to a proof
+  addhyp⊢ : Γ ∈* Γ' → Γ ⊢ A → Γ' ⊢ A
+  addhyp⊢ s (zero x) = zero (mon∈∈* x s)
+  addhyp⊢ s (lam h) = lam (addhyp⊢ (both∈* s) h)
+  addhyp⊢ s (app h h₁) = app (addhyp⊢ s h) (addhyp⊢ s h₁)
+  addhyp⊢ s (andi h₁ h₂) = andi (addhyp⊢ s h₁) (addhyp⊢ s h₂)
+  addhyp⊢ s (ande₁ h) = ande₁ (addhyp⊢ s h)
+  addhyp⊢ s (ande₂ h) = ande₂ (addhyp⊢ s h)
+
   -- Extension of ⊢ to contexts
   _⊢⁺_ : Con → Con → Prop
   Γ ⊢⁺ [] = ⊤
   Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ')
   infix 5 _⊢⁺_
 
+  -- We show that the relation respects ∈*
+
+  mon∈*⊢⁺ : Γ' ∈* Γ → Γ ⊢⁺ Γ'
+  mon∈*⊢⁺ zero∈* = tt
+  mon∈*⊢⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁺ h) ⟩
+
   -- The relation respects ⊆
   mon⊆⊢⁺ : Γ' ⊆ Γ → Γ ⊢⁺ Γ'
-  mon⊆⊢⁺ {[]} sub = tt
+  mon⊆⊢⁺ h = mon∈*⊢⁺ (⊆→∈* h)
-  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⊆) ⟩
 
-  -- We can add hypotheses to the left 
+  -- We can add hypotheses to to a proof
-  addhyp⊢⁺ : Γ ⊢⁺ Γ' → (A ∷ Γ) ⊢⁺ Γ'
+  addhyp⊢⁺ : Γ ∈* Γ' → Γ ⊢⁺ Γ'' → Γ' ⊢⁺ Γ''
-  addhyp⊢⁺ {Γ' = []} h = tt
+  addhyp⊢⁺ {Γ'' = []} s h = tt
-  addhyp⊢⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺ (proj₂ h) ⟩
+  addhyp⊢⁺ {Γ'' = x ∷ Γ''} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢ s Γx , addhyp⊢⁺ s ΓΓ'' ⟩
   
   -- The relation respects ⊢
   halftran⊢⁺ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F
-  halftran⊢⁺ h⁺ zero = proj₁ h⁺
+  halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺
-  halftran⊢⁺ h⁺ (next h) = halftran⊢⁺ (proj₂ h⁺) h
+  halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero (next∈ x)) = halftran⊢⁺ (proj₂ h⁺) (zero x)
-  halftran⊢⁺ h⁺ (lam h) = lam (halftran⊢⁺ ⟨ zero , addhyp⊢⁺ h⁺ ⟩ h)
+  halftran⊢⁺ h⁺ (lam h) = lam (halftran⊢⁺ ⟨ (zero zero∈) , (addhyp⊢⁺ (right∈* refl∈*) h⁺) ⟩ h)
-  halftran⊢⁺ h⁺ (app h h') = app (halftran⊢⁺ h⁺ h) (halftran⊢⁺ h⁺ h')
+  halftran⊢⁺ h⁺ (app h h₁) = app (halftran⊢⁺ h⁺ h) (halftran⊢⁺ h⁺ h₁)
   halftran⊢⁺ h⁺ (andi hf hg) = andi (halftran⊢⁺ h⁺ hf) (halftran⊢⁺ h⁺ hg)
   halftran⊢⁺ h⁺ (ande₁ hfg) = ande₁ (halftran⊢⁺ h⁺ hfg)
   halftran⊢⁺ h⁺ (ande₂ hfg) = ande₂ (halftran⊢⁺ h⁺ hfg)
@@ -89,8 +107,7 @@ module PropositionalLogic (PV : Set) where
   -- ⊢* are normal forms
   mutual
     data _⊢⁰_ : Con → Form → Prop where
-      zero : (A ∷ Γ) ⊢⁰ A
+      zero :  A ∈ Γ → Γ ⊢⁰ A
-      next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A
       app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
     data _⊢*_ : Con → Form → Prop where
       neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x
@@ -101,12 +118,19 @@ module PropositionalLogic (PV : Set) where
   -- Both are tighter than ⊢
   ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F
   ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F
-  ⊢⁰→⊢ zero = zero
+  ⊢⁰→⊢ (zero h) = zero h
-  ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h)
   ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x)
   ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x
   ⊢*→⊢ (lam h) = lam (⊢*→⊢ h)
 
+  -- We can add hypotheses to a proof
+  addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A
+  addhyp⊢* : Γ ∈* Γ' → Γ ⊢* A → Γ' ⊢* A
+  addhyp⊢⁰ s (zero x) = zero (mon∈∈* x s)
+  addhyp⊢⁰ s (app h h₁) = app (addhyp⊢⁰ s h) (addhyp⊢* s h₁)
+  addhyp⊢* s (neu⁰ x) = neu⁰ (addhyp⊢⁰ s x)
+  addhyp⊢* s (lam h) = lam (addhyp⊢* (both∈* s) h)
+
   -- Extension of ⊢⁰ to contexts
   -- i.e. there is a neutral proof for any element
   _⊢⁰⁺_ : Con → Con → Prop
@@ -114,29 +138,33 @@ module PropositionalLogic (PV : Set) where
   Γ ⊢⁰⁺ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁰⁺ Γ')
   infix 5 _⊢⁰⁺_
 
+  -- The relation respects ∈*
+
+  mon∈*⊢⁰⁺ : Γ' ∈* Γ → Γ ⊢⁰⁺ Γ'
+  mon∈*⊢⁰⁺ zero∈* = tt
+  mon∈*⊢⁰⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁰⁺ h) ⟩
+
   -- The relation respects ⊆
   mon⊆⊢⁰⁺ : Γ' ⊆ Γ → Γ ⊢⁰⁺ Γ'
-  mon⊆⊢⁰⁺ {[]} sub = tt
+  mon⊆⊢⁰⁺ h = mon∈*⊢⁰⁺ (⊆→∈* h)
-  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⊆) ⟩
+  refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero zero∈ , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩
 
   -- A useful lemma, that we can add hypotheses 
-  addhyp⊢⁰⁺ : Γ ⊢⁰⁺ Γ' → (A ∷ Γ) ⊢⁰⁺ Γ'
+  addhyp⊢⁰⁺ : Γ ∈* Γ' → Γ ⊢⁰⁺ Γ'' → Γ' ⊢⁰⁺ Γ''
-  addhyp⊢⁰⁺ {Γ' = []} h = tt
+  addhyp⊢⁰⁺ {Γ'' = []} s h = tt
-  addhyp⊢⁰⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁰⁺ (proj₂ h) ⟩
+  addhyp⊢⁰⁺ {Γ'' = A ∷ Γ'} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢⁰ s Γx , addhyp⊢⁰⁺ s ΓΓ'' ⟩
 
   -- 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⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero zero∈ , addhyp⊢⁰⁺ (right∈* refl∈*) h⁺ ⟩ h)
-  halftran⊢⁰⁺⁰ h⁺ zero = proj₁ h⁺
+  halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺
-  halftran⊢⁰⁺⁰ h⁺ (next h) = halftran⊢⁰⁺⁰ (proj₂ h⁺) h
+  halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero (next∈ h)) = halftran⊢⁰⁺⁰ (proj₂ h⁺) (zero h)
   halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h')
 
   -- The relation is transitive
@@ -161,8 +189,8 @@ module PropositionalLogic (PV : Set) where
   ⟦ A ∷ Γ ⟧ᶜ ρ = (⟦ A ⟧ᶠ ρ) ∧ (⟦ Γ ⟧ᶜ ρ)
 
   ⟦_⟧ᵈ : Γ ⊢ A → {ρ : Env} → ⟦ Γ ⟧ᶜ ρ → ⟦ A ⟧ᶠ ρ
-  ⟦ zero ⟧ᵈ p = proj₁ p
+  ⟦_⟧ᵈ {x ∷ Γ} (zero zero∈) p = proj₁ p
-  ⟦ next th ⟧ᵈ p = ⟦ th ⟧ᵈ (proj₂ p)
+  ⟦_⟧ᵈ {x ∷ Γ} (zero (next∈ h)) p = ⟦ zero h ⟧ᵈ (proj₂ p)
   ⟦ lam th ⟧ᵈ = λ pₐ p₀ → ⟦ th ⟧ᵈ ⟨ p₀ , pₐ ⟩
   ⟦ app th₁ th₂ ⟧ᵈ = λ p → ⟦ th₁ ⟧ᵈ p (⟦ th₂ ⟧ᵈ p)
   ⟦ andi hf hg ⟧ᵈ = λ p → ⟨ ⟦ hf ⟧ᵈ p , ⟦ hg ⟧ᵈ p ⟩
@@ -184,8 +212,7 @@ module PropositionalLogic (PV : Set) where
     app : ⊢sk (A ⇒ B) → ⊢sk A → ⊢sk B
 
   data _⊢skC_ : Con → Form → Prop where
-    zero : (A ∷ Γ) ⊢skC A
+    zero : A ∈ Γ → Γ ⊢skC A
-    next : Γ ⊢skC A → (B ∷ Γ) ⊢skC A
     SS : Γ ⊢skC ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
     KK : Γ ⊢skC (A ⇒ B ⇒ A)
     ANDi : Γ ⊢skC (A ⇒ B ⇒ (A ∧∧ B))
@@ -197,11 +224,11 @@ module PropositionalLogic (PV : Set) where
   ⊢⇔⊢sk : ([] ⊢ A) ⇔ ⊢sk A
   
   ⊢sk→⊢ :  ⊢sk A → ([] ⊢ A)
-  ⊢sk→⊢ SS = lam (lam (lam ( app (app (next (next zero)) zero) (app (next zero) zero))))
+  ⊢sk→⊢ SS = lam (lam (lam ( app (app (zero $ next∈ $ next∈ zero∈) (zero zero∈)) (app (zero $ next∈ $ zero∈) (zero zero∈)))))
-  ⊢sk→⊢ KK = lam (lam (next zero))
+  ⊢sk→⊢ KK = lam (lam (zero $ next∈ $ zero∈))
-  ⊢sk→⊢ ANDi = lam (lam (andi (next zero) zero))
+  ⊢sk→⊢ ANDi = lam (lam (andi (zero $ next∈ $ zero∈) (zero zero∈)))
-  ⊢sk→⊢ ANDe₁ = lam (ande₁ zero)
+  ⊢sk→⊢ ANDe₁ = lam (ande₁ (zero zero∈))
-  ⊢sk→⊢ ANDe₂ = lam (ande₂ zero)
+  ⊢sk→⊢ ANDe₂ = lam (ande₂ (zero zero∈))
   ⊢sk→⊢ (app x x₁) = app (⊢sk→⊢ x) (⊢sk→⊢ x₁)
 
   skC→sk : [] ⊢skC A → ⊢sk A
@@ -216,8 +243,8 @@ module PropositionalLogic (PV : Set) where
   lam-sk : (A ∷ Γ) ⊢skC B → Γ ⊢skC (A ⇒ B)
   lam-sk-zero : Γ ⊢skC (A ⇒ A)
   lam-sk-zero {A = A} = app (app SS KK) (KK {B = A})
-  lam-sk zero = lam-sk-zero
+  lam-sk (zero zero∈) = lam-sk-zero
-  lam-sk (next x) = app KK x
+  lam-sk (zero (next∈ h)) = app KK (zero h)
   lam-sk SS = app KK SS
   lam-sk KK = app KK KK
   lam-sk ANDi = app KK (app (app SS (app (app SS (app KK SS)) (app (app SS (app KK KK)) (app (app SS (app KK ANDi)) (lam-sk-zero))))) (app KK lam-sk-zero))
@@ -227,8 +254,7 @@ module PropositionalLogic (PV : Set) where
 
   
   ⊢→⊢skC : Γ ⊢ A → Γ ⊢skC A
-  ⊢→⊢skC zero = zero
+  ⊢→⊢skC (zero h) = zero h
-  ⊢→⊢skC (next x) = next (⊢→⊢skC x)
   ⊢→⊢skC (lam x) = lam-sk (⊢→⊢skC x)
   ⊢→⊢skC (app x x₁) = app (⊢→⊢skC x) (⊢→⊢skC x₁)
   ⊢→⊢skC (andi x y) = app (app ANDi (⊢→⊢skC x)) (⊢→⊢skC y)

Readme.agda

@@ -12,7 +12,7 @@ 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))))
+d-C = lam (lam (lam (app (zero $ next∈ $ next∈ zero∈) (app (zero $ next∈ zero∈) (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
@@ -115,15 +115,39 @@ module PierceDisproof where
   PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt)
   
   
-
+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 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
+  open import PropositionalKripkeGeneral String
+
+  -- We now have access to quote and unquote functions with this
+  u1 = NormalizationFrame.u NormalizationTests.Frame⊢
+  q1 = NormalizationFrame.q NormalizationTests.Frame⊢
+  u2 = NormalizationFrame.u NormalizationTests.Frame⊢⁰
+  q2 = NormalizationFrame.q NormalizationTests.Frame⊢⁰
+  u3 = NormalizationFrame.u NormalizationTests.Frame∈*
+  q3 = NormalizationFrame.q NormalizationTests.Frame∈*
+  u4 = NormalizationFrame.u NormalizationTests.Frame⊂⁺
+  q4 = NormalizationFrame.q NormalizationTests.Frame⊂⁺
+  u5 = NormalizationFrame.u NormalizationTests.Frame⊂
+  q5 = NormalizationFrame.q NormalizationTests.Frame⊂
+  u6 = NormalizationFrame.u NormalizationTests.Frame⊆
+  q6 = NormalizationFrame.q NormalizationTests.Frame⊆