Add formalization of substructural logics in src

CHANGELOG/mlebar-UC.md

@@ -0,0 +1 @@
+* Added a folder "Logic" in src. This provides a formalization of several substructural logics based on chapter 2 of Greg Restall's "An Introduction to Substructural Logics". My hope is that this can provide a useful framework for anyone wanting to study a variety of logics in Agda. This was a master's research project done under Professor Stuart Kurtz, and I'm really happy with my work here - I would love to contribute to the standard library, and I am happy to make any appropriate modification to help with that.

src/Logic/Connectives/And-Logic.agda

@@ -0,0 +1,63 @@
+----------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Logic with 'and' connective + related proof
+----------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Logic.Connectives.And-Logic where
+
+open import Logic.Logic
+
+record And-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct )
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∧_ : Lang → Lang → Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_  _⇒_
+    and-introduction :
+      ∀ {X : Struct} {A B : Lang} →
+      X ⊢ A →
+      X ⊢ B →
+      -------------------
+      X ⊢ (A ∧ B)
+    and-elimination-1 :
+      ∀ {X : Struct} {A B : Lang} →
+      X ⊢ (A ∧ B) →
+      -------------------
+      X ⊢ A
+    and-elimination-2 :
+      ∀ {X : Struct} {A B : Lang} →
+      X ⊢ (A ∧ B) →
+      -------------------
+      X ⊢ B
+
+if-and-distrib :
+  ∀ (Lang : Set) (Struct : Set)
+  (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∧_ : Lang → Lang → Lang) →
+  And-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ → ∀ {A B C : Lang}  →
+  -----------------------------------------------------------------
+  (S ((A ⇒ B) ∧ (A ⇒ C))) ⊢ (A ⇒ (B ∧ C))
+
+-- proof from page 34
+if-and-distrib Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ x =
+  Logic.if-introduction y
+    (And-Logic.and-introduction x
+      (Logic.if-elimination y
+        (And-Logic.and-elimination-1 x
+          (Logic.hypothesis y))
+        (Logic.hypothesis y))
+      (Logic.if-elimination y
+        (And-Logic.and-elimination-2 x
+          (Logic.hypothesis y))
+        (Logic.hypothesis y)))
+    where
+    y = And-Logic.is-logic x
+

src/Logic/Connectives/Backif-Logic.agda

@@ -0,0 +1,62 @@
+----------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Logic with backward conditional connective +
+-- related proof
+----------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Logic.Connectives.Backif-Logic where
+
+open import Logic.Logic
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+
+record Backif-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct )
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _⇐_ : Lang → Lang → Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_  _⇒_
+
+    backif-introduction :
+      ∀ {X : Struct} {A B : Lang} →
+      ((S A) ⨾ X) ⊢ B →
+      -------------------
+      X ⊢ (B ⇐ A)
+
+    backif-elimination :
+      ∀ {X Y : Struct} {A B : Lang} →
+      X ⊢ (B ⇐ A) →
+      Y ⊢ A →
+      -------------------
+      (Y ⨾ X) ⊢ B
+
+
+-- Uniqueness of back-conditionals
+backif-unique :
+  ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _⇐₁_ _⇐₂_ : Lang → Lang → Lang) →
+  Backif-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐₁_ →
+  Backif-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐₂_ →
+  ∀ {A B : Lang} →
+  ---------------------------------------------------------
+  (S (A ⇐₁ B)) ⊢ (A ⇐₂ B) × (S (A ⇐₂ B)) ⊢ (A ⇐₁ B)
+
+backif-unique Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐₁_ _⇐₂_ x y =
+  ⟨ (Backif-Logic.backif-introduction y
+      (Backif-Logic.backif-elimination x
+        (Logic.hypothesis z)
+        (Logic.hypothesis w))) ,
+      Backif-Logic.backif-introduction x
+        (Backif-Logic.backif-elimination y
+          (Logic.hypothesis w)
+          (Logic.hypothesis z)) ⟩
+    where
+    z = Backif-Logic.is-logic x
+    w = Backif-Logic.is-logic y

src/Logic/Connectives/Fusion-Logic.agda

@@ -0,0 +1,62 @@
+----------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Logic with 'fusion' connective + related proof
+----------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Logic.Connectives.Fusion-Logic where
+
+open import Logic.Logic
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+
+record Fusion-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∘_ : Lang → Lang → Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_
+
+    fusion-introduction :
+      ∀ {X Y : Struct} {A B : Lang} →
+      X ⊢ A → Y ⊢ B →
+      -------------------
+      (X ⨾ Y) ⊢ (A ∘ B)
+
+    fusion-elimination :
+      ∀ {X : Struct} {A B C : Lang} →
+      X ⊢ (A ∘ B) →
+      ------------------------------------------
+      C⟨ (S A) ⨾ (S B) ⟩ ⊢ C → C⟨ X ⟩ ⊢ C
+
+
+-- Lemma 2.25 (Uniqueness of fusion)
+fusion-unique :
+  ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∘₁_ _∘₂_ : Lang → Lang → Lang) →
+  Fusion-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘₁_ →
+  Fusion-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘₂_  →
+  ∀ {A B : Lang} →
+  ---------------------------------------------------------
+  (S (A ∘₁ B)) ⊢ (A ∘₂ B) × (S (A ∘₂ B)) ⊢ (A ∘₁ B)
+
+fusion-unique Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘₁_ _∘₂_ x y =
+  ⟨ Logic.context z
+      (Fusion-Logic.fusion-elimination x (Logic.hypothesis w))
+      (Fusion-Logic.fusion-introduction y
+          (Logic.hypothesis w)
+          (Logic.hypothesis w)) ,
+    Logic.context w
+      (Fusion-Logic.fusion-elimination y (Logic.hypothesis z))
+      (Fusion-Logic.fusion-introduction x
+          (Logic.hypothesis z)
+          (Logic.hypothesis z)) ⟩
+    where
+    z = Fusion-Logic.is-logic x
+    w = Fusion-Logic.is-logic y

src/Logic/Connectives/Or-Logic.agda

@@ -0,0 +1,89 @@
+----------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Logic with 'or' connective + related proof
+----------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Logic.Connectives.Or-Logic where
+
+open import Logic.Logic
+open import Logic.Connectives.And-Logic
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+
+record Or-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct )
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∨_ : Lang → Lang → Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_  _⇒_
+
+    product-context :
+      ∀ {X Y Z : Struct} {A : Lang} →
+      (C⟨ X ⟩ ⊢ A × C⟨ Y ⟩ ⊢ A → C⟨ Z ⟩ ⊢ A) →
+      X ⊢ A × Y ⊢ A  →
+      ---------
+      Z ⊢ A
+
+    semicolon-product-context-l :
+      ∀ {X Y Z W : Struct} {A : Lang} →
+      (C⟨ X ⟩ ⊢ A × C⟨ Y ⟩ ⊢ A → C⟨ Z ⟩ ⊢ A) →
+      ----------------------------------------
+      (C⟨ W ⨾ X ⟩ ⊢ A × C⟨ W ⨾ Y ⟩ ⊢ A → C⟨ W ⨾ Z ⟩ ⊢ A)
+
+    semicolon-product-context-r :
+      ∀ {X Y Z W : Struct} {A : Lang} →
+      (C⟨ X ⟩ ⊢ A × C⟨ Y ⟩ ⊢ A → C⟨ Z ⟩ ⊢ A) →
+      ----------------------------------------
+      (C⟨ X ⨾ W ⟩ ⊢ A × C⟨ Y ⨾ W ⟩ ⊢ A → C⟨ Z ⨾ W ⟩ ⊢ A)
+
+    or-introduction-1 :
+      ∀ {X : Struct} {A B : Lang} →
+      X ⊢ A →
+      ---------
+      X ⊢ (A ∨ B)
+
+    or-introduction-2 :
+      ∀ {X : Struct} {A B : Lang} →
+      X ⊢ B →
+      ---------------
+      X ⊢ (A ∨ B)
+
+    or-elimination :
+      ∀ {X : Struct} {A B C : Lang} →
+      X ⊢ (A ∨ B) →
+      --------------------------------------------------
+      (C⟨ (S A) ⟩ ⊢ C × C⟨ (S B) ⟩ ⊢ C  → C⟨ X ⟩ ⊢ C)
+
+
+or-if-distrib :
+  ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∧_ _∨_ : Lang → Lang → Lang) →
+  Or-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∨_ →
+  And-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ →
+  ∀ {A B C : Lang} →
+  ---------------------------------------
+  S ((A ⇒ C) ∧ (B ⇒ C)) ⊢ ((A ∨ B) ⇒ C)
+
+or-if-distrib Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ _∨_ x y =
+   Logic.if-introduction z
+    (Or-Logic.product-context x
+      (Or-Logic.semicolon-product-context-l x
+        (Or-Logic.or-elimination x
+          (Logic.hypothesis z)))
+      ⟨ Logic.if-elimination z
+        (And-Logic.and-elimination-1 y
+          (Logic.hypothesis z))
+        (Logic.hypothesis z) ,
+        Logic.if-elimination z
+          (And-Logic.and-elimination-2 y
+            (Logic.hypothesis z))
+          (Logic.hypothesis z) ⟩)
+    where
+    z = Or-Logic.is-logic x

src/Logic/Connectives/Trivial-Logic.agda

@@ -0,0 +1,60 @@
+----------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Logic with 'trivial truth' connective + related proof
+----------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Logic.Connectives.Trivial-Logic where
+
+open import Logic.Logic
+open import Logic.Punctuation.Leftid-Logic
+open import Logic.Connectives.Truth-Logic
+open import Logic.Structural-Rules.K-Logic
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+
+
+record Trivial-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct )
+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ : Lang → Lang → Lang)
+  (⊤ ⊥ : Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_  _⇒_
+
+    ⊤-introduction :
+      ∀ {X : Struct} →
+      ---------
+      X ⊢ ⊤
+
+    ⊥-elimination :
+      ∀ {X : Struct} {A : Lang} →
+      X ⊢ ⊥ →
+      ------------
+      C⟨ X ⟩ ⊢ A
+
+-- Lemma 2.32
+t-⊤-equiv :
+  ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct)
+  (_⊢_ : Struct → Lang → Set)
+  (C⟨_⟩ : Struct → Struct)
+  (_⨾_ : Struct → Struct → Struct) (∅ : Struct)
+  (_⇒_ : Lang → Lang → Lang)  (t ⊤ ⊥ : Lang) →
+  Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t →
+  Trivial-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ ⊤ ⊥ →
+  K-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ →
+  ------------------------------------------
+  ∀ {A B : Lang} → (S t) ⊢ ⊤  × (S ⊤) ⊢ t
+
+t-⊤-equiv Lang Struct S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_  t ⊤ ⊥ x y z =
+  ⟨ (Trivial-Logic.⊤-introduction y) ,
+    Logic.context w
+      (lPo-Logic.left-pop u)
+        (Logic.context w (K-Logic.weaken z) (Truth-Logic.t-introduction x)) ⟩
+    where
+    w = K-Logic.is-logic z
+    v = Truth-Logic.is-leftid-Logic x
+    u = Leftid-Logic.is-left-pop v