{-
HOMOTOPY BASIS

Using the results of the previous modules, we construct a homotopy
basis for a terminating/Noetherian 2-polygraph with a Winkler-
Buchberger structure.
-}

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Nat

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
open import Cubical.Relation.Nullary.Base

open import squier.accessibility
open import squier.listextension
open import squier.graphclosures

open import squier.polygraphs
open import squier.cancelInverses
open import squier.newman

module squier.homotopybasis {ℓ₀ ℓ₁ ℓ₂ : Level} (p : 2-polygraph {ℓ₀} {ℓ₁} {ℓ₂}) where

open polygraph-properties p

hasHomotopyBasis = ∀ {x y} (u v : x ↭* y) → u ⇔* v
cancelsEmpty = ∀ {x} (u : x ↭* x) → lengthᵗ u ≡  → u ⇔* []ᵗ

private variable
  ℓ₃ : Level

-- ### constructing a homotopy basis, main lemma
-- Here: make convenient assumption; later, we use this to
-- derive the result from weaker assumptions.
module basis-construction
              (ord : hasOrder {ℓ₃})
              (noether : isNoetherian ord)
              (cr : hasCR p)
              (ce : cancelsEmpty)
              (cri : cancels*RInv p)
              (cc : ⇔*isCongrClosed) where

  -- as in above module
  _>_ = fst ord
  >-trans = fst (snd ord)
  ↝2> = snd (snd ord)

  -- recall that cancelling inverses on the right gives cancelling
  -- inverses on the left:
  cli = cancelsR2L p cri

  -- We assume that ⇔* is congruence-closed, but the special case where
  -- we only extend on one side turns out to be very useful:
  ccr : ⇔*isCongrClosedR
  ccr = ⇔*cc2ccr cc

  ccl : ⇔*isCongrClosedL
  ccl = ⇔*cc2ccl cc

  has-pre-hbasis : (x : Σ₀) → (u : x ↭* x) → (u ⇔* []ᵗ)
  has-pre-hbasis x₀ = acc-ind Σ₀ _<_ P (λ x _ → proof x) x₀ (noether x₀)
    where
    _<_ = λ x y → y > x
    P = λ x → (u : x ↭* x) → (u ⇔* []ᵗ)

    proof : (x : Σ₀) → ((y : Σ₀) → y < x → P y) → P x
    proof x ih u = goal
      where

        {- First, use CR to split u as follows:
                u
          x <-------> x
           \         /
            \   α   /
           v \     /w
              \   /
                x'
        -}

        -- Would like to write:
        -- (x' , v , w , α) = cr u
        -- But I don't get Agda to accept it. Thus:

        cru = cr u
        x' = fst cru
        v = fst (snd cru)
        w = fst (snd (snd cru))
        α = snd (snd (snd cru))

        open order
        -- Remember the following property: Either v has length 0, or x' < x.
        v≡0? : (lengthᵗ v ≡ ) ⊎ (x' < x)
        v≡0? = ↝*2≥ ord v
        -- Same for w:
        w≡0? : (lengthᵗ w ≡ ) ⊎ (x' < x)
        w≡0? = ↝*2≥ ord w


        -- Now: If both v and w have length 0, we are done by the
        -- following argument:
        -- (Note: If one has length 0, then so has the other, but
        --  we don't need to implement this.)
        case-v≡w≡0 : (lengthᵗ v ≡ ) → (lengthᵗ w ≡ ) → u ⇔* []ᵗ
        case-v≡w≡0 v≡0 w≡0 =
          u
            ⇔*⟨ α ⟩
          mkValley v w
            ⇔*⟨ ce (mkValley v w) (lengthᵗ (mkValley v w)
                                     ≡⟨ ++-length (embed⁺ v) (embed⁻ w) ⟩
                                  (lengthᵗ (embed⁺ v) + lengthᵗ (embed⁻ w))
                                     ≡⟨ cong (λ n → lengthᵗ (embed⁺ v) + n) (emb⁻-length w ∙ w≡0) ⟩
                                  (lengthᵗ (embed⁺ v) + )
                                     ≡⟨ cong (λ n → n + ) (emb⁺-length v ∙ v≡0) ⟩
                                  ( + )
                                     ≡⟨ refl ⟩
                                    ∎) ⟩
          []ᵗ

        -- Let's now do the case that x' < x.
        -- Since it will soon be very useful, we formulate another variation of
        -- "cancelling inverses":
        v⁺v⁻⇔*[] : (embed⁺ v ++ᵗ embed⁻ v) ⇔* []ᵗ
        v⁺v⁻⇔*[] = subst (λ w → (embed⁺ v ++ᵗ w) ⇔* []ᵗ) (sym (rewrite-embed⁻ v)) (cri (embed⁺ v))

        -- We then calculate:
        case-x'<x : (x' < x) → u ⇔* []ᵗ
        case-x'<x p =
          let
            -- We can now use the induction hypothesis for x':
            γ : mkPeak w v ⇔* []ᵗ
            γ = ih x' p (mkPeak w v)
          in
            u
              ⇔*⟨ α ⟩
            mkValley v w
              ⇔*⟨ ≡2⇔* (sym ++ᵗ[]ᵗ) ⟩
            (mkValley v w) ++ᵗ []ᵗ
              ⇔*⟨ ccr (mkValley v w) []ᵗ (embed⁺ v ++ᵗ embed⁻ v) (reverse v⁺v⁻⇔*[] ) ⟩
            (mkValley v w) ++ᵗ (embed⁺ v ++ᵗ embed⁻ v)
              ⇔*⟨ []ᵗ ⟩
            (embed⁺ v ++ᵗ embed⁻ w) ++ᵗ (embed⁺ v ++ᵗ embed⁻ v)
              ⇔*⟨ ≡2⇔* (++ᵗ-assoc (embed⁺ v) (embed⁻ w) (embed⁺ v ++ᵗ embed⁻ v)
                         ∙ cong (_++ᵗ_ (embed⁺ v))
                                (sym (++ᵗ-assoc (embed⁻ w) (embed⁺ v) (embed⁻ v)))) ⟩
            embed⁺ v ++ᵗ (embed⁻ w ++ᵗ embed⁺ v) ++ᵗ embed⁻ v
              ⇔*⟨ cc (embed⁺ v) (embed⁻ w ++ᵗ embed⁺ v) []ᵗ (embed⁻ v) γ ⟩
            embed⁺ v ++ᵗ []ᵗ ++ᵗ embed⁻ v
              ⇔*⟨ []ᵗ ⟩ -- nothing happening here!
            embed⁺ v ++ᵗ embed⁻ v
              ⇔*⟨ v⁺v⁻⇔*[] ⟩
            []ᵗ
              ⇔*∎

        -- Finally, we combine the cases:
        goal : u ⇔* []ᵗ
        goal with v≡0? | w≡0?
        goal | inl v≡0 | inl w≡0 = case-v≡w≡0 v≡0 w≡0
        goal | inl v≡0 | inr p   = case-x'<x p
        goal | inr p   | _       = case-x'<x p



  -- easy consequence: Two parallel sequences instead of a loop
  has-hbasis : hasHomotopyBasis
  has-hbasis {x} {y} u v =
    u
      ⇔*⟨ ≡2⇔* (sym ++ᵗ[]ᵗ)  ⟩
    u ++ᵗ []ᵗ
      ⇔*⟨ ccr u []ᵗ (reverse v ++ᵗ v) (reverse (cli v)) ⟩
    u ++ᵗ (reverse v) ++ᵗ v
      ⇔*⟨ ≡2⇔* (sym (++ᵗ-assoc u (reverse v) v)) ⟩
    (u ++ᵗ (reverse v)) ++ᵗ v
      ⇔*⟨ ccl (u ++ᵗ reverse v) []ᵗ v (has-pre-hbasis x (u ++ᵗ reverse v)) ⟩
    []ᵗ ++ᵗ v
      ⇔*⟨ []ᵗ ⟩
    v
      ⇔*∎

{- Note however that the above assumes a Church-Rosser structure.
   We can do better and only assume a Winkler-Buchberger structure,
   using the generalised Newman lemma of the previous module: -}

Noeth×WB×Congr×Cancel⇒Basis :
  (ord : hasOrder {ℓ₃}) → (isNoetherian ord) → (hasWB p ord) → ⇔*isCongrClosed
  → cancelsEmpty → cancels*RInv p → hasHomotopyBasis
Noeth×WB×Congr×Cancel⇒Basis ord noether wb cc ce cri =
  basis-construction.has-hbasis ord noether cr ce cri cc
    where
      cr : hasCR p
      cr = wb2cr.cr p cc ord noether wb