{-
GRAPH CLOSURES

This module contains standard definitions and lemmas for working with
(not necessarily proof-irrelevant) binary relations, such as the
inductive definition of the symmetric closure.
-}

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Cubical.Data.List renaming (rev to listrev)
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order.Recursive


{- Note: The following module from the cubical library defines its own
   relations (which forces us to use them). Thus, we cannot use the
   relations from Relation.Binary, where some of the definitions and
   lemmas below are already implemented. -}

open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc;
            Rel to BinRel)

open import Cubical.Data.List.Base hiding (rev)
open import Cubical.Data.List.Properties

module squier.graphclosures where

-- Variables for universe levels, not important
private variable
  ℓ₀ ℓ₁ ℓ₂ : Level
  A : Type ℓ₀
  R : BinRel A ℓ₁

-- The symmetric closure as an inductive type
data SymClosure {A : Type ℓ₀} (R : BinRel A ℓ₁) : BinRel A (ℓ-max ℓ₀ ℓ₁) where
  inj  : {a b : A} → (R a b) → SymClosure R a b
  rev : {a b : A} → (R a b) → SymClosure R b a

{- Note: Below, we use cons-lists instead of snoc-lists in order to be
   compatible with the library. -}

infixr  _∷ᵗ_
-- The reflexive-transitive closure
data TransReflClosure {A : Type ℓ₀} (R : BinRel A ℓ₁) : BinRel A (ℓ-max ℓ₀ ℓ₁) where
  []ᵗ : {a : A} → TransReflClosure R a a
  _∷ᵗ_ : {a b c : A} → R a b → TransReflClosure R b c → TransReflClosure R a c

-- module _ {A : Type ℓ₀} {R : BinRel A ℓ₁} where

-- elimination principle of the reflexive-transitive closure
elim-transRefl :
  (B : {a b : A} (ab : TransReflClosure R a b) → Type ℓ₂) →
  (e : {a : A} → B {a} []ᵗ) →
  (c : {a b c : A} (ab : R a b) (bc : TransReflClosure R b c) → B bc → B (ab ∷ᵗ bc)) →
  {a b : A} → (ab : TransReflClosure R a b) → B ab
elim-transRefl B e c []ᵗ = e
elim-transRefl B e c (s ∷ᵗ ab) = c s ab (elim-transRefl B e c ab)

-- equal elements are related by the reflexivity[-transitive] closure
≡→[] : ∀ {R : BinRel A ℓ₁} {a b : A} → a ≡ b → TransReflClosure R a b
≡→[] {R = R} {a = a} {b = b} a≡b = subst (λ a' → TransReflClosure R a a') a≡b []ᵗ

infixr  _++ᵗ_

-- concatenation of closure-sequences
_++ᵗ_ : ∀ {a b c} → TransReflClosure R a b → TransReflClosure R b c → TransReflClosure R a c
[]ᵗ ++ᵗ b↝c = b↝c
s ∷ᵗ a↝b ++ᵗ b↝c = s ∷ᵗ (a↝b ++ᵗ b↝c)

-- concatenation is associative
++ᵗ-assoc : ∀ {a b c d} →
              (u : TransReflClosure R a b) →
              (v : TransReflClosure R b c) →
              (w : TransReflClosure R c d) →
              ((u ++ᵗ v) ++ᵗ w) ≡ (u ++ᵗ v ++ᵗ w)
++ᵗ-assoc []ᵗ v w = refl
++ᵗ-assoc (s ∷ᵗ u) v w = cong (_∷ᵗ_ s) (++ᵗ-assoc u v w)

-- reflexivity is right-unital (left-unitality holds by definition)
++ᵗ[]ᵗ : ∀ {a b} →
           {u : TransReflClosure R a b} →
           (u ++ᵗ []ᵗ) ≡ u
++ᵗ[]ᵗ {u = []ᵗ} = refl
++ᵗ[]ᵗ {u = s ∷ᵗ v} = cong (_∷ᵗ_ s) (++ᵗ[]ᵗ {u = v})

-- Some simple constructions on lists


module _ {ℓ₀ : Level} {A : Type ℓ₀} (P : A → Type ℓ₁) where
-- (not sure why Agda requires the variables explicitely here...)

  -- a type family (predicate) is inhabited (fulfilled) for all
  -- elements of a list
  forall-in-list : List A → Type (ℓ-max ℓ₀ ℓ₁)
  forall-in-list xs = foldr (λ a p → P a × p) Unit* xs

  forall-++ : (l₁ l₂ : List A) → (forall-in-list l₁) → (forall-in-list l₂)
                                → forall-in-list (l₁ ++ l₂)
  forall-++ [] l₂ _ p₂ = p₂
  forall-++ (a ∷ l₁) l₂ (pa , p₁) p₂ = pa , forall-++ l₁ l₂ p₁ p₂


  -- forall-in-list is invariant under list reversal
  forall-rev : (l : List A) → (forall-in-list l)
                            → forall-in-list (listrev l)
  forall-rev [] _ = tt*
  forall-rev (a ∷ l) (pa , pl) =
                     forall-++ (listrev l) [ a ] (forall-rev l pl) (pa , tt*)

{- Note: Lemmas such as
     object-list(l++k) = object-list(l) ++ tail object-list k
   are in the library, but marked as private. -}

-- Removing the first element from of a list
safe-tail : List A → List A
safe-tail []       = []
safe-tail (_ ∷ xs) = xs

-- Removing the last element from a list ("liat" is "tail" spelled
-- backwards)
safe-liat : List A → List A
safe-liat [] = []
safe-liat (x ∷ []) = []
safe-liat (x ∷ x₁ ∷ xs) = x ∷ safe-liat (x₁ ∷ xs)

-- We sometimes want to remove both the first and the last element
-- from a list (see `safe-middle` below).
-- Fortunately, it's quite easy to see that both obvious definitions
-- are equal:
compare-middle : (xs : List A) → safe-tail (safe-liat xs) ≡ safe-liat (safe-tail xs)
compare-middle [] = refl
compare-middle (x ∷ []) = refl
compare-middle (x₁ ∷ x₂ ∷ xs) = refl

-- This one seems to compute slightly better:
safe-middle : List A → List A
safe-middle xs = safe-tail (safe-liat xs)

{- If a property is valid for everything in a list, then it is in
   particular valid for parts of the list.
   We are mostly interested in the "safe-middle" part of a list, but
   to do this, we need to consider safe-liat first: -}
restrict-forall-list-liat : {ℓ₀ : Level} {A : Type ℓ₀} (P : A → Type ℓ₁) (l : List A)
                            → forall-in-list P l → forall-in-list P (safe-liat l)
restrict-forall-list-liat P [] _ = tt*
restrict-forall-list-liat P (a₁ ∷ []) pl = tt*
restrict-forall-list-liat P (a₁ ∷ a₂ ∷ l) (p₁ , pa₂l) =
                                       p₁ , restrict-forall-list-liat P (a₂ ∷ l) pa₂l

-- Then, we consider safe-tail:
restrict-forall-list-tail : {ℓ₀ : Level} {A : Type ℓ₀} (P : A → Type ℓ₁) (l : List A)
                            → forall-in-list P l → forall-in-list P (safe-tail l)
restrict-forall-list-tail P [] _ = tt*
restrict-forall-list-tail P (a ∷ l) (_ , pl) = pl

-- And finally, we can show that (safe-middle l) satisfies a property
-- if the original list l does!
restrict-forall-list : {ℓ₀ : Level} {A : Type ℓ₀} (P : A → Type ℓ₁) (l : List A)
                       → forall-in-list P l → forall-in-list P (safe-middle l)
restrict-forall-list P l pl =
  restrict-forall-list-tail P (safe-liat l)
    (restrict-forall-list-liat P l pl)


-- probably don't need this one:
-- compute-middle-l : (x : A) (xs : List A) → safe-middle (x ∷ xs) ≡ safe-liat xs
-- compute-middle-l x xs = compare-middle (x ∷ xs)

module _ {A : Type ℓ₀} {R : BinRel A ℓ₁} where

  private
    _↝*_ = TransReflClosure R

  -- length of a sequence of relation steps
  lengthᵗ : ∀ {a b} → (a ↝* b) → ℕ
  lengthᵗ []ᵗ = 
  lengthᵗ (s ∷ᵗ u) = suc (lengthᵗ u)

  -- concatenation preserves length
  ++-length : ∀ {a b c} (u : a ↝* b) (v : b ↝* c)
                → lengthᵗ (u ++ᵗ v) ≡ lengthᵗ u + lengthᵗ v
  ++-length []ᵗ v = refl
  ++-length (x ∷ᵗ u) v = cong suc (++-length u v)

  -- if elements are related by a sequence of length zero,
  -- then they are equal
  length≡0 : ∀ {a b} {u : a ↝* b} → (lengthᵗ u ≡ ) → a ≡ b
  length≡0 {u = []ᵗ} _ = refl
  length≡0 {u = x ∷ᵗ u} suc≡0 =
              Cubical.Data.Empty.rec (<→≢ tt (sym suc≡0))

{- Note: The reason why we do this again is that `R` in ++ and `R` in
  `reverse` are different. (Can this be avoided?) -}
module _ {A : Type ℓ₀} {R : BinRel A ℓ₁} where

  private
    _↝*_ = TransReflClosure R
    _↔_ = SymClosure R
    _↔*_ = TransReflClosure (SymClosure R)

  -- reverse on the symmetric closure
  negate : ∀ {a b} → (a ↔ b) → (b ↔ a)
  negate (inj s) = rev s
  negate (rev s) = inj s

  -- reversing is self-inverse
  negate-negate : ∀ {a b} → (s : a ↔ b) → negate (negate s) ≡ s
  negate-negate (inj s) = refl
  negate-negate (rev s) = refl

  -- reversing a sequence
  -- (this is the obvious generalisation of a lemma in
  -- Cubical.Data.List.Properties)
  reverse : ∀ {a c} → (a ↔* c) → (c ↔* a)
  reverse []ᵗ = []ᵗ
  reverse (s ∷ᵗ b↝c) = (reverse b↝c) ++ᵗ (negate s ∷ᵗ []ᵗ)

  -- auxiliary lemma
  reverse-snoc : ∀ {a c d} → (u : a ↔* c) (z : c ↔ d) →
                   reverse (u ++ᵗ z ∷ᵗ []ᵗ) ≡ (negate z) ∷ᵗ reverse u
  reverse-snoc []ᵗ z = refl
  reverse-snoc (s ∷ᵗ b↝c) z = cong (_++ᵗ negate s ∷ᵗ []ᵗ) (reverse-snoc b↝c z)

  -- reversing a sequence is self-inverse
  reverse-reverse : ∀ {a c} → (u : a ↔* c) → reverse (reverse u) ≡ u
  reverse-reverse []ᵗ = refl
  reverse-reverse (s ∷ᵗ b↝c) =
    reverse (reverse (s ∷ᵗ b↝c))
      ≡⟨ reverse-snoc (reverse b↝c) (negate s) ⟩
    negate (negate s) ∷ᵗ reverse (reverse b↝c)
      ≡⟨ cong (λ s' → s' ∷ᵗ reverse (reverse  b↝c)) (negate-negate s) ⟩
    s ∷ᵗ reverse (reverse b↝c)
      ≡⟨ cong (_∷ᵗ_ s) (reverse-reverse b↝c) ⟩
    s ∷ᵗ b↝c
      ∎

  -- reverse and ++ᵗ interact in the usual way:
  reverse-++ᵗ : ∀ {a b c} (u : a ↔* b) (v : b ↔* c) →
                  (reverse (u ++ᵗ v)) ≡ ((reverse v) ++ᵗ (reverse u))
  reverse-++ᵗ []ᵗ v = subst (λ w → reverse v ≡ w) (sym ++ᵗ[]ᵗ) refl
  reverse-++ᵗ (s ∷ᵗ u) v =
    reverse (u ++ᵗ v) ++ᵗ negate s ∷ᵗ []ᵗ
      ≡⟨ cong {x = reverse (u ++ᵗ v)}
               {y = reverse v ++ᵗ reverse u}
               (λ w → w ++ᵗ negate s ∷ᵗ []ᵗ)
               (reverse-++ᵗ u v) ⟩
    ((reverse v ++ᵗ reverse u) ++ᵗ negate s ∷ᵗ []ᵗ)
      ≡⟨ ++ᵗ-assoc (reverse v) (reverse u) _ ⟩
    reverse v ++ᵗ reverse u ++ᵗ negate s ∷ᵗ []ᵗ
      ∎


  -- embedding the reflexive-transitive closure into the
  -- symmetric-reflexive-transitive closure:

  embed⁺ : ∀ {a c} → (a ↝* c) → (a ↔* c)
  embed⁺ []ᵗ = []ᵗ
  embed⁺ (s ∷ᵗ b↝c) = inj s ∷ᵗ embed⁺ b↝c

  embed⁻ : ∀ {a c} → (a ↝* c) → (c ↔* a)
  embed⁻ []ᵗ = []ᵗ
  embed⁻ (s ∷ᵗ b↝c) = embed⁻ b↝c ++ᵗ (rev s ∷ᵗ []ᵗ)

  {- Note: We might define embed⁻ as reverse ∘ embed⁺, but the same work
     would probably have to be done somewhere else. -}
  -- a simple lemma on massaging embeddings.
  rewrite-embed⁻ : ∀ {a c} → (u : a ↝* c) → embed⁻ u ≡ reverse (embed⁺ u)
  rewrite-embed⁻ []ᵗ = refl
  rewrite-embed⁻ (s ∷ᵗ u) = cong (λ v → v ++ᵗ rev s ∷ᵗ []ᵗ) (rewrite-embed⁻ u)

  rewrite-embed⁺ : ∀ {a c} → (u : a ↝* c) → embed⁺ u ≡ reverse (embed⁻ u)
  rewrite-embed⁺ u =
    embed⁺ u
      ≡⟨ sym (reverse-reverse _) ⟩
    reverse (reverse (embed⁺ u))
      ≡⟨ cong reverse (sym (rewrite-embed⁻ u)) ⟩
    reverse (embed⁻ u)
      ∎

  -- embeddings don't change the length (1)
  emb⁻-length : ∀ {a c} → (u : a ↝* c) → lengthᵗ (embed⁻ u) ≡ lengthᵗ u
  emb⁻-length []ᵗ = refl
  emb⁻-length (a↝b ∷ᵗ b↝*c) =
    lengthᵗ (embed⁻ b↝*c ++ᵗ rev a↝b ∷ᵗ []ᵗ)
      ≡⟨ ++-length (embed⁻ b↝*c) (rev a↝b ∷ᵗ []ᵗ) ⟩
    lengthᵗ (embed⁻ b↝*c) + _ -- yellow: lengthᵗ (rev a↝b ∷ᵗ []ᵗ)
      ≡⟨ cong (λ n → n + ) (emb⁻-length b↝*c) ⟩
    (lengthᵗ b↝*c) + 
      ≡⟨ +-comm _  ⟩
    suc (lengthᵗ b↝*c)
      ∎

  -- embeddings don't change the length (2)
  emb⁺-length : ∀ {a c} → (u : a ↝* c) → lengthᵗ (embed⁺ u) ≡ lengthᵗ u
  emb⁺-length []ᵗ = refl
  emb⁺-length (a↝b ∷ᵗ b↝*c) = cong suc (emb⁺-length b↝*c)

  -- embedding-concatenation rewriting
  emb⁻-++ : ∀ {a b c} (u : a ↝* b) (v : b ↝* c)
              → embed⁻ (u ++ᵗ v) ≡ (embed⁻ v ++ᵗ embed⁻ u)
  emb⁻-++ []ᵗ v = sym ++ᵗ[]ᵗ
  emb⁻-++ (x ∷ᵗ u) v =
    (embed⁻ (u ++ᵗ v) ++ᵗ rev x ∷ᵗ []ᵗ)
      ≡⟨ cong (λ uv → uv ++ᵗ rev x ∷ᵗ []ᵗ) (emb⁻-++ u v) ⟩
    (embed⁻ v ++ᵗ embed⁻ u) ++ᵗ rev x ∷ᵗ []ᵗ
      ≡⟨ ++ᵗ-assoc (embed⁻ v) (embed⁻ u) (rev x ∷ᵗ []ᵗ) ⟩
    (embed⁻ v ++ᵗ embed⁻ u ++ᵗ rev x ∷ᵗ []ᵗ)
      ∎

  {- Note: a specialised construction: -}

  object-list : ∀ {b c} → (b ↝* c) → List A
  object-list ([]ᵗ {a}) = a ∷ [] -- [ a ]
  object-list (_∷ᵗ_ {a} {b} {c} _ b↝c) = a ∷ object-list b↝c

{-
  ∷ᵗ-to-∷ : ∀ {a b c} (u : a ↝* b) (v : b ↝* c) →
              object-list (u ++ᵗ v) ≡ object-list u ++ (safe-tail (object-list v))
  ∷ᵗ-to-∷ []ᵗ []ᵗ = refl
  ∷ᵗ-to-∷ []ᵗ (v₀ ∷ᵗ v) = refl
  ∷ᵗ-to-∷ (u₀ ∷ᵗ u) v = cong (_ ∷_) (∷ᵗ-to-∷ u v)
-}

  obj-++-commute : ∀ {a b c} (u : a ↝* b) (v : b ↝* c) →
                     object-list (u ++ᵗ v) ≡ object-list u ++ (safe-tail (object-list v))
  obj-++-commute []ᵗ []ᵗ = refl
  obj-++-commute []ᵗ (v₀ ∷ᵗ v) = refl
  obj-++-commute (u₀ ∷ᵗ u) v = cong (_ ∷_) (obj-++-commute u v)


module _ {A : Type ℓ₀} {R : BinRel A ℓ₁} where
  private
    _↝*_ = TransReflClosure R

  -- embedding negatively and then taking the object list
  -- is
  -- embedding positively, taking the object list, and reversing
  obj-emb-rev : ∀ {a b} (u : a ↝* b) →
                  object-list (embed⁻ u) ≡ listrev (object-list (embed⁺ u))
  obj-emb-rev []ᵗ = refl
  obj-emb-rev (_∷ᵗ_ {a} {a₁} {b} u₀ u) =
    object-list (embed⁻ (u₀ ∷ᵗ u))
      ≡⟨ refl ⟩
    object-list (embed⁻ u ++ᵗ rev u₀ ∷ᵗ []ᵗ)
      ≡⟨ obj-++-commute (embed⁻ u) (rev u₀ ∷ᵗ []ᵗ) ⟩
    object-list (embed⁻ u) ++ (safe-tail (a₁ ∷ a ∷ []))
                -- not sure why Agda doesn't accept   _ ∷ a ∷ []
      ≡⟨ refl ⟩
     object-list (embed⁻ u) ++ (a ∷ [])
      ≡⟨ cong (λ l → l ++ (a ∷ [])) (obj-emb-rev u) ⟩
    listrev (object-list (embed⁺ u)) ++ (a ∷ [])
      ≡⟨ refl ⟩
    listrev (object-list (embed⁺ (u₀ ∷ᵗ u)))
      ∎


module _ {A : Type ℓ₀} {R : BinRel A ℓ₁} where

  private
    _↝_ = R
    _↝*_ = TransReflClosure R

  safe-liat-a∷obj : ∀ {a b c} (u : b ↝* c)
    → safe-liat (a ∷ object-list u) ≡ a ∷ safe-liat (object-list u)
  safe-liat-a∷obj []ᵗ = refl
  safe-liat-a∷obj (x ∷ᵗ u) = refl

  {-
  There seems to be a strange termination failure that makes our
  lives hard. This is Agda version 2.6.2.2.

  -- The following does not termination check:
  mwe : ∀ {a b} (u : a ↝* b) → Unit
  mwe []ᵗ = tt
  mwe (s ∷ᵗ []ᵗ) = tt
  mwe (s ∷ᵗ t ∷ᵗ u) = mwe (t ∷ᵗ u)

  -- Even though is works with lists:
  works : List A → Unit
  works [] = tt
  works (s ∷ []) = tt
  works (s ∷ t ∷ u) = works (t ∷ u)

  For this reason, we need an ulgy workaround, where we introduce
  an explicit list, in the following:
  -}


  remove-last-aux : (xs : List A) {a b : A} (u : a ↝* b)
    (p : object-list u ≡ xs)
    → object-list u ≡ safe-liat (object-list u) ++ [ b ]
  remove-last-aux [] []ᵗ p = refl
  remove-last-aux [] (_ ∷ᵗ []ᵗ) p = refl
  remove-last-aux [] (s₀ ∷ᵗ s₁ ∷ᵗ u) p = Cubical.Data.Empty.rec (¬cons≡nil p)
  remove-last-aux (x ∷ xs) []ᵗ p = refl
  remove-last-aux (x ∷ xs) {a} {b} (s ∷ᵗ u) p =
    a ∷ object-list u
      ≡⟨ cong (a ∷_) (remove-last-aux xs u (cong safe-tail p)) ⟩
    a ∷ safe-liat (object-list u) ++ [ b ]
      ≡⟨ cong (_++ [ b ]) (sym (safe-liat-a∷obj u)) ⟩
    safe-liat (a ∷ object-list u) ++ [ b ]
      ∎

  remove-last : ∀ {a b} (u : a ↝* b) →
    object-list u ≡ safe-liat (object-list u) ++ [ b ]
  remove-last u = remove-last-aux (object-list u) u refl

  split-object-list : ∀ {a b c} (s : a ↝ b) (u : b ↝* c) →
    object-list (s ∷ᵗ u) ≡ a ∷ safe-middle (object-list (s ∷ᵗ u)) ++ [ c ]
  split-object-list {a} {b} {c} s u = cong (a ∷_) (sym calc)
    where
      calc = safe-tail (safe-liat (a ∷ object-list u)) ++ [ c ]
               ≡⟨ cong (λ l → safe-tail l ++ [ c ]) (safe-liat-a∷obj u) ⟩
             safe-tail (a ∷ safe-liat (object-list u)) ++ [ c ]
               ≡⟨ refl ⟩
             safe-liat (object-list u) ++ [ c ]
               ≡⟨ sym (remove-last u) ⟩
             object-list u
               ∎

-- Finally, we consider the transitive closure without the reflexive component:
data TransClosure {A : Type ℓ₀} (R : BinRel A ℓ₁) : BinRel A (ℓ-max ℓ₀ ℓ₁) where
  [_]⁺ : {a b : A} → R a b → TransClosure R a b
  _∷⁺_ : {a b c : A} → R a b → TransClosure R b c → TransClosure R a c

-- Being transitive is defined in the usual way.
isTransitive : BinRel A ℓ₁ → Type _
isTransitive _~_ = ∀ {x y z} → x ~ y → y ~ z → x ~ z

-- The transivite closure is transitive. (And of course, the same is
-- the case for the reflexive-transitive closure, but we don't need
-- that, so we don't prove it.)

infixr  _++⁺_

_++⁺_ : isTransitive (TransClosure R)
[ a↝b ]⁺ ++⁺ b↝c = a↝b ∷⁺ b↝c
(a↝b₀ ∷⁺ b₀↝b) ++⁺ b↝c = a↝b₀ ∷⁺ (b₀↝b ++⁺ b↝c)

-- Reversing a relation commutes with taking the transitive closure.
-- We only implement one direction (since it suffices for us):

revClosureComm : {a b : A} → (TransClosure R b a) → TransClosure (λ x y → R y x) a b
revClosureComm [ b↝a ]⁺ = [ b↝a ]⁺
revClosureComm {a = a} {b = b} (b↝b₁ ∷⁺ b₁↝*a) = (revClosureComm b₁↝*a) ++⁺ [ b↝b₁ ]⁺

-- Finally, we related the two transitive closures.
-- Of course there would be a lot more to say, but we only need the
-- following:
_++⁺*_ : {a b c : A} → TransClosure R a b
                     → TransReflClosure R b c
                     → TransClosure R a c
a↝⁺b ++⁺* []ᵗ = a↝⁺b
a↝⁺b ++⁺* (b↝b₁ ∷ᵗ b₁↝*c) = (a↝⁺b ++⁺ [ b↝b₁ ]⁺) ++⁺* b₁↝*c