From bf20aed4e427a97da2df8201e4c256005f61d0d0 Mon Sep 17 00:00:00 2001 From: mlebar-UC Date: Thu, 4 Sep 2025 16:49:19 -0500 Subject: [PATCH] Add formalization of substructural logics in src --- CHANGELOG/mlebar-UC.md | 1 + fix-whitespace | 1 + src/Logic/Connectives/And-Logic.agda | 63 +++++++++++++++ src/Logic/Connectives/Backif-Logic.agda | 62 +++++++++++++++ src/Logic/Connectives/Fusion-Logic.agda | 62 +++++++++++++++ src/Logic/Connectives/Or-Logic.agda | 89 +++++++++++++++++++++ src/Logic/Connectives/Trivial-Logic.agda | 60 +++++++++++++++ src/Logic/Connectives/Truth-Logic.agda | 55 +++++++++++++ src/Logic/Logic.agda | 94 +++++++++++++++++++++++ src/Logic/Logics/BCK-Logic.agda | 28 +++++++ src/Logic/Logics/E+-Logic.agda | 29 +++++++ src/Logic/Logics/Full-Conn-Logic.agda | 40 ++++++++++ src/Logic/Logics/J-Logic.agda | 28 +++++++ src/Logic/Logics/L-Logic.agda | 32 ++++++++ src/Logic/Logics/LI-Logic.agda | 29 +++++++ src/Logic/Logics/MALL+-Logic.agda | 30 ++++++++ src/Logic/Logics/Minimal-Logic.agda | 38 +++++++++ src/Logic/Logics/Or-Comma-Logic.agda | 42 ++++++++++ src/Logic/Logics/P-Logic.agda | 28 +++++++ src/Logic/Logics/R+-Logic.agda | 30 ++++++++ src/Logic/Logics/RM+-Logic.agda | 27 +++++++ src/Logic/Logics/T+-Logic.agda | 28 +++++++ src/Logic/Logics/TW+-Logic.agda | 44 +++++++++++ src/Logic/Punctuation/Comma-Logic.agda | 56 ++++++++++++++ src/Logic/Punctuation/Leftid-Logic.agda | 90 ++++++++++++++++++++++ src/Logic/Punctuation/Rightid-Logic.agda | 76 ++++++++++++++++++ src/Logic/Structural-Rules/B'-logic.agda | 26 +++++++ src/Logic/Structural-Rules/B-logic.agda | 51 ++++++++++++ src/Logic/Structural-Rules/B^c-logic.agda | 26 +++++++ src/Logic/Structural-Rules/C-logic.agda | 51 ++++++++++++ src/Logic/Structural-Rules/CI-logic.agda | 49 ++++++++++++ src/Logic/Structural-Rules/K'-logic.agda | 26 +++++++ src/Logic/Structural-Rules/K-logic.agda | 46 +++++++++++ src/Logic/Structural-Rules/M-logic.agda | 26 +++++++ src/Logic/Structural-Rules/W-logic.agda | 51 ++++++++++++ src/Logic/Structural-Rules/WI-logic.agda | 26 +++++++ 36 files changed, 1540 insertions(+) create mode 100644 CHANGELOG/mlebar-UC.md create mode 160000 fix-whitespace create mode 100644 src/Logic/Connectives/And-Logic.agda create mode 100644 src/Logic/Connectives/Backif-Logic.agda create mode 100644 src/Logic/Connectives/Fusion-Logic.agda create mode 100644 src/Logic/Connectives/Or-Logic.agda create mode 100644 src/Logic/Connectives/Trivial-Logic.agda create mode 100644 src/Logic/Connectives/Truth-Logic.agda create mode 100644 src/Logic/Logic.agda create mode 100644 src/Logic/Logics/BCK-Logic.agda create mode 100644 src/Logic/Logics/E+-Logic.agda create mode 100644 src/Logic/Logics/Full-Conn-Logic.agda create mode 100644 src/Logic/Logics/J-Logic.agda create mode 100644 src/Logic/Logics/L-Logic.agda create mode 100644 src/Logic/Logics/LI-Logic.agda create mode 100644 src/Logic/Logics/MALL+-Logic.agda create mode 100644 src/Logic/Logics/Minimal-Logic.agda create mode 100644 src/Logic/Logics/Or-Comma-Logic.agda create mode 100644 src/Logic/Logics/P-Logic.agda create mode 100644 src/Logic/Logics/R+-Logic.agda create mode 100644 src/Logic/Logics/RM+-Logic.agda create mode 100644 src/Logic/Logics/T+-Logic.agda create mode 100644 src/Logic/Logics/TW+-Logic.agda create mode 100644 src/Logic/Punctuation/Comma-Logic.agda create mode 100644 src/Logic/Punctuation/Leftid-Logic.agda create mode 100644 src/Logic/Punctuation/Rightid-Logic.agda create mode 100644 src/Logic/Structural-Rules/B'-logic.agda create mode 100644 src/Logic/Structural-Rules/B-logic.agda create mode 100644 src/Logic/Structural-Rules/B^c-logic.agda create mode 100644 src/Logic/Structural-Rules/C-logic.agda create mode 100644 src/Logic/Structural-Rules/CI-logic.agda create mode 100644 src/Logic/Structural-Rules/K'-logic.agda create mode 100644 src/Logic/Structural-Rules/K-logic.agda create mode 100644 src/Logic/Structural-Rules/M-logic.agda create mode 100644 src/Logic/Structural-Rules/W-logic.agda create mode 100644 src/Logic/Structural-Rules/WI-logic.agda diff --git a/CHANGELOG/mlebar-UC.md b/CHANGELOG/mlebar-UC.md new file mode 100644 index 0000000000..2804d7fb2a --- /dev/null +++ b/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. diff --git a/fix-whitespace b/fix-whitespace new file mode 160000 index 0000000000..58a57e9623 --- /dev/null +++ b/fix-whitespace @@ -0,0 +1 @@ +Subproject commit 58a57e9623d707bac2ddd33d0a242f84ba93d358 diff --git a/src/Logic/Connectives/And-Logic.agda b/src/Logic/Connectives/And-Logic.agda new file mode 100644 index 0000000000..1110c77878 --- /dev/null +++ b/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 + diff --git a/src/Logic/Connectives/Backif-Logic.agda b/src/Logic/Connectives/Backif-Logic.agda new file mode 100644 index 0000000000..6b06c58ba0 --- /dev/null +++ b/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 diff --git a/src/Logic/Connectives/Fusion-Logic.agda b/src/Logic/Connectives/Fusion-Logic.agda new file mode 100644 index 0000000000..9767941e5c --- /dev/null +++ b/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 diff --git a/src/Logic/Connectives/Or-Logic.agda b/src/Logic/Connectives/Or-Logic.agda new file mode 100644 index 0000000000..bdaef554e9 --- /dev/null +++ b/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 diff --git a/src/Logic/Connectives/Trivial-Logic.agda b/src/Logic/Connectives/Trivial-Logic.agda new file mode 100644 index 0000000000..7ae06decdb --- /dev/null +++ b/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 diff --git a/src/Logic/Connectives/Truth-Logic.agda b/src/Logic/Connectives/Truth-Logic.agda new file mode 100644 index 0000000000..9dd022c03a --- /dev/null +++ b/src/Logic/Connectives/Truth-Logic.agda @@ -0,0 +1,55 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with 'truth' connective + related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Connectives.Truth-Logic where + +open import Logic.Punctuation.Leftid-Logic +open import Logic.Logic +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) + + +record Truth-Logic {Lang : Set} {Struct : Set} (S : Lang → Struct) (_⊢_ : Struct → Lang → Set) (C⟨_⟩ : Struct → Struct ) (_⨾_ : Struct → Struct → Struct) (∅ : Struct) (_⇒_ : Lang → Lang → Lang) (t : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-leftid-Logic : Leftid-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + + t-introduction : ∅ ⊢ t + + t-elimination : + ∀ {X : Struct} {A : Lang} → + X ⊢ t → C⟨ ∅ ⟩ ⊢ A → + ------------ + C⟨ X ⟩ ⊢ A + +-- Exercise 2.13 (Uniqueness of truth constant) +unique-truth : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) (t₁ t₂ : Lang) → + Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t₁ → + Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t₂ → + ----------------------------- + (S t₁) ⊢ t₂ × (S t₂) ⊢ t₁ + +unique-truth Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ ∅ t₁ t₂ x y = + ⟨ Logic.context n + (Truth-Logic.t-elimination x + (Logic.hypothesis m)) + (Truth-Logic.t-introduction y) , + Logic.context m + (Truth-Logic.t-elimination y + (Logic.hypothesis n)) + (Truth-Logic.t-introduction x) ⟩ + where + z = Truth-Logic.is-leftid-Logic x + w = Truth-Logic.is-leftid-Logic y + m = Leftid-Logic.is-logic z + n = Leftid-Logic.is-logic w diff --git a/src/Logic/Logic.agda b/src/Logic/Logic.agda new file mode 100644 index 0000000000..ac69766b2f --- /dev/null +++ b/src/Logic/Logic.agda @@ -0,0 +1,94 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Logic + some basic proofs about conditional +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logic where + +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) + +record Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + hypothesis : + ∀ {A : Lang} → + ------------------- + (S A) ⊢ A + + context : + ∀ {X X' : Struct} {A : Lang} → + (C⟨ X ⟩ ⊢ A → C⟨ X' ⟩ ⊢ A) → + X ⊢ A → + --------- + X' ⊢ A + + semicolon--context-l : + ∀ {X X' Y Y' Z : Struct} {A : Lang} → + (C⟨ X ⟩ ⊢ A → C⟨ X' ⟩ ⊢ A) → + ---------------------------------------- + (C⟨ Y ⨾ X ⟩ ⊢ A → C⟨ Y ⨾ X' ⟩ ⊢ A) + + semicolon--context-r : + ∀ {X X' Y : Struct} {A : Lang} → + (C⟨ X ⟩ ⊢ A → C⟨ X' ⟩ ⊢ A) → + ---------------------------------------- + (C⟨ X ⨾ Y ⟩ ⊢ A → C⟨ X' ⨾ Y ⟩ ⊢ A) + + if-introduction : + ∀ {X : Struct} {A B : Lang} → + (X ⨾ (S A)) ⊢ B → + ------------- + X ⊢ (A ⇒ B) + + if-elimination : + ∀ {X Y : Struct} {A B : Lang} → + X ⊢ (A ⇒ B) → + Y ⊢ A → + ------------- + (X ⨾ Y) ⊢ B + +-- proof from page 23 +chain-ifs : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → + Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → + ∀ {A B C : Lang} → + (S A) ⊢ B → + ------------------------ + (S (B ⇒ C)) ⊢ (A ⇒ C) + + +chain-ifs Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x y = Logic.if-introduction x(Logic.if-elimination x (Logic.hypothesis x) y) + +-- Lemma 2.22 (Uniqueness of conditionals) +conditional-unique : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒₁_ _⇒₂_ : Lang → Lang → Lang) → + Logic S _⊢_ C⟨_⟩ _⨾_ _⇒₁_ → + Logic S _⊢_ C⟨_⟩ _⨾_ _⇒₂_ → + ∀ {A B : Lang} → + ------------------------------------------------ + S (A ⇒₁ B) ⊢ (A ⇒₂ B) × S (A ⇒₂ B) ⊢ (A ⇒₁ B) + +conditional-unique Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒₁_ _⇒₂_ x y = + ⟨ Logic.if-introduction y + (Logic.if-elimination x + (Logic.hypothesis x) + (Logic.hypothesis x)) , + Logic.if-introduction x + (Logic.if-elimination y + (Logic.hypothesis x) + (Logic.hypothesis x)) ⟩ diff --git a/src/Logic/Logics/BCK-Logic.agda b/src/Logic/Logics/BCK-Logic.agda new file mode 100644 index 0000000000..6ad5d8b5b5 --- /dev/null +++ b/src/Logic/Logics/BCK-Logic.agda @@ -0,0 +1,28 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Affine Logic (BCK in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.BCK-Logic where + +open import Logic.Logic +open import Logic.Logics.MALL+-Logic +open import Logic.Structural-Rules.K-Logic + +record BCK-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-MALL⁺-logic : + MALL⁺-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t ⊤ ⊥ + + is-K-logic : K-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + diff --git a/src/Logic/Logics/E+-Logic.agda b/src/Logic/Logics/E+-Logic.agda new file mode 100644 index 0000000000..f92b5a9438 --- /dev/null +++ b/src/Logic/Logics/E+-Logic.agda @@ -0,0 +1,29 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Entailment Logic (DBB'lPrPuW[⇒, ∘, ∧, ∨, t] +-- in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.E+-Logic where + +open import Logic.Logic +open import Logic.Logics.T+-Logic +open import Logic.Punctuation.Rightid-Logic + +record E⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ _/_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-T⁺-logic : + T⁺-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t + + is-rPu-logic : rPu-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + diff --git a/src/Logic/Logics/Full-Conn-Logic.agda b/src/Logic/Logics/Full-Conn-Logic.agda new file mode 100644 index 0000000000..1ec3280f6b --- /dev/null +++ b/src/Logic/Logics/Full-Conn-Logic.agda @@ -0,0 +1,40 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic containing all connectives - not defined directly in +-- the book but used for easily defining other logics +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.Full-Conn-Logic where + +open import Logic.Logic +open import Logic.Connectives.And-Logic +open import Logic.Connectives.Or-Logic +open import Logic.Connectives.Backif-Logic +open import Logic.Connectives.Fusion-Logic +open import Logic.Connectives.Trivial-Logic +open import Logic.Connectives.Truth-Logic + +record Full-Conn-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-and-logic : And-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ + + is-or-logic : Or-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∨_ + + is-fusion-logic : Fusion-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘_ + + is-backif-logic : Backif-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐_ + + is-trivial-logic : Trivial-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ ⊤ ⊥ + + is-truth-logic : Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t + diff --git a/src/Logic/Logics/J-Logic.agda b/src/Logic/Logics/J-Logic.agda new file mode 100644 index 0000000000..b6458581a0 --- /dev/null +++ b/src/Logic/Logics/J-Logic.agda @@ -0,0 +1,28 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Intuitionistic Logic (BCWK in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.J-Logic where + +open import Logic.Logic +open import Logic.Logics.BCK-Logic +open import Logic.Structural-Rules.W-Logic + +record J-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-BCK-logic : + BCK-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t ⊤ ⊥ + + is-W-logic : W-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + diff --git a/src/Logic/Logics/L-Logic.agda b/src/Logic/Logics/L-Logic.agda new file mode 100644 index 0000000000..02e925ba31 --- /dev/null +++ b/src/Logic/Logics/L-Logic.agda @@ -0,0 +1,32 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Lambek Associative Calculus (BBᶜP[⇒, ⇐, ∘] in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.L-Logic where + +open import Logic.Logic +open import Logic.Structural-Rules.B-Logic +open import Logic.Structural-Rules.B^c-Logic +open import Logic.Connectives.Backif-Logic +open import Logic.Connectives.Fusion-Logic + +record L-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⟨_⟩ _⨾_ _⇒_ + + is-backif-logic : Backif-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐_ + + is-fusion-logic : Fusion-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘_ + + is-B-logic : B-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-Bᶜ-logic : Bᶜ-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ diff --git a/src/Logic/Logics/LI-Logic.agda b/src/Logic/Logics/LI-Logic.agda new file mode 100644 index 0000000000..ee71fdd1a1 --- /dev/null +++ b/src/Logic/Logics/LI-Logic.agda @@ -0,0 +1,29 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Lambek Associative Calculus with Identity (BBᶜP[⇒, ⇐, ∘, t] -- in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.LI-Logic where + +open import Logic.Logic +open import Logic.Logics.L-Logic +open import Logic.Logics.P-Logic +open import Logic.Connectives.Truth-Logic + +record LI-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∘_ : Lang → Lang → Lang) (t : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-L-logic : L-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐_ _∘_ + + is-P-logic : P-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + + is-truth-logic : Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t diff --git a/src/Logic/Logics/MALL+-Logic.agda b/src/Logic/Logics/MALL+-Logic.agda new file mode 100644 index 0000000000..b1e48e6e3f --- /dev/null +++ b/src/Logic/Logics/MALL+-Logic.agda @@ -0,0 +1,30 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Multiplicative Additive Linear Logic (BC in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.MALL+-Logic where + +open import Logic.Logic +open import Logic.Structural-Rules.B-Logic +open import Logic.Structural-Rules.C-Logic +open import Logic.Logics.Full-Conn-Logic + +record MALL⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-B-logic : B-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-C-logic : C-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-full-conn-logic : Full-Conn-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t ⊤ ⊥ + diff --git a/src/Logic/Logics/Minimal-Logic.agda b/src/Logic/Logics/Minimal-Logic.agda new file mode 100644 index 0000000000..61b6492d79 --- /dev/null +++ b/src/Logic/Logics/Minimal-Logic.agda @@ -0,0 +1,38 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Minimal Logic (BCWK[⇒, ∧, ∨] in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.Minimal-Logic where + +open import Logic.Logic +open import Logic.Structural-Rules.B-Logic +open import Logic.Structural-Rules.C-Logic +open import Logic.Structural-Rules.W-Logic +open import Logic.Structural-Rules.K-Logic +open import Logic.Connectives.And-Logic +open import Logic.Connectives.Or-Logic + +record Minimal-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⟨_⟩ _⨾_ _⇒_ + + is-and-logic : And-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ + + is-or-logic : Or-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∨_ + + is-B-logic : B-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-C-logic : C-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-W-logic : W-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-K-logic : K-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ diff --git a/src/Logic/Logics/Or-Comma-Logic.agda b/src/Logic/Logics/Or-Comma-Logic.agda new file mode 100644 index 0000000000..a3e94b62e2 --- /dev/null +++ b/src/Logic/Logics/Or-Comma-Logic.agda @@ -0,0 +1,42 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic containing both 'or' connective and 'comma' +-- punctuation mark. The setup in here is required to allow for correct use of +-- structural rules in a language containing both 'or' and 'comma' +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.Or-Comma-Logic where + +open import Logic.Logic +open import Logic.Connectives.Or-Logic +open import Logic.Punctuation.Comma-Logic +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) + +record Or-Comma-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⟨_⟩ _⨾_ _⇒_ + + is-or-logic : Or-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∨_ + + is-comma-logic : Comma-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ _⇒_ + + comma-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) + + comma-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) + diff --git a/src/Logic/Logics/P-Logic.agda b/src/Logic/Logics/P-Logic.agda new file mode 100644 index 0000000000..5e5e3cf7a7 --- /dev/null +++ b/src/Logic/Logics/P-Logic.agda @@ -0,0 +1,28 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic containing an id - not included as part of table of +-- logics in the book, but used to define other logics +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.P-Logic where + +open import Logic.Logic +open import Logic.Punctuation.Rightid-Logic +open import Logic.Punctuation.Leftid-Logic + +record P-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-rightid-logic : Rightid-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + + is-leftid-logic : Leftid-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + diff --git a/src/Logic/Logics/R+-Logic.agda b/src/Logic/Logics/R+-Logic.agda new file mode 100644 index 0000000000..2b0855f068 --- /dev/null +++ b/src/Logic/Logics/R+-Logic.agda @@ -0,0 +1,30 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Relevant Logic (DBCW in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.R+-Logic where + +open import Logic.Logic +open import Logic.Logics.Or-Comma-Logic +open import Logic.Logics.MALL+-Logic +open import Logic.Structural-Rules.W-Logic + +record R⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ _/_ : Struct → Struct → Struct)(∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-or-comma-logic : Or-Comma-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ _⇒_ _∨_ + + is-W-logic : W-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-MALL⁺-logic : MALL⁺-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t ⊤ ⊥ + diff --git a/src/Logic/Logics/RM+-Logic.agda b/src/Logic/Logics/RM+-Logic.agda new file mode 100644 index 0000000000..19c55cb0b7 --- /dev/null +++ b/src/Logic/Logics/RM+-Logic.agda @@ -0,0 +1,27 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Relevant Logic with Mingle (DBCWM in Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.RM+-Logic where + +open import Logic.Logic +open import Logic.Logics.R+-Logic +open import Logic.Structural-Rules.M-Logic + +record RM⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ _/_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t ⊤ ⊥ : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-R⁺-logic : R⁺-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t ⊤ ⊥ + + is-M-logic : M-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + diff --git a/src/Logic/Logics/T+-Logic.agda b/src/Logic/Logics/T+-Logic.agda new file mode 100644 index 0000000000..a5e4ef91f1 --- /dev/null +++ b/src/Logic/Logics/T+-Logic.agda @@ -0,0 +1,28 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Ticket Entailment (DBB'lPW[⇒, ∘, ∧, ∨, t] in +-- Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.T+-Logic where + +open import Logic.Logic +open import Logic.Logics.TW+-Logic +open import Logic.Structural-Rules.W-Logic + +record T⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ _/_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-TW⁺-logic : TW⁺-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ ∅ _⇒_ _⇐_ _∧_ _∨_ _∘_ t + + is-W-logic : W-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + diff --git a/src/Logic/Logics/TW+-Logic.agda b/src/Logic/Logics/TW+-Logic.agda new file mode 100644 index 0000000000..637d8669aa --- /dev/null +++ b/src/Logic/Logics/TW+-Logic.agda @@ -0,0 +1,44 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Definition for Positive Ticket Entailment (DBB'lP[⇒, ∘, ∧, ∨, t] in +-- Restall) +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Logics.TW+-Logic where + +open import Logic.Logic +open import Logic.Logics.Or-Comma-Logic +open import Logic.Structural-Rules.B-Logic +open import Logic.Structural-Rules.B'-Logic +open import Logic.Punctuation.Leftid-Logic +open import Logic.Connectives.Truth-Logic +open import Logic.Connectives.And-Logic +open import Logic.Connectives.Backif-Logic +open import Logic.Connectives.Fusion-Logic + +record TW⁺-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ _/_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ _⇐_ _∧_ _∨_ _∘_ : Lang → Lang → Lang) (t : Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-or-comma-logic : Or-Comma-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ _⇒_ _∨_ + + is-B-logic : B-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-B'-logic : B'-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-truth-logic : Truth-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t + + is-and-logic : And-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∧_ + + is-backif-logic : Backif-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _⇐_ + + is-fusion-logic : Fusion-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ _∘_ + diff --git a/src/Logic/Punctuation/Comma-Logic.agda b/src/Logic/Punctuation/Comma-Logic.agda new file mode 100644 index 0000000000..a7c19dc280 --- /dev/null +++ b/src/Logic/Punctuation/Comma-Logic.agda @@ -0,0 +1,56 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with 'comma' punctuation +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Punctuation.Comma-Logic where + +open import Logic.Logic + +record Comma-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⟨_⟩ _⨾_ _⇒_ + + comma-assoc : + ∀ {X Y Z : Struct} {A : Lang} → + C⟨ X / (Y / Z) ⟩ ⊢ A → + ----------------------------- + C⟨ (X / Y) / Z ⟩ ⊢ A + + comma-commute : + ∀ {X Y : Struct} {A : Lang} → + C⟨ X / Y ⟩ ⊢ A → + ----------------------------- + C⟨ Y / X ⟩ ⊢ A + + comma-contract : + ∀ {X : Struct} {A : Lang} → + C⟨ X / X ⟩ ⊢ A → + --------------- + C⟨ X ⟩ ⊢ A + + comma-weaken : + ∀ {X Y : Struct} {A : Lang} → + C⟨ X ⟩ ⊢ A → + ------------------- + C⟨ X / Y ⟩ ⊢ A + + comma-context-l : + ∀ {X X' Y : Struct} {A : Lang} → + (C⟨ X ⟩ ⊢ A → C⟨ X' ⟩ ⊢ A) → + ----------------------------------------- + (C⟨ (Y / X) ⟩ ⊢ A → C⟨ (Y / X') ⟩ ⊢ A) + + comma-context-r : + ∀ {X X' Y : Struct} {A : Lang} → + (C⟨ X ⟩ ⊢ A → C⟨ X' ⟩ ⊢ A) → + ----------------------------------------- + (C⟨ (X / Y) ⟩ ⊢ A → C⟨ (X' / Y) ⟩ ⊢ A) diff --git a/src/Logic/Punctuation/Leftid-Logic.agda b/src/Logic/Punctuation/Leftid-Logic.agda new file mode 100644 index 0000000000..dcca566f12 --- /dev/null +++ b/src/Logic/Punctuation/Leftid-Logic.agda @@ -0,0 +1,90 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with 'left ID' connective + related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Punctuation.Leftid-Logic where + +open import Logic.Logic + +record lPu-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + left-push : + ∀ {X : Struct} {A : Lang} → + C⟨ X ⟩ ⊢ A → + ----------------- + C⟨ ∅ ⨾ X ⟩ ⊢ A + +record lPo-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + left-pop : + ∀ {X : Struct} {A : Lang} → + C⟨ ∅ ⨾ X ⟩ ⊢ A → + ------------ + C⟨ X ⟩ ⊢ A + +record Leftid-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-left-push : lPu-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + + is-left-pop : lPo-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + +--Theorem 2.29 (page 31) +register-consequence-1 : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) → + lPu-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ → + ∀ {A B : Lang} → + ------------------------- + (S A) ⊢ B → ∅ ⊢ (A ⇒ B) + +register-consequence-1 Lang Struct S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ x y = + Logic.if-introduction z (Logic.context z (lPu-Logic.left-push x) y) + where + z = lPu-Logic.is-logic x + +register-consequence-2 : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) → + lPo-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ → ∀ {A B : Lang} → + --------------------------- + ∅ ⊢ (A ⇒ B) → (S A) ⊢ B + +register-consequence-2 Lang Struct S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ x y = + Logic.context z + (lPo-Logic.left-pop x) + (Logic.if-elimination z y + (Logic.hypothesis z)) + where + z = lPo-Logic.is-logic x + diff --git a/src/Logic/Punctuation/Rightid-Logic.agda b/src/Logic/Punctuation/Rightid-Logic.agda new file mode 100644 index 0000000000..10b2881ecf --- /dev/null +++ b/src/Logic/Punctuation/Rightid-Logic.agda @@ -0,0 +1,76 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with 'right id' connective + related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Punctuation.Rightid-Logic where + +open import Logic.Logic +open import Logic.Connectives.Truth-Logic + +record rPu-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + right-push : + ∀ {X : Struct} {A : Lang} → + C⟨ X ⟩ ⊢ A → + ----------------- + C⟨ X ⨾ ∅ ⟩ ⊢ A + +record rPo-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + right-pop : + ∀ {X : Struct} {A : Lang} → + C⟨ X ⨾ ∅ ⟩ ⊢ A → + --------------- + C⟨ X ⟩ ⊢ A + +record Rightid-Logic + {Lang : Set} {Struct : Set} (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct ) + (_⨾_ : Struct → Struct → Struct) (∅ : Struct) + (_⇒_ : Lang → Lang → Lang) : Set where + field + is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ + + is-right-push : rPu-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + + is-right-pop : rPo-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ + +t-reduce : + ∀ (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 → + rPo-Logic S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ → + ∀ {A B : Lang} → + ------------------ + (S (t ⇒ A)) ⊢ A + +t-reduce Lang Struct S _⊢_ C⟨_⟩ _⨾_ ∅ _⇒_ t x y = + Logic.context z + (rPo-Logic.right-pop y) + (Logic.if-elimination z + (Logic.hypothesis z) + (Truth-Logic.t-introduction x)) + where + z = rPo-Logic.is-logic y diff --git a/src/Logic/Structural-Rules/B'-logic.agda b/src/Logic/Structural-Rules/B'-logic.agda new file mode 100644 index 0000000000..d871f268c2 --- /dev/null +++ b/src/Logic/Structural-Rules/B'-logic.agda @@ -0,0 +1,26 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Twisted Associative structural rule + related +-- proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.B'-Logic where + +open import Logic.Logic + +record B'-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⟨_⟩ _⨾_ _⇒_ + + twisted-assoc : + ∀ {X Y Z : Struct} {A : Lang} → + ---------------------------------------------------- + (C⟨ (X ⨾ ( Y ⨾ Z)) ⟩ ⊢ A → C⟨ ((Y ⨾ X) ⨾ Z) ⟩ ⊢ A) diff --git a/src/Logic/Structural-Rules/B-logic.agda b/src/Logic/Structural-Rules/B-logic.agda new file mode 100644 index 0000000000..332d54d2b0 --- /dev/null +++ b/src/Logic/Structural-Rules/B-logic.agda @@ -0,0 +1,51 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Associative structural rule + related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.B-Logic where + +open import Logic.Logic + +record B-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⟨_⟩ _⨾_ _⇒_ + + assoc : + ∀ {X Y Z : Struct} {A : Lang} → + C⟨ (X ⨾ ( Y ⨾ Z)) ⟩ ⊢ A → + ------------------------- + C⟨ ((X ⨾ Y) ⨾ Z) ⟩ ⊢ A + +if-extend : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → + B-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → + ∀ {A B C : Lang} → + ------------------------------------ + (S (A ⇒ B)) ⊢ ((C ⇒ A) ⇒ (C ⇒ B)) + +--proof from page 27 +if-extend Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x = + Logic.if-introduction y + (Logic.if-introduction y + (Logic.context y + (B-Logic.assoc x) + (Logic.if-elimination y + (Logic.hypothesis y) + (Logic.if-elimination y + (Logic.hypothesis y) + (Logic.hypothesis y))))) + where + y = B-Logic.is-logic x diff --git a/src/Logic/Structural-Rules/B^c-logic.agda b/src/Logic/Structural-Rules/B^c-logic.agda new file mode 100644 index 0000000000..dc8f9dc2bf --- /dev/null +++ b/src/Logic/Structural-Rules/B^c-logic.agda @@ -0,0 +1,26 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Converse Associative structural rule +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.B^c-Logic where + +open import Logic.Logic + +record Bᶜ-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⟨_⟩ _⨾_ _⇒_ + + converse-assoc : + ∀ {X Y Z : Struct} {A : Lang} → + C⟨ ((X ⨾ Y) ⨾ Z) ⟩ ⊢ A → + ------------------------- + C⟨ (X ⨾ ( Y ⨾ Z)) ⟩ ⊢ A diff --git a/src/Logic/Structural-Rules/C-logic.agda b/src/Logic/Structural-Rules/C-logic.agda new file mode 100644 index 0000000000..8172495e35 --- /dev/null +++ b/src/Logic/Structural-Rules/C-logic.agda @@ -0,0 +1,51 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Strong Commutatitivity structural rule + +-- related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.C-Logic where + +open import Logic.Logic + +record C-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⟨_⟩ _⨾_ _⇒_ + + strong-commute : ∀ {X Y Z : Struct} {A : Lang} → + C⟨ ((X ⨾ Y) ⨾ Z) ⟩ ⊢ A → + ----------------------------- + C⟨ ((X ⨾ Z) ⨾ Y) ⟩ ⊢ A + +if-rearrange : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → + C-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → + ∀ {A B C : Lang} → + ----------------------------------- + (S (A ⇒ (B ⇒ C))) ⊢ (B ⇒ (A ⇒ C)) + +--proof from page 27 +if-rearrange Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x = + Logic.if-introduction y + (Logic.if-introduction y + ( Logic.context y + (C-Logic.strong-commute x) + (Logic.if-elimination y + (Logic.if-elimination y + (Logic.hypothesis y) + (Logic.hypothesis y)) + (Logic.hypothesis y)))) + where + y = C-Logic.is-logic x diff --git a/src/Logic/Structural-Rules/CI-logic.agda b/src/Logic/Structural-Rules/CI-logic.agda new file mode 100644 index 0000000000..7e89a57362 --- /dev/null +++ b/src/Logic/Structural-Rules/CI-logic.agda @@ -0,0 +1,49 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Weak Commutatitivity structural rule + related +-- proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.CI-Logic where + +open import Logic.Logic + +record CI-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⟨_⟩ _⨾_ _⇒_ + + weak-commute : + ∀ {X Y : Struct} {A : Lang} → + C⟨ X ⨾ Y ⟩ ⊢ A → + ----------------- + C⟨ Y ⨾ X ⟩ ⊢ A + + +modus-ponens-pullback : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → CI-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → ∀ {A B : Lang} → + ----------------------- + (S A) ⊢ ((A ⇒ B) ⇒ B) + + +-- proof from page 27 +modus-ponens-pullback Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x = + Logic.if-introduction y + (Logic.context y + (CI-Logic.weak-commute x) + (Logic.if-elimination y + (Logic.hypothesis y) + (Logic.hypothesis y))) + where + y = CI-Logic.is-logic x diff --git a/src/Logic/Structural-Rules/K'-logic.agda b/src/Logic/Structural-Rules/K'-logic.agda new file mode 100644 index 0000000000..5662c27ffc --- /dev/null +++ b/src/Logic/Structural-Rules/K'-logic.agda @@ -0,0 +1,26 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Commuted Weakening structural rule +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.K'-Logic where + +open import Logic.Logic + +record K'-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⟨_⟩ _⨾_ _⇒_ + + commute-weaken : + ∀ {X Y : Struct} {A : Lang} → + C⟨ X ⟩ ⊢ A → + --------------- + C⟨ Y ⨾ X ⟩ ⊢ A diff --git a/src/Logic/Structural-Rules/K-logic.agda b/src/Logic/Structural-Rules/K-logic.agda new file mode 100644 index 0000000000..afc55c2a92 --- /dev/null +++ b/src/Logic/Structural-Rules/K-logic.agda @@ -0,0 +1,46 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Weakening structural rule + related proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.K-Logic where + +open import Logic.Logic + +record K-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⟨_⟩ _⨾_ _⇒_ + + weaken : + ∀ {X Y : Struct} {A : Lang} → + (C⟨ X ⟩ ) ⊢ A → + ------------------ + (C⟨ X ⨾ Y ⟩) ⊢ A + +if-weaken : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → + K-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → + ∀ {A B : Lang} → + ----------------- + (S A) ⊢ (B ⇒ A) + +--proof from page 27 +if-weaken Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x = + Logic.if-introduction y + (Logic.context y + (K-Logic.weaken x) + (Logic.hypothesis y)) + where + y = K-Logic.is-logic x diff --git a/src/Logic/Structural-Rules/M-logic.agda b/src/Logic/Structural-Rules/M-logic.agda new file mode 100644 index 0000000000..07b458cd75 --- /dev/null +++ b/src/Logic/Structural-Rules/M-logic.agda @@ -0,0 +1,26 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Mingle structural rule +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.M-Logic where + +open import Logic.Logic + +record M-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⟨_⟩ _⨾_ _⇒_ + + weak-contract : + ∀ {X : Struct} {A : Lang} → + C⟨ X ⟩ ⊢ A → + ------------------ + C⟨ (X ⨾ X) ⟩ ⊢ A diff --git a/src/Logic/Structural-Rules/W-logic.agda b/src/Logic/Structural-Rules/W-logic.agda new file mode 100644 index 0000000000..ce2c3688e9 --- /dev/null +++ b/src/Logic/Structural-Rules/W-logic.agda @@ -0,0 +1,51 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Strong Contraction structural rule + related +-- proof +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.W-Logic where + +open import Logic.Logic + +record W-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⟨_⟩ _⨾_ _⇒_ + + strong-contract : + ∀ {X Y : Struct} {A : Lang} → + C⟨ ((X ⨾ Y) ⨾ Y) ⟩ ⊢ A → + ----------------- + C⟨ X ⨾ Y ⟩ ⊢ A + +double-if-contract : + ∀ (Lang : Set) (Struct : Set) (S : Lang → Struct) + (_⊢_ : Struct → Lang → Set) + (C⟨_⟩ : Struct → Struct) + (_⨾_ : Struct → Struct → Struct) + (_⇒_ : Lang → Lang → Lang) → + W-Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_ → + ∀ {A B C : Lang} → + --------------------------- + S (A ⇒ (A ⇒ B)) ⊢ (A ⇒ B) + +-- proof from page 28 +double-if-contract Lang Struct S _⊢_ C⟨_⟩ _⨾_ _⇒_ x = + Logic.if-introduction y + (Logic.context y + (W-Logic.strong-contract x) + (Logic.if-elimination y + (Logic.if-elimination y + (Logic.hypothesis y) + (Logic.hypothesis y)) + (Logic.hypothesis y))) + where + y = W-Logic.is-logic x diff --git a/src/Logic/Structural-Rules/WI-logic.agda b/src/Logic/Structural-Rules/WI-logic.agda new file mode 100644 index 0000000000..70205542f6 --- /dev/null +++ b/src/Logic/Structural-Rules/WI-logic.agda @@ -0,0 +1,26 @@ +---------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Logic with Weak Contraction structural rule +---------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +module Logic.Structural-Rules.WI-Logic where + +open import Logic.Logic + +record WI-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⟨_⟩ _⨾_ _⇒_ + + weak-contract : + ∀ {X : Struct} {A : Lang} → + C⟨ (X ⨾ X) ⟩ ⊢ A → + ------------ + C⟨ X ⟩ ⊢ A