Added a generalized version of the Normalization proof

ListUtil.agda

@@ -9,6 +9,7 @@ module ListUtil where
       T : Set₀
       L : List T
       L' : List T
+      L'' : List T
       A : T
       B : T
 
@@ -38,12 +39,33 @@ 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 ?
@@ -58,7 +80,27 @@ module ListUtil where
   data _⊂⁺_ : List T → List T → Prop where
     zero⊂⁺ : _⊂⁺_ {T} [] []
     next⊂⁺ : L ⊂⁺ L' → L ⊂⁺ A ∷ L'
-    dup⊂⁺ : A ∷ L ⊂⁺ L' → A ∷ 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)
@@ -73,19 +115,26 @@ module ListUtil where
 
   -- We show that the relation is reflexive and is implied by ⊆
   refl∈* : L ∈* L
-  ⊆→∈* : L ⊆ L' → L ∈* L'
+  ⊂⁺→∈* : L ⊂⁺ L' → L ∈* L'
   refl∈* {L = []} = zero∈*
-  refl∈* {L = x ∷ L} = next∈* zero∈ (⊆→∈* (next⊆ zero⊆))
+  refl∈* {L = x ∷ L} = next∈* zero∈ (⊂⁺→∈* (next⊂⁺ refl⊂⁺))
-  ⊆→∈* zero⊆ = refl∈*
+  ⊂⁺→∈* zero⊂⁺ = refl∈*
-  ⊆→∈* {L = []} (next⊆ h) = zero∈*
+  ⊂⁺→∈* {L = []} (next⊂⁺ h) = zero∈*
-  ⊆→∈* {L = x ∷ L} (next⊆ h) = next∈* (next∈ (mon∈∈* zero∈ (⊆→∈* h))) (⊆→∈* (retro⊆ (next⊆ h)))
+  ⊂⁺→∈* {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)
 
-  -- Allows to grow ∈* from both sides
   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

@@ -58,8 +58,8 @@ 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Γ)
 
@@ -86,9 +86,9 @@ 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))
     ⊩ᶠ→⊢ {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∈))))
 
     -- Finally, we can deduce completeness of the Kripke model
     completeness : {F : Form} → [] ⊫ F → [] ⊢ F
@@ -119,7 +119,7 @@ module PropositionalKripke (PV : Set) where
     ⊢→⊩ᶠ {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 ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) 
 
   module OtherProofs where
 
@@ -135,13 +135,31 @@ module PropositionalKripke (PV : Set) where
   
     
   
-    {- Renamings -}
+    {- Renamings : ∈* -}
-
+    UK∈* : Kripke
-    {- Weakening anywhere, order preserving, duplication authorized -}
+    UK∈* = record {
-
+      Worlds = Con;
-    {- Weakening anywhere, no duplication, order preserving -}
+      _≤_ = _∈*_;
+      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 -}
+    {- 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
+      }
+
+    

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⊆