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)

--------------------------------------------------------------------------------------------