From d1a0177d2c8717926beb13865aa214195526affd Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Thu, 25 May 2023 12:02:36 +0200
Subject: [PATCH] tinied up everything in enclosed files, with normalized
 notation

---
 .gitignore               |   4 +-
 Prop.agda                |  46 ++++++++++++
 PropUtil.agda            |  46 ++++++++++++
 PropositionalKripke.agda | 120 +++++++++++++++++++++++++++++
 PropositionalLogic.agda  | 158 +++++++++++++++++++++++++++++++++++++++
 5 files changed, 373 insertions(+), 1 deletion(-)
 create mode 100644 Prop.agda
 create mode 100644 PropUtil.agda
 create mode 100644 PropositionalKripke.agda
 create mode 100644 PropositionalLogic.agda

diff --git a/.gitignore b/.gitignore
index a64485f..5afa5d4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 *.agdai
 *~
-
+\#*\#
+.\#*
+*.kate-swp
diff --git a/Prop.agda b/Prop.agda
new file mode 100644
index 0000000..ab70ae5
--- /dev/null
+++ b/Prop.agda
@@ -0,0 +1,46 @@
+{-# 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)
diff --git a/PropUtil.agda b/PropUtil.agda
new file mode 100644
index 0000000..69d105c
--- /dev/null
+++ b/PropUtil.agda
@@ -0,0 +1,46 @@
+{-# OPTIONS --prop #-}
+
+module PropUtil 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
+
+  -- ∨ 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
+  
+  -- ¬ is a shorthand for « → ⊥ »
+  ¬ : Prop → Prop
+  ¬ P = P → ⊥
+
+  -- ⊥ elimination
+  case⊥ : {P : Prop} → ⊥ → P
+  case⊥ ()
+  
+  -- ⇔ shorthand
+  _⇔_ : Prop → Prop → Prop
+  P ⇔ Q = (P → Q) ∧ (Q → P)
diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda
new file mode 100644
index 0000000..5720337
--- /dev/null
+++ b/PropositionalKripke.agda
@@ -0,0 +1,120 @@
+{-# OPTIONS --prop #-}
+
+module PropositionalKripke (PV : Set) where
+
+  open import PropUtil
+  open import PropositionalLogic PV
+
+  private
+    variable
+      x : PV
+      y : PV
+      F : Form
+      G : Form
+      Γ : Con
+      Γ' : Con
+      Η : Con
+      Η' : Con
+  
+  record Kripke : Set₁ where
+    field
+      Worlds : Set₀
+      _≤_ : Worlds → Worlds → Prop
+      refl≤ : {w : Worlds} → w ≤ w
+      tran≤ : {a b c : Worlds} → a ≤ b → b ≤ c → a ≤ c
+      _⊩_ : Worlds → PV → Prop
+      mon⊩ : {a b : Worlds} → a ≤ b → {p : PV} → a ⊩ p → b ⊩ p
+
+    private
+      variable
+        w : Worlds
+        w' : Worlds
+        w₁ : Worlds
+        w₂ : Worlds
+        w₃ : Worlds
+    
+    {- Extending ⊩ to Formulas and Contexts -}
+    _⊩ᶠ_ : 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)
+    
+    -- The extensions are monotonous
+    mon⊩ᶠ : w ≤ w' → w ⊩ᶠ F → w' ⊩ᶠ F
+    mon⊩ᶠ {F = Var x} ww' wF = mon⊩ ww' wF
+    mon⊩ᶠ {F = F ⇒ G} ww' wF w'w'' w''F = wF (tran≤ ww' w'w'') w''F
+
+    mon⊩ᶜ : w ≤ w' → w ⊩ᶜ Γ → w' ⊩ᶜ Γ
+    mon⊩ᶜ {Γ = []} ww' wΓ = wΓ
+    mon⊩ᶜ {Γ = F ∷ Γ} ww' wΓ = ⟨ mon⊩ᶠ {F = F}  ww' (proj₁ wΓ) , mon⊩ᶜ ww' (proj₂ wΓ) ⟩
+
+    {- General operator matching the shape of ⊢ -}
+    _⊫_ : Con → Form → Prop
+    Γ ⊫ F = {w : Worlds} → w ⊩ᶜ Γ → w ⊩ᶠ F
+
+    {- Soundness -}
+    ⟦_⟧ : Γ ⊢ F → Γ ⊫ F
+    ⟦ zero ⟧ = proj₁
+    ⟦ next p ⟧ = λ x → ⟦ p ⟧ (proj₂ x)
+    ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩
+    ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ)
+
+
+
+
+  
+  {- 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
+    open Kripke UK
+    open UniversalKripke using (halftran≤)
+
+    ⊩ᶠ→⊢ : {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))
+    ⊩ᶠ→⊢ {Var x} h = h
+    ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+
+    completeness : {F : Form} → [] ⊫ F → [] ⊢ F
+    completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt)
+
+    {- Normalization -}
+    norm : [] ⊢ F → [] ⊢ F
+    norm x = completeness (⟦ x ⟧)
+    -- norm is identity ?!
+    idnorm : norm x ≡ x
+    idnorm = ?
+    -- autonorm : (P₁ P₂ : Prop) → (x₁ : P₁) → (norm x₁ : P₂) → P₁ ≡⊢ P₂
+    -- βηnorm : (P₁ P₂ : Prop) → (x₁ : P₁) → (norm x₁ : P₂) → (x₂ : P₂) → norm x₁ ≡ x₂ → P₁ ≡⊢ P₂
+
+    -- autonorm P = {!!}
+    --βηnorm P₁ P₂ = ?
diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda
new file mode 100644
index 0000000..9cefcc0
--- /dev/null
+++ b/PropositionalLogic.agda
@@ -0,0 +1,158 @@
+{-# OPTIONS --prop #-}
+
+module PropositionalLogic (PV : Set) where
+
+  open import PropUtil
+  open import Data.List using (List; _∷_; []) public
+
+  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
+
+  private
+    variable
+      A   : Form
+      A'  : Form
+      B   : Form
+      B'  : Form
+      C   : Form
+      Γ   : Con
+      Γ'  : Con
+
+  -- 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)
+
+  
+  data _⊢_ : Con → Form → Prop where
+    zero : (A ∷ Γ) ⊢ A
+    next : Γ ⊢ A → (B ∷ Γ) ⊢ A
+    lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B)
+    app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B
+
+  infix 5 _⊢_
+
+  -- Equality of derivation
+  infix 2 _≡⊢_
+  data _≡⊢_ : Prop → Prop → Prop where
+    refl : Γ ⊢ A ≡⊢ Γ ⊢ A
+  {-zero≡⊢ : (A ∷ Γ) ⊢ A ≡⊢ (A' ∷ Γ') ⊢ A'
+    next≡⊢ : Γ ⊢ A ≡⊢ Γ' ⊢ A' → (B ∷ Γ) ⊢ A ≡⊢ (B ∷ Γ') ⊢ A'
+    lam≡⊢ : (A ∷ Γ) ⊢ B ≡⊢ (A' ∷ Γ') ⊢ B' →  Γ ⊢ (A ⇒ B) ≡⊢  Γ' ⊢ (A' ⇒ B')
+    app≡⊢ :  Γ ⊢ (A ⇒ B) ≡⊢  Γ' ⊢ (A' ⇒ B') →  Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ ⊢ B ≡⊢ Γ' ⊢ B'
+  -}
+  {-
+  -- Reflexivity of equality
+  refl≡⊢ : {Γ : Con} → {A : Form} → Γ ⊢ A ≡⊢ Γ ⊢ A
+  refl≡⊢ = {!!}
+
+  -- Symmetry of equality
+  sym≡⊢ : {Γ Γ' : Con} → {A A' : Form} → Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ' ⊢ A' ≡⊢ Γ ⊢ A
+  sym≡⊢ = {!!}
+
+  -- Transitivity of equality
+  tran≡⊢ : {Γ Γ' Γ'' : Con} → {A A' A'' : Form} → Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ' ⊢ A' ≡⊢ Γ'' ⊢ A'' → Γ ⊢ A ≡⊢ Γ'' ⊢ A''
+  tran≡⊢ = {!!}
+  -}
+
+  -- 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) ⟩
+    
+  {--- Simple translation with in an Environment ---}
+
+  Env = PV → Prop
+
+  ⟦_⟧ᶠ : Form → Env → Prop
+  ⟦ Var x ⟧ᶠ ρ = ρ x
+  ⟦ A ⇒ B ⟧ᶠ ρ = (⟦ A ⟧ᶠ ρ) → (⟦ B ⟧ᶠ ρ)
+
+  ⟦_⟧ᶜ : Con → Env → Prop
+  ⟦ [] ⟧ᶜ ρ = ⊤
+  ⟦ A ∷ Γ ⟧ᶜ ρ = (⟦ A ⟧ᶠ ρ) ∧ (⟦ Γ ⟧ᶜ ρ)
+
+  ⟦_⟧ᵈ : Γ ⊢ A → {ρ : Env} → ⟦ Γ ⟧ᶜ ρ → ⟦ A ⟧ᶠ ρ
+  ⟦ zero ⟧ᵈ p = proj₁ p
+  ⟦ next th ⟧ᵈ p = ⟦ th ⟧ᵈ (proj₂ p)
+  ⟦ lam th ⟧ᵈ = λ pₐ p₀ → ⟦ th ⟧ᵈ ⟨ p₀ , pₐ ⟩
+  ⟦ app th₁ th₂ ⟧ᵈ = λ p → ⟦ th₁ ⟧ᵈ p (⟦ th₂ ⟧ᵈ p)
+
+
+  {--- Combinatory Logic ---}
+
+  data ⊢sk : Form → Prop where
+    SS : ⊢sk ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
+    KK : ⊢sk (A ⇒ B ⇒ A)
+    app : ⊢sk (A ⇒ B) → ⊢sk A → ⊢sk B
+
+  data _⊢skC_ : Con → Form → Prop where
+    zero : (A ∷ Γ) ⊢skC A
+    next : Γ ⊢skC A → (B ∷ Γ) ⊢skC A
+    SS : Γ ⊢skC ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
+    KK : Γ ⊢skC (A ⇒ B ⇒ A)
+    app : Γ ⊢skC (A ⇒ B) → Γ ⊢skC A → Γ ⊢skC B
+
+
+  -- combinatory gives the same proofs as classic
+  ⊢⇔⊢sk : ([] ⊢ A) ⇔ ⊢sk A
+  
+  ⊢sk→⊢ :  ⊢sk A → ([] ⊢ A)
+  ⊢sk→⊢ SS = lam (lam (lam ( app (app (next (next zero)) zero) (app (next zero) zero))))
+  ⊢sk→⊢ KK = lam (lam (next zero))
+  ⊢sk→⊢ (app x x₁) = app (⊢sk→⊢ x) (⊢sk→⊢ x₁)
+
+  skC→sk : [] ⊢skC A → ⊢sk A
+  skC→sk SS = SS
+  skC→sk KK = KK
+  skC→sk (app d e) = app (skC→sk d) (skC→sk e)
+
+
+  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 (next x) = app KK x
+  lam-sk SS = app KK SS
+  lam-sk KK = app KK KK
+  lam-sk (app x₁ x₂) = app (app SS (lam-sk x₁)) (lam-sk x₂)
+
+  ⊢→⊢skC : Γ ⊢ A → Γ ⊢skC A
+  ⊢→⊢skC zero = zero
+  ⊢→⊢skC (next x) = next (⊢→⊢skC x)
+  ⊢→⊢skC (lam x) = lam-sk (⊢→⊢skC x)
+  ⊢→⊢skC (app x x₁) = app (⊢→⊢skC x) (⊢→⊢skC x₁)
+
+  ⊢⇔⊢sk = ⟨ (λ x → skC→sk (⊢→⊢skC x)) , ⊢sk→⊢ ⟩