Skip to content

Instantly share code, notes, and snippets.

@louisswarren

louisswarren/.gitignore

Last active Nov 22, 2020
Embed
What would you like to do?
cat
*.vim
*.agdai
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
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 β))))
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)
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
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 (λ ()) (λ ())))) ]
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 ∷ ())) })) ]
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
You can’t perform that action at this time.