{{ message }}

Instantly share code, notes, and snippets.

# louisswarren/.gitignore

Last active Nov 22, 2020
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 }