Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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 Xwhere
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 Xwhere
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″)
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.