Instantly share code, notes, and snippets.

louisswarren/Decidable.agda Last active Jul 27, 2019

barcher
 open import Agda.Builtin.Equality public data ⊥ : Set where ¬_ : (A : Set) → Set ¬ A = A → ⊥ infix 4 _≢_ _≢_ : {A : Set} → A → A → Set x ≢ y = ¬(x ≡ y) ⊥-elim : {A : Set} → ⊥ → A ⊥-elim () 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
 open import Decidable module Formula (X : Set) ⦃ _ : Discrete X ⦄ where open import Agda.Builtin.Nat renaming (Nat to ℕ) infixr 105 _⇒_ data Formula : Set where atom : X → Formula _⇒_ : Formula → Formula → Formula instance formulaD : Discrete Formula formulaD ⟨ atom x ≟ atom y ⟩ with x ≟ y ... | yes refl = yes refl ... | no x≢y = no λ { refl → x≢y refl } formulaD ⟨ α ⇒ β ≟ γ ⇒ δ ⟩ with α ≟ γ | β ≟ δ ... | yes refl | yes refl = yes refl ... | _ | no γ≢δ = no λ { refl → γ≢δ refl } ... | no α≢β | _ = no λ { refl → α≢β refl } formulaD ⟨ atom _ ≟ _ ⇒ _ ⟩ = no λ () formulaD ⟨ _ ⇒ _ ≟ atom _ ⟩ = no λ ()
 module List where open import Agda.Builtin.Equality open import Agda.Builtin.List public open import Decidable infixr 5 _++_ _++_ : {A : Set} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ xs ++ ys ++assoc : {A : Set} → (xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs ++assoc [] ys zs = refl ++assoc (x ∷ xs) ys zs rewrite ++assoc xs ys zs = refl infix 4 _∈_ _∉_ data _∈_ {A : Set} (x : A) : List A → Set where [] : ∀{xs} → x ∈ (x ∷ xs) _∷_ : ∀{xs} → (y : A) → x ∈ xs → x ∈ (y ∷ xs) _∉_ : {A : Set} → (x : A) → List A → Set x ∉ xs = ¬(x ∈ xs) after : {A : Set} {ys : List A} → ∀ x xs → x ∈ (xs ++ x ∷ ys) after x [] = [] after x (y ∷ xs) = y ∷ after x xs later : {A : Set} {x : A} {xs : List A} → ∀ ys → x ∈ xs → x ∈ ys ++ xs later [] x∈xs = x∈xs later (y ∷ ys) x∈xs = y ∷ later ys x∈xs is_∈_ : {A : Set} ⦃ _ : Discrete A ⦄ → (x : A) → (xs : List A) → Dec (x ∈ xs) is x ∈ [] = no λ () is x ∈ (y ∷ xs) with x ≟ y ... | yes refl = yes [] ... | no x≢y with is x ∈ xs ... | yes x∈xs = yes (y ∷ x∈xs) ... | no x∉xs = no λ { [] → x≢y refl ; (_ ∷ x∈xs) → x∉xs x∈xs } data All {A : Set} (P : Pred A) : List A → Set syntax All P xs = ∀[ xs ] P data All {A} P where [] : ∀[ [] ] P _∷_ : ∀{x xs} → P x → ∀[ xs ] P → ∀[ x ∷ xs ] P is∀[_] : {A : Set} {P : Pred A} → (xs : List A) → Decidable P → Dec (∀[ xs ] P) is∀[ [] ] p = yes [] is∀[ x ∷ xs ] p with p x ... | no ¬Px = no λ { (Px ∷ _) → ¬Px Px } ... | yes Px with is∀[ xs ] p ... | yes ∀xsP = yes (Px ∷ ∀xsP) ... | no ¬∀xsP = no λ { (_ ∷ ∀xsP) → ¬∀xsP ∀xsP }
 open import Decidable module Model (X : Set) ⦃ _ : Discrete X ⦄ where open import Agda.Builtin.Sigma open import Formula X open import List open import Tree infix 1 _⊨_ _⊨̷_ data _⊨_ (l : List X) : Formula → Set data _⊨̷_ (l : List X) : Formula → Set data _⊨_ l where atom : ∀{x} → x ∈ l → l ⊨ atom x _∣⇒_ : ∀{β} → ∀ α → l ⊨ β → l ⊨ α ⇒ β _⇒∣_ : ∀{α} → l ⊨̷ α → ∀ β → l ⊨ α ⇒ β data _⊨̷_ l where atom : ∀{x} → x ∉ l → l ⊨̷ atom x _⇒_ : ∀{α β} → l ⊨ α → l ⊨̷ β → l ⊨̷ α ⇒ β Closed⊨atom : (x : X) → Closed λ {l} t → l ⊨ atom x Closed⊨atom x t (atom x∈l) t≼t′ with Labelext t≼t′ ... | s , refl = atom (later s x∈l) does_⊨_ : (l : List X) → (α : Formula) → (l ⊨ α) ⊎ (l ⊨̷ α) does l ⊨ atom x with is x ∈ l ... | yes x∈l = inl (atom x∈l) ... | no x∉l = inr (atom x∉l) does l ⊨ (α ⇒ β) with does l ⊨ α | does l ⊨ β ... | inr ⊨̷α | _ = inl (⊨̷α ⇒∣ β) ... | _ | inl ⊨β = inl (α ∣⇒ ⊨β) ... | inl ⊨α | inr ⊨̷β = inr (⊨α ⇒ ⊨̷β) ⊨̷elim : {l : List X} {α : Formula} → l ⊨̷ α → l ⊨ α → ⊥ ⊨̷elim (atom x∉l) (atom x∈l) = x∉l x∈l ⊨̷elim (l⊨α ⇒ l⊨̷β) (α ∣⇒ l⊨β) = ⊨̷elim l⊨̷β l⊨β ⊨̷elim (l⊨α ⇒ l⊨̷β) (l⊨̷α ⇒∣ β) = ⊨̷elim l⊨̷α l⊨α fromMeta : {l : List X} {α β : Formula} → (l ⊨ α → l ⊨ β) → l ⊨ α ⇒ β fromMeta {l} {α} {β} ⊨α→⊨β with does l ⊨ α | does l ⊨ β ... | inr ⊨̷α | _ = ⊨̷α ⇒∣ β ... | _ | inl ⊨β = α ∣⇒ ⊨β ... | inl ⊨α | inr ⊨̷β = α ∣⇒ (⊨α→⊨β ⊨α) toMeta : {l : List X} {α β : Formula} → l ⊨ α ⇒ β → l ⊨ α → l ⊨ β toMeta (α ∣⇒ ⊨β) ⊨α = ⊨β toMeta (⊨̷α ⇒∣ β) ⊨α = ⊥-elim (⊨̷elim ⊨̷α ⊨α) -- WRONG DEFN --_⊩_ : {l : List X} → (t : Tree l) → Formula → Set --t ⊩ α = ∀[≽ t ] λ {m} t′ → m ⊨ α -- --⊩closed : (α : Formula) → Closed (_⊩ α) --⊩closed α = ClosedClosed λ {l} _ → l ⊨ α -- --does_⊩_ : {l : List X} → (t : Tree l) → (α : Formula) → Dec (t ⊩ α) --does_⊩_ {l} t (atom x) with does l ⊨ (atom x) --... | inl l⊨x = yes λ t≼t′ → Closed⊨atom x t l⊨x t≼t′ --... | inr l⊨̷x = no λ { ≽t→⊩x → ⊨̷elim l⊨̷x (≽t→⊩x []) } --does t ⊩ (α ⇒ β) with does t ⊩ α | does t ⊩ β --... | _ | yes ⊩β = yes λ t≼t′ → α ∣⇒ (⊩β t≼t′) --... | no ¬⊩α | _ = yes {! !} --... | yes ⊩α | no ¬⊩β = no {! !} -- -- --_⊩atom_ : {l : List X} {x : X} → (t : Tree l) → x ∈ l → t ⊩ atom x --(t ⊩atom x∈l) [] = atom x∈l --(stem ts ⊩atom x∈l) (t∈s ∷ t≼t′) = (_ ⊩atom later _ x∈l) t≼t′ -- --_⊩arrow_ : {l : List X} {x : X} {α β : Formula} → (t : Tree l) → ∀[≽ t ] (λ t′ → t ⊩ α → t ⊩ β) → t ⊩ α ⇒ β --(t ⊩arrow k) [] = {! !} -- where -- b : ? -- b = k [] {! !} {! !} --(.(stem _) ⊩arrow k) (x ∷ x₁) = {! !}
 open import Agda.Builtin.Nat renaming (Nat to ℕ) open import Decidable instance ℕD : Discrete ℕ ℕD ⟨ zero ≟ zero ⟩ = yes refl ℕD ⟨ suc x ≟ suc y ⟩ with x ≟ y ... | yes refl = yes refl ... | no x≢y = no λ { refl → x≢y refl } ℕD ⟨ zero ≟ suc _ ⟩ = no λ () ℕD ⟨ suc _ ≟ zero ⟩ = no λ () open import Formula ℕ open import List fis_∈_ : (x : Formula) → (xs : List Formula) → Dec (x ∈ xs) fis x ∈ xs = is x ∈ xs
 module Tree where open import Agda.Builtin.Equality open import Agda.Builtin.Sigma open import List hiding (All) data Tree {A : Set} (l : List A) : Set record Subtree {A : Set} (l : List A) : Set where constructor subtree inductive field ext : List A tree : Tree (ext ++ l) data Tree {A} l where leaf : Tree l stem : List (Subtree l) → Tree l Labels : {A : Set} {l : List A} → Tree l → List A Labels {A} {l} t = l TreePred : Set → Set₁ TreePred A = {l : List A} → Tree l → Set -- A proof of ≼ is a path within the tree data _≼_ {A : Set} {l : List A} : Tree l → {m : List A} → Tree m → Set where [] : ∀{t} → t ≼ t _∷_ : ∀{ts s t m} {t′ : Tree m} → (subtree s t) ∈ ts → t ≼ t′ → (stem ts) ≼ t′ ≼trans : {A : Set} {l m n : List A} {t : Tree l} {t′ : Tree m} {t″ : Tree n} → t ≼ t′ → t′ ≼ t″ → t ≼ t″ ≼trans [] t′≼t″ = t′≼t″ ≼trans (t∈ts ∷ t≼t′) t′≼t″ = t∈ts ∷ ≼trans t≼t′ t′≼t″ Labelext : {A : Set} {l m : List A} {t : Tree l} {t′ : Tree m} → t ≼ t′ → Σ _ λ s → m ≡ s ++ l Labelext [] = [] , refl Labelext (t∈ts ∷ t≼t′) with Labelext t≼t′ Labelext (_∷_ {s = s} _ _) | s′ , refl = s′ ++ s , ++assoc s′ s _ ∀[≽_]_ : {A : Set} {l : List A} → Tree l → TreePred A → Set ∀[≽ t ] P = ∀{m} {t′ : Tree m} → t ≼ t′ → P t′ Closed : {A : Set} → TreePred A → Set Closed P = ∀{l} → (t : Tree l) → P t → ∀[≽ t ] P -- A tree predicate defined by generalising another tree predicate over the -- entire tree is closed ClosedClosed : {A : Set} → (P : TreePred A) → Closed (∀[≽_] P) ClosedClosed P t ∀[≽t]P t≼t′ t′≼t″ = ∀[≽t]P (≼trans t≼t′ t′≼t″)