{-
GENERALISATIONS OF NEWMAN'S LEMMA

Several core constructions. If a relation is wellfounded, then several
notions of confluence are interderivable. In particular, from a
Winkler-Buchberger structure (i.e. a very weak form of confluence),
we can construct a Church-Rosser structure (a strong form of
confluence).
-}

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Empty hiding (rec)
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.graphclosures
open import squier.polygraphs



-- Level variables are fixed for the whole module
module squier.newman {ℓ₀ ℓ₁ ℓ₂ : Level} (p : 2-polygraph {ℓ₀} {ℓ₁} {ℓ₂}) where

private variable
  ℓ₃ : Level


open polygraph-properties p

-- ### various confluence structures

-- having a Winkler-Buchberger structure:
-- for any local peak ("span"), there is a zig-zag that stays under the peak.
hasWB : hasOrder {ℓ₃} → Type _
hasWB (_>_ , _) = ∀ {y x z} (s : x ↝ y) (t : x ↝ z) →
                    Σ[ u ∈ y ↭* z ]
                      forall-in-list {ℓ₀ = ℓ₀} (λ a → x > a) (safe-middle (object-list u))
                      × (mkLocalPeak s t ⇔* u)

-- having local confluence structure:
-- any local peak can be completed to a "diamond"
hasLC = ∀ {y x z} (s : x ↝ y) (t : x ↝ z) →
          Σ[ x' ∈ Σ₀ ]
          Σ[ s' ∈ y ↝* x' ]
          Σ[ t' ∈ z ↝* x' ]
             (mkLocalPeak s t ⇔* mkValley s' t')

-- having confluence structure:
-- any peak (arbitrarily many steps) can be completed to a "diamond"
hasC = ∀ {y x z} (s : x ↝* y) (t : x ↝* z) →
         Σ[ x' ∈ Σ₀ ]
         Σ[ s' ∈ y ↝* x' ]
         Σ[ t' ∈ z ↝* x' ]
           (mkPeak s t ⇔* mkValley s' t')

-- having a Church-Rosser structure:
-- any zig-zag can be replaced by a valley
hasCR = ∀ {y z} (u : y ↭* z) →
          Σ[ x' ∈ Σ₀ ]
          Σ[ s' ∈ y ↝* x' ]
          Σ[ t' ∈ z ↝* x' ]
            (u ⇔* mkValley s' t')

{- Note: LC and C aren't actually used. Is is easier to got from WB
   to CR directly. -}

-- WB generates a zig-zag that is actually smaller
module _ (ord : hasOrder {ℓ₃}) (wb : hasWB ord) where

  private
    _>_ = fst ord
    open import squier.listextension Σ₀ (λ x y → y > x)
    _<ᴸ⁺_ = TransClosure _<ᴸ_


  wb-smaller-aux : ∀ {y x z} (s : x ↝ y) (t : x ↝ z) → (u : y ↭* z)
                     → (forall-in-list {ℓ₀ = ℓ₀} (λ a → x > a)
                                        (safe-middle (object-list u)))
                     → object-list u <ᴸ⁺ object-list (mkLocalPeak s t)
  wb-smaller-aux {y} {x} {.y} s t []ᵗ ∀> =
                 (stp {x} {[]} {[ y ]} _) ∷⁺ [ (stp {y} {[]} {x ∷ [ y ]} _) ]⁺
  wb-smaller-aux {y} {x} {z} s t (u₀ ∷ᵗ u) ∀> =
    let
      split-u₀u = split-object-list {R = SymClosure _↝_} u₀ u
      y-middle-z-<-y-x-z : (y ∷ safe-middle (y ∷ object-list u) ++ [ z ])
                              <ᴸ⁺ (y ∷ x ∷ z ∷ [])
      y-middle-z-<-y-x-z =
        [ add {n = y} (stp {x} {safe-middle (y ∷ object-list u)} {[ z ]} ∀>) ]⁺
    in
      subst (λ v → v <ᴸ⁺ (y ∷ x ∷ z ∷ [])) (sym split-u₀u) y-middle-z-<-y-x-z



  wb-smaller : ∀ {y x z} (s : x ↝ y) (t : x ↝ z)
                 → object-list (fst (wb s t)) <ᴸ⁺ object-list (mkLocalPeak s t)
  wb-smaller {y} {x} {z} s t =
                 wb-smaller-aux s t (fst (wb s t)) (fst (snd (wb s t)))

-- from Winkler-Buchberger to Church-Rosser
module wb2cr {ℓ₃ : Level} (cc : ⇔*isCongrClosed) (ord : hasOrder {ℓ₃})
             (noether : isNoetherian ord) (wb : hasWB ord) where

  private
    _>_ = fst ord
    ↝2> = snd ord

  open import squier.listextension Σ₀ (λ x y → y > x)

  _<ᴸ⁺_ = TransClosure _<ᴸ_

  -- The type family P that we want to do wellfounded induction on:
  P : List Σ₀ → Type _
  P l = ∀ {y z} (u : y ↭* z) → l ≡ (object-list u) →
            Σ[ x ∈ Σ₀ ]
            Σ[ s ∈ y ↝* x ]
            Σ[ t ∈ z ↝* x ]
              (u ⇔* mkValley s t)
              × ((object-list (mkValley s t) <ᴸ⁺ l) ⊎ (u ≡ mkValley s t))


  -- we prove P by wellfounded induction
  induction : (l : List Σ₀) (ih : ∀ l' → l' <ᴸ⁺ l → P l') → P l
  -- First case: the zig-zag is empty
  induction l ih {y} {.y} []ᵗ l≡[] = y , []ᵗ , []ᵗ , []ᵗ , inr refl
  -- Second case: the zig-zag is `q ∷ᵗ u`
  induction l ih {y} {z} (q ∷ᵗ u) l≡qu
    {- In this case, we calculate the valley for the smaller zig-zag u.
       There are two ways to do this; either use structural induction,
       i.e. recursively call `induction`, or use wellfounded induction,
       i.e. use `ih`. The term for structural induction is
         induction (object-list u)
               (λ l' l'<u → e l' (l'<u ++ᵗ subst (λ ll → object-list u <ᴸ ll)
                                  (sym l≡qu)
                                  (stp {y} tt*) ∷ᵗ []ᵗ))
               u
               refl
       In the Agda code below, we instead us wellfounded induction: -}
    with ih (object-list u)
            [ subst (λ ll → object-list u <ᴸ ll) (sym l≡qu) (stp {y} tt*) ]⁺
            u refl
  {- By induction, we now get:

            q        u
         y <-> b <-------> z
                \         /
                 \   α   /
                s \     /t
                   \   /
                     x

     In addition, we EITHER get a proof `st<u` which says that that
     (s.t) is stricly less than u, OR a proof `u≡st` which says that
     (s.t) is equal to u. We distinguish these cases by pattern matching.
     In the first case, we get `st<u`:
  -}
  induction l ih {y} {z} (q ∷ᵗ u) l≡qu | x , s , t , α , inl st<u =
    -- In this case, we apply the induction hypothesis `ih` to q.s.t;
    -- this allows us to simply calculate the result:
    let
      -- useful inequality:
      yst<l = subst (λ l' → object-list(q ∷ᵗ mkValley s t) <ᴸ⁺ l')
                    (sym l≡qu)
                    (add+ {y} st<u)
      -- then the actual call
      (x₁ , s₁ , t₁ , α₁ , s₁t₁<qst-⊎-qst≡s₁t₁) =
          ih (object-list (q ∷ᵗ (mkValley s t)))
             yst<l
             (q ∷ᵗ (mkValley s t))
             refl
      α-combined =
          (q ∷ᵗ u
             ⇔*⟨ ⇔*cc2ccr cc (q ∷ᵗ []ᵗ) u (mkValley s t) α ⟩
           q ∷ᵗ mkValley s t
             ⇔*⟨ α₁ ⟩
           mkValley s₁ t₁
             ⇔*∎)
      -- Now we need to say: Is the constructed valley strictly less
      -- than what we started with, or is it equal to what we started
      -- with? Of course, it's strictly less. However, we need to
      -- case-split on what `s₁t₁<qst-⊎-s₁t₁≡qst` is.
      s₁t₁<qu =
          rec {A = object-list (mkValley s₁ t₁) <ᴸ⁺ object-list (q ∷ᵗ mkValley s t)}
              {B = q ∷ᵗ mkValley s t ≡ mkValley s₁ t₁}
              {C = object-list (mkValley s₁ t₁) <ᴸ⁺ l}
              (λ st<yst → st<yst ++⁺ yst<l)
              (λ qst≡s₁t₁ → subst (λ v → object-list v <ᴸ⁺ l) qst≡s₁t₁ yst<l)
              s₁t₁<qst-⊎-qst≡s₁t₁

    in (x₁ , s₁ , t₁ , α-combined , inl s₁t₁<qu)

  -- Finally, the other case in which `u` and `s.t` are already equal.
  -- We get a proof `u≡st`. In addition, we pattern match on `q`.
  -- Recall that `q` is a single step and can either go into the
  -- direction → or the direction ←.
  -- Case: `q` goes into the direction →
  induction l ih {y} {z} (inj q ∷ᵗ u) l≡qu | x , s , t , α , inr u≡st =
    {- This case is easy; the span that we want is now given by

                     u
               y <-------> z
                \         /
                 \  q.α  /
               q.s\     /t
                   \   /
                     x

    -}
    let
      -- q.α
      qu⇔*qst = ⇔*cc2ccr cc (inj q ∷ᵗ []ᵗ) u (mkValley s t) α
      -- The newly constructed valley is equal to what we already had:
      qu≡qst = cong (λ u' → inj q ∷ᵗ u') u≡st
    in
      x , q ∷ᵗ s , t , qu⇔*qst , inr qu≡qst

  -- Case: `q` goes into the direction ←. Here, we additionally
  -- distinguish two cases:
  -- Either `s` is the empty sequence `[]ᵗ`:
  induction l ih {y} {z} (rev q ∷ᵗ u) l≡qu | x , []ᵗ , t , α , inr u≡t =
    -- This is easy, as all arrows in q.t go into direction ←, which
    -- means ([]ᵗ , t.q) is already a span:
    y , []ᵗ , (t ++ᵗ q ∷ᵗ []ᵗ) , α₁ , inr qu≡qt
      where
        qu≡qt : (rev q ∷ᵗ u) ≡ embed⁻ (t ++ᵗ q ∷ᵗ []ᵗ)
        qu≡qt =
             (rev q ∷ᵗ u)
               ≡⟨ cong (rev q ∷ᵗ_) u≡t ⟩
             (rev q ∷ᵗ embed⁻ t)
               ≡⟨ sym (emb⁻-++ t (q ∷ᵗ []ᵗ)) ⟩
             (embed⁻ (t ++ᵗ q ∷ᵗ []ᵗ))
               ∎
        α₁ : (rev q ∷ᵗ u) ⇔* (embed⁻ (t ++ᵗ q ∷ᵗ []ᵗ))
        α₁ = ≡→[] qu≡qt


  {- ... or `s` is not empty and starts with a segment, i.e. is of the
     form `s₀ ∷ᵗ s`.
     Then, the situation can be depicted as follows:

             q   s₀    s       t
          y <- b -> c ---> x <--- z

                  u = s₀.s.t
  -}
  induction l ih {y} {z} (rev q ∷ᵗ u) l≡qu | x , s₀ ∷ᵗ s , t , u⇔*s₀st , inr u≡s₀st =
    let
      -- We use the WB property on the span q·s₀:
      (v , all< , v⇔*qs₀) = wb q s₀

      {- Thus:
                 q   s₀    s       t
              y <- b -> c ---> x <--- z   =  q·u
              \________/
                  v
      -}

      vst = v ++ᵗ mkValley s t

      qs₀st⇔*vst : (rev q ∷ᵗ inj s₀ ∷ᵗ (mkValley s t)) ⇔* vst
      qs₀st⇔*vst = ⇔*cc2ccl cc (rev q ∷ᵗ inj s₀ ∷ᵗ []ᵗ) v (mkValley s t) v⇔*qs₀

      qu⇔*vst : (rev q ∷ᵗ u) ⇔* vst
      qu⇔*vst = subst (λ w → (rev q ∷ᵗ w) ⇔* vst) (sym u≡s₀st) qs₀st⇔*vst

      vst<qs₀st : object-list vst <ᴸ⁺ object-list (mkLocalPeak q s₀ ++ᵗ mkValley s t)
      vst<qs₀st =
        let
          mod-assoc  : ((object-list v) ++ (safe-tail (object-list (mkValley s t))))
                       <ᴸ⁺
                       ((object-list (mkLocalPeak q s₀)) ++
                                     (safe-tail (object-list (mkValley s t))))
          mod-assoc  = cc-r {object-list v}
                            {object-list (mkLocalPeak q s₀)}
                            {safe-tail (object-list (mkValley s t))}
                            (wb-smaller ord  wb q s₀)

          rebracket₁ : ((object-list v) ++ (safe-tail (object-list (mkValley s t))))
                       <ᴸ⁺
                       (object-list (mkLocalPeak q s₀ ++ᵗ mkValley s t))
          rebracket₁ = subst (λ w → ((object-list v) ++
                                          (safe-tail (object-list (mkValley s t)))) <ᴸ⁺ w)
                             (sym (obj-++-commute (mkLocalPeak q s₀) (mkValley s t)))
                             mod-assoc
          rebracket₂ : object-list vst <ᴸ⁺ object-list (mkLocalPeak q s₀ ++ᵗ mkValley s t)
          rebracket₂ = subst (λ w → w <ᴸ⁺ object-list (mkLocalPeak q s₀ ++ᵗ mkValley s t))
                             (sym (obj-++-commute v (mkValley s t)))
                             rebracket₁

        in
          rebracket₂

      vst<l : object-list vst <ᴸ⁺ l
      vst<l = subst (λ ll → _ <ᴸ⁺ ll)
                    (sym (l≡qu ∙ cong (y ∷_) (cong object-list u≡s₀st)))
                    vst<qs₀st

      {- Since `vst` is smaller than the original zig-zag, we can
        apply the induction hypothesis `ih`. -}
      (x₁ , s₁ , t₁ , vst⇔*s₁t₁ , s₁t₁<vst-⊎-vst≡s₁t₁) =
                                                       ih (object-list vst) vst<l vst refl

      qu⇔*s₁t₁ : (rev q ∷ᵗ u) ⇔* mkValley s₁ t₁
      qu⇔*s₁t₁ = qu⇔*vst ++ᵗ vst⇔*s₁t₁

      -- combine vst<l and s₁t₁<l-⊎-vst≡s₁t₁
      s₁t₁<l : object-list (mkValley s₁ t₁) <ᴸ⁺ l
      s₁t₁<l = rec (λ s₁t₁<vst → s₁t₁<vst ++⁺ vst<l)
                   (λ vst≡s₁t₁ → subst (λ w → object-list w <ᴸ⁺ l) vst≡s₁t₁ vst<l)
                   s₁t₁<vst-⊎-vst≡s₁t₁

    in
      x₁ , s₁ , t₁ , qu⇔*s₁t₁ , inl s₁t₁<l

  all-P : (xs : List Σ₀) → P xs
  all-P = WFI.induction {_<_ = _<ᴸ⁺_}
                        (transitive-wellfounded _ _ (isWF⟨<⟩⇒isWF⟨<ᴸ⟩ noether))
                        {P = P}
                        induction

  -- ... and finally, we get the desired result
  cr : hasCR
  cr {y} {z} u =
    let (x , s , t , α , _) = all-P (object-list u) {y} {z} u refl
    in (x , s , t , α)