Skip to content

Instantly share code, notes, and snippets.

@louisswarren

louisswarren/.gitignore

Last active November 22, 2020 05:53
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save louisswarren/16a599cbeae3983d4fe1e0d62c965cb3 to your computer and use it in GitHub Desktop.
Save louisswarren/16a599cbeae3983d4fe1e0d62c965cb3 to your computer and use it in GitHub Desktop.
Download ZIP
cat
Raw
.gitignore
*.vim
*.agdai
Raw
Decidable.agda
open import Agda.Builtin.Equality public
data ⊥ : Set where
¬_ : Set → Set
¬ A = A → ⊥
_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
Pred : Set → Set₁
Pred A = A → Set
Decidable : {A : Set} → Pred A → Set
Decidable P = ∀ x → Dec (P x)
record Discrete (A : Set) : Set where
constructor discrete
field
_⟨_≟_⟩ : (x y : A) → Dec (x ≡ y)
open Discrete public
_≟_ : {A : Set} → ⦃ Discrete A ⦄ → (x y : A) → Dec (x ≡ y)
_≟_ ⦃ d ⦄ x y = d ⟨ x ≟ y ⟩
data _⊎_ (A B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
Raw
Deduction.agda
module Deduction where
open import Ensemble
open import Formula
infix 1 _⊢_ ⊢_
data _⊢_ {A : Set} : Ensemble (Formula A) → Formula A → Set₁ where
close : ∀{Γ Δ α} → ⌊ Δ ⌋ → Γ ⊂ Δ → Γ ⊢ α → Δ ⊢ α
assume : (α : Formula A)
→ ⟨ α ⟩ ⊢ α
intro : ∀{Γ β} → (α : Formula A)
→ Γ ⊢ β
--------------- ⇒⁺
→ Γ - α ⊢ α ⇒ β
elim : ∀{Γ₁ Γ₂ α β}
→ Γ₁ ⊢ α ⇒ β → Γ₂ ⊢ α
--------------------------- ⇒⁻
→ Γ₁ ∪ Γ₂ ⊢ β
⊢_ : {A : Set} → Formula A → Set₁
⊢ α = ∅ ⊢ α
ground-context : {A : Set} {Γ : Ensemble (Formula A)} {α : Formula A}
→ Γ ⊢ α → ⌊ Γ ⌋
ground-context (close ⌊Δ⌋ Γ⊂Δ Γ⊢α) = ⌊Δ⌋
ground-context (assume α ) = ∣⟨ α ⟩∣
ground-context (intro α Γ⊢β ) = ground-context Γ⊢β ∣-∣ α
ground-context (elim Γ₁⊢α⇒β Γ₂⊢α ) = ground-context Γ₁⊢α⇒β ∣∪∣ ground-context Γ₂⊢α
private
pf : {A : Set} → (α β γ : Formula A) → ⟨ α ⇒ β ⇒ γ ⟩ ⊢ β ⇒ α ⇒ γ
pf α β γ = close
∣⟨ α ⇒ β ⇒ γ ⟩∣
(λ x z z₁ → z (λ z₂ z₃ → z₃ (λ z₄ z₅ → z₅ (λ z₆ → z₆ z₁ z₄) z₂)))
(intro β
(intro α
(elim
(elim
(assume (α ⇒ β ⇒ γ))
(assume α))
(assume β))))
Raw
Ensemble.agda
module Ensemble where
open import Agda.Primitive
open import Decidable
open import List using (List ; [] ; _∷_)
Ensemble : ∀{a} → Set a → Set (lsuc a)
Ensemble {a} A = A → Set a
infix 4 _∈_ _∉_
_∈_ : {A : Set} → A → Ensemble A → Set
α ∈ αs = αs α
_∉_ : {A : Set} → A → Ensemble A → Set
α ∉ αs = ¬(α ∈ αs)
infix 4 _⊂_
_⊂_ : {A : Set} → Ensemble A → Ensemble A → Set
αs ⊂ βs = ∀ x → x ∈ αs → ¬(x ∉ βs)
∅ : {A : Set} → Ensemble A
∅ = λ _ → ⊥
⟨_⟩ : {A : Set} → A → Ensemble A
⟨ α ⟩ = λ x → x ≡ α
infixr 5 _∪_
_∪_ : {A : Set} → Ensemble A → Ensemble A → Ensemble A
(αs ∪ βs) = λ x → x ∉ αs → ¬(x ∉ βs)
infixl 5 _-_
_-_ : {A : Set} → Ensemble A → A → Ensemble A
(αs - α) = λ x → ¬(x ≢ α → x ∉ αs)
data ⌊_⌋ {A : Set} : Pred A → Set₁ where
∣∅∣ : ⌊ ∅ ⌋
∣⟨_⟩∣ : (α : A) → ⌊ (⟨ α ⟩) ⌋
_∣∪∣_ : ∀{αs βs} → ⌊ αs ⌋ → ⌊ βs ⌋ → ⌊ αs ∪ βs ⌋
_∣-∣_ : ∀{αs} → ⌊ αs ⌋ → (α : A) → ⌊ αs - α ⌋
infixr 5 _∣∪∣_
infixl 5 _∣-∣_
_∈_⁇ : {A : Set} → ⦃ Discrete A ⦄ → ∀{αs} → (x : A) → ⌊ αs ⌋ → Dec (x ∈ αs)
x ∈ ∣∅∣ ⁇ = no (λ x∈∅ → x∈∅)
x ∈ ∣⟨ α ⟩∣ ⁇ = x ≟ α
x ∈ As ∣∪∣ Bs ⁇ with x ∈ As ⁇
... | yes x∈αs = yes λ x∉αs _ → x∉αs x∈αs
... | no x∉αs with x ∈ Bs ⁇
... | yes x∈βs = yes λ _ x∉βs → x∉βs x∈βs
... | no x∉βs = no λ x∉αs∪βs → x∉αs∪βs x∉αs x∉βs
x ∈ As ∣-∣ α ⁇ with x ≟ α
... | yes refl = no λ α∈αs-α → α∈αs-α λ α≢α _ → α≢α refl
... | no x≢α with x ∈ As ⁇
... | yes x∈αs = yes λ x≢α→x∉αs → x≢α→x∉αs x≢α x∈αs
... | no x∉αs = no λ x∈αs-α
→ x∈αs-α (λ _ _ → x∈αs-α (λ _ _ → x∈αs-α (λ _ → x∉αs)))
syntax AllSans P xs αs = ∀[ αs ∖ xs ] P
data AllSans {A : Set} (P : Pred A) (xs : List A) : Ensemble A → Set₁ where
∣∅∣ : ∀[ ∅ ∖ xs ] P
∣⟨_⟩∣ : ∀{α} → P α → ∀[ ⟨ α ⟩ ∖ xs ] P
∣⟨∋̷_⟩∣ : ∀{α} → α List.∈ xs → ∀[ ⟨ α ⟩ ∖ xs ] P
_∣∪∣_ : ∀{αs βs} → ∀[ αs ∖ xs ] P → ∀[ βs ∖ xs ] P → ∀[ αs ∪ βs ∖ xs ] P
∣∷-∣ : ∀{αs x} → ∀[ αs ∖ x ∷ xs ] P → ∀[ αs - x ∖ xs ] P
syntax All P αs = ∀[ αs ] P
All : {A : Set} → Pred A → Ensemble A → Set₁
∀[ αs ] P = ∀[ αs ∖ [] ] P
weakAll : {A : Set} {P : Pred A} {αs : Ensemble A} → ⦃ Discrete A ⦄
→ ⌊ αs ⌋ → (∀ x → x ∈ αs → P x) → ∀[ αs ] P
weakAll {A} {P} As ∀αsP = φ As λ x x∈αs _ → ∀αsP x x∈αs
where
φ : ∀{xs αs} → ⌊ αs ⌋ → (∀ x → x ∈ αs → x List.∉ xs → P x) → ∀[ αs ∖ xs ] P
φ ∣∅∣ ∀∅∖xsP = ∣∅∣
φ {xs} ∣⟨ α ⟩∣ ∀α∖xsP with α List.∈ xs ⁇
... | yes α∈xs = ∣⟨∋̷ α∈xs ⟩∣
... | no α∉xs = ∣⟨ ∀α∖xsP α refl α∉xs ⟩∣
φ (As ∣∪∣ Bs) ∀αs∪βs∖xsP = φ As ∀αs∖xsP ∣∪∣ φ Bs ∀βs∖xsP
where
∀αs∖xsP : _
∀αs∖xsP = λ x x∈αs → ∀αs∪βs∖xsP x λ x∉αs _ → x∉αs x∈αs
∀βs∖xsP : _
∀βs∖xsP = λ x x∈βs → ∀αs∪βs∖xsP x λ _ x∉βs → x∉βs x∈βs
φ (As ∣-∣ α) ∀αs-α∖xsP = ∣∷-∣ (φ As ∀αs∖α∷xsP)
where
∀αs∖α∷xsP : _
∀αs∖α∷xsP x x∈αs x∉α∷xs = ∀αs-α∖xsP x x∈αs-α x∉xs
where
x∈αs-α = λ x≢α→x∉αs → x≢α→x∉αs (λ x≡α → x∉α∷xs List.[ x≡α ]) x∈αs
x∉xs = λ x∈xs → x∉α∷xs (α ∷ x∈xs)
Raw
Formula.agda
module Formula where
open import Decidable
data Formula (A : Set) : Set where
• : A → Formula A
_⇒_ : Formula A → Formula A → Formula A
infixr 105 _⇒_
instance DiscreteFormula : {A : Set} → ⦃ Discrete A ⦄ → Discrete (Formula A)
DiscreteFormula ⟨ • x ≟ • y ⟩ with x ≟ y
... | yes refl = yes refl
... | no x≢y = no λ { refl → x≢y refl }
DiscreteFormula ⟨ • _ ≟ _ ⇒ _ ⟩ = no λ ()
DiscreteFormula ⟨ _ ⇒ _ ≟ • _ ⟩ = no λ ()
DiscreteFormula ⟨ α₁ ⇒ β₁ ≟ α₂ ⇒ β₂ ⟩
with α₁ ≟ α₂
... | no α₁≢α₂ = no λ { refl → α₁≢α₂ refl }
... | yes refl with β₁ ≟ β₂
... | no β₁≢β₂ = no λ { refl → β₁≢β₂ refl }
... | yes refl = yes refl
Raw
Kripke.agda
module Kripke where
open import Decidable
open import Ensemble
open import Formula
open import List hiding (_∈_ ; _∉_ ; _∈_⁇)
record Tree {A : Set} (Γ : Ensemble A) : Set₁
record Subtree {A : Set} (Γ : Ensemble A) : Set₁ where
constructor subtree
inductive
field
Δ : Ensemble A
Γ⊂Δ : Γ ⊂ Δ
t : Tree Δ
record Tree Γ where
constructor tree
inductive
field
branches : List (Subtree Γ)
open Tree public
pattern leaf = tree []
infix 1 _⊨_ _⊨̷_ _⊩_ _⊩̷_
data _⊨_ {A : Set} {Γ : Ensemble A} (t : Tree Γ) : Formula A → Set
data _⊨̷_ {A : Set} {Γ : Ensemble A} (t : Tree Γ) : Formula A → Set
data _⊨_ {A} {Γ} t where
• : ∀{x} → x ∈ Γ → t ⊨ • x
∣⇒ : ∀{α β} → t ⊨̷ α → t ⊨ α ⇒ β
⇒| : ∀{α β} → t ⊨ β → t ⊨ α ⇒ β
data _⊨̷_ {A} {Γ} t where
•̷ : ∀{x} → x ∉ Γ → t ⊨̷ • x
⇒̷ : ∀{α β} → t ⊨ α → t ⊨̷ β → t ⊨̷ α ⇒ β
_⊨_⁇ : {A : Set} {Γ : Ensemble A} {⌊Γ⌋ : ⌊ Γ ⌋} → ⦃ Discrete A ⦄ → (t : Tree Γ) → (α : Formula A) → (t ⊨ α) ⊎ (t ⊨̷ α)
_⊨_⁇ {A} {Γ} {⌊Γ⌋} t (• x) with x ∈ ⌊Γ⌋ ⁇
... | yes x∈Γ = inl (• x∈Γ)
... | no x∉Γ = inr (•̷ x∉Γ)
_⊨_⁇ {A} {Γ} {k} t (α ⇒ β) with _⊨_⁇ {_} {_} {k} t α
... | inr t⊨̷α = inl (∣⇒ t⊨̷α)
... | inl t⊨α with _⊨_⁇ {_} {_} {k} t β
... | inl t⊨β = inl (⇒| t⊨β)
... | inr t⊨̷β = inr (⇒̷ t⊨α t⊨̷β)
data _⊩_ {A : Set} {Γ : Ensemble A} (t : Tree Γ) (α : Formula A) : Set₁ where
tree : t ⊨ α → List.∀[ branches t ] (λ t′ → Subtree.t t′ ⊩ α) → t ⊩ α
data _⊩̷_ {A : Set} {Γ : Ensemble A} (t : Tree Γ) (α : Formula A) : Set₁ where
here : t ⊨̷ α → t ⊩̷ α
later : List.∃[ branches t ] (λ t′ → Subtree.t t′ ⊩̷ α) → t ⊩̷ α
-- Let's try this out
open import Agda.Builtin.Nat renaming (Nat to ℕ)
kk : Tree ⟨ 0 ⟩
kk = tree
( subtree (⟨ 0 ⟩ ∪ ⟨ 1 ⟩) (λ x z z₁ → z₁ (λ z₂ _ → z₂ z)) leaf
∷ subtree (⟨ 0 ⟩ ∪ ⟨ 2 ⟩) (λ x z z₁ → z₁ (λ z₂ _ → z₂ z)) leaf
∷ [])
kk⊩0 : kk ⊩ • 0
kk⊩0 = tree (• refl) (tree (• (λ x x₁ → x refl)) [] ∷ tree (• (λ x x₁ → x refl)) [] ∷ [])
kk⊩̷1 : kk ⊩̷ • 1
kk⊩̷1 = here (•̷ (λ ()))
kk⊩1⇒0 : kk ⊩ • 1 ⇒ • 0
kk⊩1⇒0 = tree (∣⇒ (•̷ (λ ()))) (tree (⇒| (• (λ x x₁ → x refl))) [] ∷ tree (∣⇒ (•̷ (λ z → z (λ ()) (λ ())))) [] ∷ [])
kk⊩̷1⇒2 : kk ⊩̷ • 1 ⇒ • 2
kk⊩̷1⇒2 = later [ here (⇒̷ (• (λ x x₁ → x₁ refl)) (•̷ (λ z → z (λ ()) (λ ())))) ]
Raw
KripkeList.agda
module KripkeList where
open import Decidable
open import Formula
open import List
data Tree {A : Set} : List A → Set₁
record Subtree {A : Set} (Γ : List A) : Set₁ where
constructor subtree
inductive
field
Δ : List A
branches : Tree (Δ ++ Γ)
open Subtree using (branches) public
data Tree where
tree : ∀ Γ → List (Subtree Γ) → Tree Γ
subtrees : {A : Set} {Γ : List A} → Tree Γ → List (Subtree Γ)
subtrees (tree Γ ts) = ts
leaf : {A : Set} {Γ : List A} → Tree Γ
leaf {A} {Γ} = tree Γ []
infix 1 _⊨_ _⊨̷_ _⊩_ _⊩̷_
data _⊨_ {A : Set} {Γ : List A} (t : Tree Γ) : Formula A → Set
data _⊨̷_ {A : Set} {Γ : List A} (t : Tree Γ) : Formula A → Set
data _⊨_ {A} {Γ} t where
• : ∀{x} → x ∈ Γ → t ⊨ • x
∣⇒ : ∀{α β} → t ⊨̷ α → t ⊨ α ⇒ β
⇒| : ∀{α β} → t ⊨ β → t ⊨ α ⇒ β
data _⊨̷_ {A} {Γ} t where
•̷ : ∀{x} → x ∉ Γ → t ⊨̷ • x
⇒̷ : ∀{α β} → t ⊨ α → t ⊨̷ β → t ⊨̷ α ⇒ β
_⊨_⁇ : {A : Set} {Γ : List A} → ⦃ Discrete A ⦄ → (t : Tree Γ) → (α : Formula A) → (t ⊨ α) ⊎ (t ⊨̷ α)
_⊨_⁇ {A} {Γ} t (• x) with x ∈ Γ ⁇
... | yes x∈Γ = inl (• x∈Γ)
... | no x∉Γ = inr (•̷ x∉Γ)
t ⊨ α ⇒ β ⁇ with t ⊨ α ⁇
... | inr t⊨̷α = inl (∣⇒ t⊨̷α)
... | inl t⊨α with t ⊨ β ⁇
... | inl t⊨β = inl (⇒| t⊨β)
... | inr t⊨̷β = inr (⇒̷ t⊨α t⊨̷β)
data _⊩_ {A : Set} {Γ : List A} (t : Tree Γ) (α : Formula A) : Set₁ where
tree : t ⊨ α → List.∀[ subtrees t ] (λ t′ → branches t′ ⊩ α) → t ⊩ α
data _⊩̷_ {A : Set} {Γ : List A} (t : Tree Γ) (α : Formula A) : Set₁ where
here : t ⊨̷ α → t ⊩̷ α
later : List.∃[ subtrees t ] (λ t′ → branches t′ ⊩̷ α) → t ⊩̷ α
-- Let's try this out
open import Agda.Builtin.Nat renaming (Nat to ℕ)
kk : Tree (0 ∷ [])
kk = tree (0 ∷ []) (subtree (1 ∷ []) leaf ∷ (subtree (2 ∷ []) leaf ∷ []))
kk⊩0 : kk ⊩ • 0
kk⊩0 = tree (• [ refl ]) (tree (• (1 ∷ [ refl ])) [] ∷ (tree (• (2 ∷ [ refl ])) [] ∷ []))
kk⊩̷1 : kk ⊩̷ • 1
kk⊩̷1 = here (•̷ λ { [ () ] ; (.0 ∷ ()) })
kk⊩1⇒0 : kk ⊩ • 1 ⇒ • 0
kk⊩1⇒0 = tree (∣⇒ (•̷ λ { [ () ] ; (.0 ∷ ()) })) (tree (⇒| (• (1 ∷ [ refl ]))) [] ∷ tree (∣⇒ (•̷ λ { (.2 ∷ [ () ]) ; (.2 ∷ (.0 ∷ ())) })) [] ∷ [])
kk⊩̷1⇒2 : kk ⊩̷ • 1 ⇒ • 2
kk⊩̷1⇒2 = later [ here (⇒̷ (• [ refl ]) (•̷ λ { (.1 ∷ [ () ]) ; (.1 ∷ (.0 ∷ ())) })) ]
Raw
List.agda
module List where
open import Agda.Builtin.List public
open import Decidable
instance DiscreteList : {A : Set} → ⦃ Discrete A ⦄ → Discrete (List A)
DiscreteList ⟨ [] ≟ [] ⟩ = yes refl
DiscreteList ⟨ [] ≟ _ ∷ _ ⟩ = no λ ()
DiscreteList ⟨ _ ∷ _ ≟ [] ⟩ = no λ ()
DiscreteList ⟨ x ∷ xs ≟ y ∷ ys ⟩ with x ≟ y
... | no x≢y = no λ { refl → x≢y refl }
... | yes refl with xs ≟ ys
... | yes refl = yes refl
... | no xs≢ys = no λ { refl
→ xs≢ys refl }
syntax All P xs = ∀[ xs ] P
data All {a b} {A : Set a} (P : A → Set b) : List A → Set b where
[] : ∀[ [] ] P
_∷_ : ∀{x xs} → P x → ∀[ xs ] P → ∀[ x ∷ xs ] P
∀[_]_⁇ : {A : Set} {P : A → Set} → ∀ xs → Decidable P → Dec (All P xs)
∀[ [] ] p ⁇ = yes []
∀[ x ∷ xs ] p ⁇ with p x
... | no ¬Px = no λ { (Px ∷ _) → ¬Px Px }
... | yes Px with ∀[ xs ] p ⁇
... | yes ∀xsP = yes (Px ∷ ∀xsP)
... | no ¬∀xsP = no λ { (_ ∷ ∀xsP) → ¬∀xsP ∀xsP }
syntax Any P xs = ∃[ xs ] P
data Any {a b} {A : Set a} (P : A → Set b) : List A → Set b where
[_] : ∀{x xs} → P x → ∃[ x ∷ xs ] P
_∷_ : ∀{xs} → ∀ x → ∃[ xs ] P → ∃[ x ∷ xs ] P
∃[_]_⁇ : {A : Set} {P : A → Set} → ∀ xs → Decidable P → Dec (Any P xs)
∃[ [] ] p ⁇ = no λ ()
∃[ x ∷ xs ] p ⁇ with p x
... | yes Px = yes [ Px ]
... | no ¬Px with ∃[ xs ] p ⁇
... | yes ∃xsP = yes (x ∷ ∃xsP)
... | no ¬∃xsP = no λ { [ Px ] → ¬Px Px
; (.x ∷ ∃xsP) → ¬∃xsP ∃xsP }
infix 4 _∈_ _∉_
_∈_ : {A : Set} → (x : A) → (xs : List A) → Set
x ∈ xs = ∃[ xs ] (x ≡_)
_∉_ : {A : Set} → (x : A) → (xs : List A) → Set
x ∉ xs = ¬(x ∈ xs)
_∈_⁇ : {A : Set} → ⦃ Discrete A ⦄ → (x : A) → (xs : List A) → Dec (x ∈ xs)
x ∈ [] ⁇ = no λ ()
x ∈ y ∷ xs ⁇ with x ≟ y
... | yes refl = yes [ refl ]
... | no x≢y with x ∈ xs ⁇
... | yes x∈xs = yes (y ∷ x∈xs)
... | no x∉xs = no λ { [ x≡y ] → x≢y x≡y
; (.y ∷ x∈xs) → x∉xs x∈xs }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment