module Atoms where {- This file defines Atoms and develops some basic lemmas about Atoms. -} open import Basics ------------------------------------------------------------------------------------------------------------------ --Definition of Atom ----------------------------------------------------------------------------------------------------------------- data Atom : Set where root : Atom next : Atom → Atom --------------------------------------------------------------------------------------------------------------- --= and ≠ are injective wrt next --------------------------------------------------------------------------------------------------------------- nextInj : (a b : Atom) → (next a ≡ next b) → a ≡ b nextInj a .a refl = refl a≠b⇒na≠nb : {a b : Atom} → (a ≡ b → ⊥) → ((next a ≡ next b) → ⊥) a≠b⇒na≠nb {a}{b} a≡b⊥ na≡nb = a≡b⊥ (nextInj a b na≡nb) ---------------------------------------------------------------------------------------------------------------- --Decidable equality of atoms ---------------------------------------------------------------------------------------------------------------- AtEqDec : (a b : Atom) → Dec(a ≡ b) AtEqDec root root = yes refl AtEqDec root (next b) = no (λ ()) AtEqDec (next a) root = no (λ ()) AtEqDec (next a) (next b) with AtEqDec a b AtEqDec (next a) (next .a) | yes refl = yes refl AtEqDec (next a) (next b) | no x = no (λ p → x (nextInj a b p)) --------------------------------------------------------------------------------------------------------------- --Swapping operation on atoms --------------------------------------------------------------------------------------------------------------- swap : Atom × Atom → Atom → Atom swap (a , b) c with AtEqDec c a | AtEqDec c b swap (a , b) .a | yes refl | _ = b swap (a , b) .b | no _ | yes refl = a swap (a , b) c | no _ | no _ = c swapaba≡b : (a b : Atom) → swap (a , b) a ≡ b swapaba≡b a b with AtEqDec a a swapaba≡b a b | yes refl = refl swapaba≡b a b | no x with x refl swapaba≡b a b | no _ | () swapabb≡a : (a b : Atom) → swap (a , b) b ≡ a swapabb≡a a b with AtEqDec b a swapabb≡a b .b | yes refl = refl swapabb≡a a b | no _ with AtEqDec b b swapabb≡a a b | no _ | yes refl = refl swapabb≡a a b | no _ | no x with x refl swapabb≡a a b | no _ | no _ | () swapabc≡c : (a b c : Atom) (f : c ≡ a → ⊥) (g : c ≡ b → ⊥) → swap (a , b) c ≡ c swapabc≡c a b c f g with AtEqDec c a swapabc≡c a b .a f g | yes refl with f refl swapabc≡c a b .a f g | yes refl | () swapabc≡c a b c f g | no _ with AtEqDec c b swapabc≡c a c .c f g | no _ | yes refl with g refl swapabc≡c a c .c f g | no _ | yes refl | () swapabc≡c a b c f g | no _ | no x = refl -------------------------------------------------------------------------------------------------------------- --Swapping is idempotent ------------------------------------------------------------------------------------------------------------- swap∘swap≡swap : (a b c : Atom) → swap (a , b) (swap (a , b) c) ≡ c swap∘swap≡swap a b c with AtEqDec c a swap∘swap≡swap a b .a | yes refl = swapabb≡a a b swap∘swap≡swap a b c | no _ with AtEqDec c b swap∘swap≡swap a c .c | no _ | yes refl = swapaba≡b a c swap∘swap≡swap a b c | no f | no g = swapabc≡c a b c f g ------------------------------------------------------------------------------------------------------------ --Support of an atom ----------------------------------------------------------------------------------------------------------- supp : Atom → List Atom supp a = [ a ] ----------------------------------------------------------------------------------------------------------- --Finding an atom that is not in a list of atoms ---------------------------------------------------------------------------------------------------------- ------------------------------------------------------------------------------------------------------ --Meaning of _∉_ ------------------------------------------------------------------------------------------------------ data _∉_ (a : Atom) : List Atom → Set where a∉[] : a ∉ [] a∉as : ∀ {b as} → a ∉ as → ( b ≠ a ) → a ∉ (b :: as) ---------------------------------------------------------------------------------------------------- --an ordering relation on atoms ---------------------------------------------------------------------------------------------------- data _<'_ : Atom → Atom → Set where r<n : ∀ {a} → root <' next a n₁<n₂ : ∀ {a b} → a <' b → next a <' next b ---------------------------------------------------------------------------------------------------- --order extended to lists of atoms --------------------------------------------------------------------------------------------------- data _<_ : List Atom → Atom → Set where []< : ∀ {a} → [] < a as< : ∀ {a b as} → as < b → a <' b → (a :: as) < b --------------------------------------------------------------------------------------------------- --The greater of two atoms -------------------------------------------------------------------------------------------------- greater : Atom → Atom → Atom greater root root = next (root) greater (next a) root = next (next a) greater root (next a) = next (next a) greater (next a) (next b) = next(greater a b) ----------------------------------------------------------------------------------------------- --Outside a list of atoms ---------------------------------------------------------------------------------------------- outside : List Atom → Atom outside [] = root outside (a :: as) = greater a (outside as) ---------------------------------------------------------------------------------------- --Proving that outside is truly outside --------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------- --Next is greater than previous ---------------------------------------------------------------------------------------- b<nb : (b : Atom) → b <' next b b<nb root = r<n b<nb (next b) = n₁<n₂ (b<nb b) ------------------------------------------------------------------------------------------ --Greater is greater than both ----------------------------------------------------------------------------------------- a>bc⇒a>b : (b c : Atom) → b <' greater b c a>bc⇒a>b root root = r<n a>bc⇒a>b root (next c) = r<n a>bc⇒a>b (next b) root = b<nb (next b) a>bc⇒a>b (next b) (next c) = n₁<n₂ (a>bc⇒a>b b c) a>bc⇒a>c : (b c : Atom) → c <' greater b c a>bc⇒a>c root root = r<n a>bc⇒a>c root (next c) = b<nb (next c) a>bc⇒a>c (next b) root = r<n a>bc⇒a>c (next b) (next c) = n₁<n₂ (a>bc⇒a>c b c) --------------------------------------------------------------------------------------------- --Greater than is transitive -------------------------------------------------------------------------------------------- a<'b<'c : (a b c : Atom) → a <' b → b <' c → a <' c a<'b<'c _ _ root a<'b = \ () a<'b<'c _ root (next _) = λ () a<'b<'c root (next b) (next c) _ _ = r<n a<'b<'c (next a) (next b) (next c) (n₁<n₂ a<'b) (n₁<n₂ b<'c) = n₁<n₂ (a<'b<'c a b c a<'b b<'c) ---------------------------------------------------------------------------------------------- --Greater than a list of atoms --------------------------------------------------------------------------------------------- as<a<'b : (a b : Atom) → (as : List Atom) → as < a → a <' b → as < b as<a<'b a b [] as<a a<'b = []< as<a<'b a b (x :: xs) (as< xs<a x<'a) a<'b = as< (as<a<'b a b xs xs<a a<'b) (a<'b<'c x a b x<'a a<'b) ---------------------------------------------------------------------------------------------- --Outside is greater than --------------------------------------------------------------------------------------------- outside< : (xs : List Atom) → xs < (outside xs) outside< [] = []< outside< (a :: as) = as< (as<a<'b (outside as) (greater a (outside as)) as (outside< as) (a>bc⇒a>c a (outside as))) (a>bc⇒a>b a (outside as)) ---------------------------------------------------------------------------------------------- --Greater than is not equal to --------------------------------------------------------------------------------------------- <≠ : {a b : Atom} → a <' b → a ≡ b → ⊥ <≠ r<n = λ () <≠ (n₁<n₂ a<'b) = a≠b⇒na≠nb (<≠ a<'b) ------------------------------------------------------------------------------------------ --Greater than does not belong to ----------------------------------------------------------------------------------------- <∉ : ∀ {a as} → as < a → a ∉ as <∉ []< = a∉[] <∉ (as< as<b a<'b) = a∉as (<∉ as<b) (<≠ a<'b) -------------------------------------------------------------------------------------------- --Hence outside is not equal to -------------------------------------------------------------------------------------------- outside∉ : (xs : List Atom) → (outside xs) ∉ xs outside∉ xs = <∉ (outside< xs) --------------------------------------------------------------------------------------------