{-
NOETHERIAN INDUCTION FOR CLOSED ZIG-ZAGS

The construction of a homotopy basis allows us to prove an induction
principle:

Assume we have a Noetherian (i.e. co-wellfounded) binary relation
  _↝_ : A → A → Type
that comes with a local confluence structure: for any pair
  (s : x ↝ y, t : x ↝ z)
there is w : A together with a pair
  (u : y ↝ w, v : z ↝ w).
Let a (possibly proof-relevant) property P on closed zig-zags be given,
  P : (x : A) → (x ↭* x) → Type
and assume we want to prove P for all closed zig-zags. To do this, it
suffices to show the following:

(1) P holds for all zig-zags of length zero (if we only work with
    sets, this will only be the empty zig-zags on any given
    object).
(2) For all zig-zags s, P holds for s∙s⁻¹.
(3) P is closed under rotation of closed zig-zags, i.e. for
    u : x ↭* y
    v : y ↭* x
    we have P (u+v) → P (v+u)
(4) P is closed under pasting of zig-zags, i.e. for
    u and v and w : x ↭* y
    we have
    P (u+v⁻¹) → P (v+w⁻¹) → P (u+w⁻¹)
(5) P is closed under symmetry, i.e. for u : x ↭* x we have
    P (u) → P (u⁻¹)
(6) P holds for the "outlines" of the local confluence structure,
    i.e. for s,t as above with the chosen u,v, we have
    P (u⁻¹∙v + wb).

(Note that assumptions 2 and 5 could be removed, following the
strategy of our paper
"Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy
Type Theory", arXiv:2001.07655
However, this proof does not factor via a Squier-style construction
of a homotopy basis.
-}

{-# 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.List renaming (rev to listrev)
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
open import squier.homotopybasis



module squier.noethercycle {ℓ₀ ℓ₁ ℓ₂₃ : Level}
                           (A : Type ℓ₀) (_↝_ : BinRel A ℓ₁) where

_↝*_ = TransReflClosure _↝_
-- _↝+_ = TransClosure _↝_
_↭*_ = TransReflClosure (SymClosure _↝_)
_↝⁺_ = TransClosure _↝_

module _ (noether : isWellFounded (λ y x → x ↝ y))
         (localConf : ∀ {y x z} (s : x ↝ y) (t : x ↝ z) →
                                Σ[ w ∈ A ] (y ↝* w) × (z ↝* w))
         (P : ∀ {x} → (x ↭* x) → Type ℓ₂₃) where

  -- Assumptions of the induction principle:

  -- (1)
  EmptyFill = {x : A} {u : x ↭* x} → lengthᵗ u ≡  → P u

  -- (2)
  InverseCancel = ∀ {x y} (u : x ↭* y) → P (u ++ᵗ (reverse u))

  -- (3)
  RotationClosed = ∀ {x y} (u : x ↭* y) (v : y ↭* x) → P (u ++ᵗ v) → P (v ++ᵗ u)

  -- (4)
  PastingClosed = ∀ {x y} (u v w : x ↭* y)
                    → P (u ++ᵗ (reverse v))
                    → P (v ++ᵗ (reverse w))
                    → P (u ++ᵗ (reverse w))

  -- (5)
  SymClosed = ∀ {x} (u : x ↭* x) → P u → P (reverse u)

  -- (6)
  ConfluenceFill = ∀ {y x z} (s : x ↝ y) (t : x ↝ z) →
                     P (rev s ∷ᵗ inj t ∷ᵗ
                            (embed⁺ (snd (snd (localConf s t))) ++ᵗ
                             embed⁻ (fst (snd (localConf s t)))))

  -- We assume the properties of "induction for closed zig-zags":
  module _ (ef : EmptyFill) (ic : InverseCancel) (rc : RotationClosed)
           (pc : PastingClosed) (sc : SymClosed) (cf : ConfluenceFill) where


    -- As a small preparation, note that a special case of
    -- PastingClosed is ConcatClosed...
    ConcatClosed = ∀ {x} (u v : x ↭* x) → P u → P v → P (u ++ᵗ v)
    -- ... so let's derive it:
    cc : ConcatClosed
    cc u v pu pv =
      let
        pu₁ : P (u ++ᵗ (reverse []ᵗ))
        pu₁ = subst P (sym ++ᵗ[]ᵗ) pu

        pv₁ : P (reverse []ᵗ ++ᵗ (reverse (reverse v)))
        pv₁ = subst P (sym (reverse-reverse v)) pv

        puv₁ : P (u ++ᵗ (reverse (reverse v)))
        puv₁ = pc u []ᵗ (reverse v) pu₁ pv₁

        puv₂ : P (u ++ᵗ v)
        puv₂ = subst P (cong (u ++ᵗ_) (reverse-reverse v)) puv₁
      in
        puv₂

    -- Let's start with the main construction.
    -- The assumptions allow us to build a 2-polygraph:
    poly : 2-polygraph
    poly .2-polygraph.Σ₀ = A
    poly .2-polygraph._↝_ = _↝_
    poly .2-polygraph._⇒_ u v = P (u ++ᵗ reverse v)

    open polygraph-properties poly hiding (_↝_ ; _↭*_ ; _↝*_)

    -- A useful property of this polygraph is that the closure
    -- ⇔* does not relate more zig-zags than ⇒.
    -- More precisely, every u ⇔* v can be rewritten as
    -- a single step u ⇒ v.

    -- We show a simple auxiliary property first:
    ⇔-to-⇒ : ∀ {x y} {u v : x ↭* y} → (u ⇔ v) → (u ⇒ v)
    ⇔-to-⇒ (inj u⇒v) = u⇒v
    ⇔-to-⇒ {u = u} {v = v} (rev u⇐v) = p⟨uv⁻¹⟩ where
      -- we calculate step by step:
      p⟨⟨vu⁻¹⟩⁻¹⟩ : P (reverse (v ++ᵗ reverse u))
      p⟨⟨vu⁻¹⟩⁻¹⟩ = sc (v ++ᵗ (reverse u)) u⇐v
      -- we simply this expression:
      p⟨u⁻¹⁻¹v⁻¹⟩ : P (reverse (reverse u) ++ᵗ reverse v)
      p⟨u⁻¹⁻¹v⁻¹⟩ = subst P (reverse-++ᵗ v (reverse u)) p⟨⟨vu⁻¹⟩⁻¹⟩
      -- one more step:
      p⟨uv⁻¹⟩ : P (u ++ᵗ reverse v)
      p⟨uv⁻¹⟩ = subst P (cong (λ w → w ++ᵗ (reverse v)) (reverse-reverse _)) p⟨u⁻¹⁻¹v⁻¹⟩

    -- Now we're ready to show that ⇔* implies ⇒:
    ⇔*-to-⇒ : ∀ {x y} {u v : x ↭* y} → (u ⇔* v) → (u ⇒ v)
    ⇔*-to-⇒ {u = u} []ᵗ = ic u
    ⇔*-to-⇒ (_∷ᵗ_ {a = u} {b = u₁} {c = v} u⇔u₁ u₁⇔*v) = pc u u₁ v p₁ p₂
      where
        p₁ : P (u ++ᵗ (reverse u₁))
        p₁ = ⇔-to-⇒ u⇔u₁

        p₂ : P (u₁ ++ᵗ (reverse v))
        p₂ = ⇔*-to-⇒ u₁⇔*v



    -- We check that this polygraph has the properties required
    -- by the theorem that constructs a basis:

    ord : hasOrder
    ord = _↝⁺_ , _++⁺_ , [_]⁺

    ord-is-noether : isWellFounded _
    ord-is-noether = (transitive-Noetherian _ _ noether)

    {- Now comes a somewhat tedious step.
       If we have a diamond, then everything is below the top vertex.
       To make the induction go through, we allow arbitrary lengthes
       on each side: -}

    diamond-is-below-top : ∀ {x y z w} (s : x ↝⁺ y) (t : x ↝⁺ z)
                             (u : y ↝* w) (v : z ↝* w) →
                             forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (object-list (mkValley u v))
    -- easy case
    diamond-is-below-top s t []ᵗ []ᵗ = t , tt*
    -- another easy case
    diamond-is-below-top s t (u₀ ∷ᵗ u) v = s , diamond-is-below-top (s ++⁺ [ u₀ ]⁺) t u v
    -- well, this case is a lot of work...
    diamond-is-below-top {x} s t []ᵗ (_∷ᵗ_ {z} {z₁} {w} v₀ v) = goal where

      -- the goal of this lemma (Goal), and a variation of the goal (Goal₂):
      Goal = forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (object-list (mkValley []ᵗ (v₀ ∷ᵗ v)))
      Goal₂ = forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ v)) ++ [ z ])

      -- a calculation
      calc₁ = object-list (mkValley []ᵗ (v₀ ∷ᵗ v))
                ≡⟨ obj-emb-rev (v₀ ∷ᵗ v) ⟩
              listrev (object-list (embed⁺ (v₀ ∷ᵗ v)))
                ∎

      -- another calculation: turns out that Goal ≡ Goal₂
      calc₂ = Goal
                ≡⟨ refl ⟩
              forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (object-list (mkValley []ᵗ (v₀ ∷ᵗ v)))
                ≡⟨ cong (λ l → forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) l) calc₁ ⟩
              forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ (v₀ ∷ᵗ v))))
                ≡⟨ refl ⟩
              forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ v)) ++ [ z ])
                ≡⟨ refl ⟩
              Goal₂
                ∎

      -- the induction hypothesis
      IH = forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (object-list (mkValley []ᵗ v))
      ih : IH
      ih = diamond-is-below-top s (t ++⁺ [ v₀ ]⁺) []ᵗ v

      -- a variation of the induction hypothesis
      IH₂ = forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ v)))

      -- We apply the same lemma as above (in calc₁)
      calc₃ = object-list (mkValley []ᵗ v)
                ≡⟨ obj-emb-rev v ⟩
              listrev (object-list (embed⁺ v))
                ∎

      -- as before in calc₂, it turns out that IH ≡ IH₂
      calc₄ = IH
                ≡⟨ refl ⟩
              forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (object-list (mkValley []ᵗ v))
                ≡⟨ cong (λ l → forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) l) calc₃ ⟩
              forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ v)))
                ≡⟨ refl ⟩
              IH₂
                ∎

      -- thus, we can transport the induction hypothesis:
      ih₂ : IH₂
      ih₂ = subst (λ X → X) calc₄ ih

      -- this allows us to show the variation of the goal...
      goal₂ : Goal₂
      goal₂ = forall-++ {ℓ₀ = ℓ₀} (x ↝⁺_) (listrev (object-list (embed⁺ v))) [ z ] ih₂ (t , tt*)

      -- ... and thus the goal itself!
      goal : Goal
      goal = subst (λ X → X) (sym calc₂) goal₂

    {- Proving that a diamond is below the top was good and well,
       but what we actually want is that only the strict-bottom
       part (without the left and right corner) are below the top.
       And our diamond also only has sides of length 1 at the upper
       part. -}
    lower-diamond-is-below-top : ∀ {x y z w} (s : x ↝ y) (t : x ↝ z)
                                   (u : y ↝* w) (v : z ↝* w) →
                                   forall-in-list {ℓ₀ = ℓ₀} (x ↝⁺_)
                                     (safe-middle (object-list (mkValley u v)))
    lower-diamond-is-below-top {x} s t u v =
      restrict-forall-list (x ↝⁺_) (object-list (mkValley u v))
                           (diamond-is-below-top [ s ]⁺ [ t ]⁺ u v)

    ord-has-WB : hasWB poly ord
    ord-has-WB s t =
      let
        s⁺ = fst (snd (localConf s t))
        t⁺ = snd (snd (localConf s t))
        {-
                /\
              s/  \t
              /    \
              \    /
             s⁺\  /t⁺
                \/
        -}
      in
        (mkValley s⁺ t⁺) ,
        lower-diamond-is-below-top s t s⁺ t⁺ , -- a huge amount of work is hidden here!
        inj (subst P (cong (λ w → mkLocalPeak s t ++ᵗ w)
                     (aux-lemma s⁺ t⁺)) (cf s t))
        ∷ᵗ []ᵗ
          where
            aux-lemma : ∀ {y w z} (u : y ↝* w) (v : z ↝* w) →
                        ((embed⁺ v) ++ᵗ (embed⁻ u)) ≡ reverse (mkValley u v)
            aux-lemma u v =
              (embed⁺ v) ++ᵗ (embed⁻ u)
                ≡⟨ cong (λ w → w ++ᵗ (embed⁻ u)) (rewrite-embed⁺ v) ⟩
              (reverse (embed⁻ v)) ++ᵗ (embed⁻ u)
                ≡⟨ cong (reverse (embed⁻ v) ++ᵗ_) (rewrite-embed⁻ u) ⟩
              reverse (embed⁻ v) ++ᵗ reverse (embed⁺ u)
                ≡⟨ sym (reverse-++ᵗ (embed⁺ u) (embed⁻ v)) ⟩
              reverse (mkValley u v)
                ∎

    -- Closure under congruence requires some work.
    -- We prove a couple of properties in an auxiliary module:

    module congClosedPreparation {x₀ x y y₀} (w₀ : x₀ ↭* x) (u v : x ↭* y)
                                 (w₁ : y ↭* y₀) (α : u ⇔* v) where

      p₀ : P (u ++ᵗ (reverse v))
      p₀ = ⇔*-to-⇒ α

      p₁ : P ((u ++ᵗ (reverse v)) ++ᵗ (reverse w₀ ++ᵗ (reverse (reverse w₀))))
      p₁ = cc (u ++ᵗ (reverse v)) (reverse w₀ ++ᵗ (reverse (reverse w₀)))
               p₀ (ic (reverse w₀))

      p₂ : P ((u ++ᵗ (reverse v)) ++ᵗ (reverse w₀ ++ᵗ w₀))
      p₂ = subst (λ w → P ((u ++ᵗ (reverse v)) ++ᵗ (reverse w₀ ++ᵗ w)))
                  (reverse-reverse w₀)
                  p₁

      p₃ : P (u ++ᵗ (reverse v) ++ᵗ reverse w₀ ++ᵗ w₀)
      p₃ = subst P (++ᵗ-assoc u (reverse v) _) p₂

      p₄ : P (((reverse v) ++ᵗ reverse w₀ ++ᵗ w₀) ++ᵗ u)
      p₄ = rc u _ p₃

      p₅ : P ((((reverse v) ++ᵗ reverse w₀ ++ᵗ w₀) ++ᵗ u) ++ᵗ (w₁ ++ᵗ reverse w₁))
      p₅ = cc (((reverse v) ++ᵗ reverse w₀ ++ᵗ w₀) ++ᵗ u)
              (w₁ ++ᵗ reverse w₁)
              p₄
              (ic w₁)

      calc₁ = (reverse v ++ᵗ reverse w₀ ++ᵗ w₀) ++ᵗ u
                ≡⟨ cong (λ t → t ++ᵗ u) (sym (++ᵗ-assoc (reverse v) _ w₀)) ⟩
              ((reverse v ++ᵗ reverse w₀) ++ᵗ w₀) ++ᵗ u
                ≡⟨ ++ᵗ-assoc _ w₀ u ⟩
              (reverse v ++ᵗ reverse w₀) ++ᵗ (w₀ ++ᵗ u)
                ∎

      calc₂ = ((reverse v ++ᵗ reverse w₀ ++ᵗ w₀) ++ᵗ u) ++ᵗ w₁ ++ᵗ reverse w₁
                ≡⟨ cong (λ w → w ++ᵗ w₁ ++ᵗ (reverse w₁)) calc₁ ⟩
              ((reverse v ++ᵗ reverse w₀) ++ᵗ (w₀ ++ᵗ u)) ++ᵗ w₁ ++ᵗ reverse w₁
                ≡⟨ ++ᵗ-assoc (reverse v ++ᵗ reverse w₀) (w₀ ++ᵗ u) (w₁ ++ᵗ reverse w₁) ⟩
               (reverse v ++ᵗ reverse w₀) ++ᵗ (w₀ ++ᵗ u) ++ᵗ w₁ ++ᵗ reverse w₁
                ∎

      p₆ : P ((reverse v ++ᵗ reverse w₀) ++ᵗ ((w₀ ++ᵗ u) ++ᵗ w₁ ++ᵗ reverse w₁))
      p₆ = subst P calc₂ p₅

      p₇ : P (((w₀ ++ᵗ u) ++ᵗ w₁ ++ᵗ reverse w₁) ++ᵗ reverse v ++ᵗ reverse w₀)
      p₇ = rc (reverse v ++ᵗ reverse w₀) _ p₆

      calc₃ = reverse w₁ ++ᵗ reverse v ++ᵗ reverse w₀
                ≡⟨ cong (reverse w₁ ++ᵗ_) (sym (reverse-++ᵗ w₀ v)) ⟩
              reverse w₁ ++ᵗ reverse (w₀ ++ᵗ v)
                ≡⟨ sym (reverse-++ᵗ (w₀ ++ᵗ v) w₁) ⟩
              reverse ((w₀ ++ᵗ v) ++ᵗ w₁)
                ≡⟨ cong reverse (++ᵗ-assoc w₀ v w₁) ⟩
              reverse (w₀ ++ᵗ v ++ᵗ w₁)
                ∎

      calc₄ = ((w₀ ++ᵗ u) ++ᵗ w₁ ++ᵗ reverse w₁) ++ᵗ reverse v ++ᵗ reverse w₀
                ≡⟨ cong (λ t → t ++ᵗ reverse v ++ᵗ reverse w₀)
                   (sym (++ᵗ-assoc (w₀ ++ᵗ u) w₁ (reverse w₁))) ⟩
              (((w₀ ++ᵗ u) ++ᵗ w₁) ++ᵗ reverse w₁) ++ᵗ reverse v ++ᵗ reverse w₀
                ≡⟨ ++ᵗ-assoc ((w₀ ++ᵗ u) ++ᵗ w₁) (reverse w₁) _ ⟩
              ((w₀ ++ᵗ u) ++ᵗ w₁) ++ᵗ reverse w₁ ++ᵗ reverse v ++ᵗ reverse w₀
                ≡⟨ cong (λ t → t ++ᵗ _) (++ᵗ-assoc w₀ u w₁) ⟩
              (w₀ ++ᵗ u ++ᵗ w₁) ++ᵗ (reverse w₁ ++ᵗ reverse v ++ᵗ reverse w₀)
                ≡⟨ cong ((w₀ ++ᵗ u ++ᵗ w₁) ++ᵗ_) calc₃ ⟩
              (w₀ ++ᵗ u ++ᵗ w₁) ++ᵗ reverse (w₀ ++ᵗ v ++ᵗ w₁)
                ∎

      p₈ : P ((w₀ ++ᵗ u ++ᵗ w₁) ++ᵗ reverse (w₀ ++ᵗ v ++ᵗ w₁))
      p₈ = subst P calc₄ p₇
      -- This is, by definition, what we need for congruence closure...

    -- ... and thus, we finally get (outside the above auxiliary module):
    congr-closed : ⇔*isCongrClosed
    congr-closed w₀ u v w₁ α = (inj (congClosedPreparation.p₈ w₀ u v w₁ α)) ∷ᵗ []ᵗ

    cancels-empty : cancelsEmpty poly
    cancels-empty u u≡0 = inj (subst P (sym ++ᵗ[]ᵗ) (ef u≡0)) ∷ᵗ []ᵗ

    cancels-rinv : cancels*RInv poly
    cancels-rinv u = inj (subst P (sym ++ᵗ[]ᵗ) (ic u)) ∷ᵗ []ᵗ
    -- An alternative would have been to just use ⇔*-to-⇒.

    -- Finally, we can construct the homotopy basis:
    basis : hasHomotopyBasis poly
    basis = Noeth×WB×Congr×Cancel⇒Basis poly
              ord
              ord-is-noether
              ord-has-WB
              congr-closed
              cancels-empty
              cancels-rinv

    {-
      ############################################
      #   Using the constructed homotopy basis,  #
      #   we can show the induction principle    #
      ############################################
    -}

    induction-for-closed-zigzags : ∀ {x} (u : x ↭* x) → P u
    induction-for-closed-zigzags u = p⟨u⟩ where

      -- small trick: instead of calling `basis u []ᵗ`, we call
      -- `basis []ᵗ (reverse u)`. It's counter-intuitive, but it
      -- computes better.
      p⟨revrev⟨u⟫ : P (reverse (reverse u))
      p⟨revrev⟨u⟫ = ⇔*-to-⇒ (basis []ᵗ (reverse u))

      p⟨u⟩ : P u
      p⟨u⟩ = subst P (reverse-reverse u) p⟨revrev⟨u⟫