{-
LIST EXTENSION

Our list extension is a variation of Dershowitz and Manna's multiset
extension. The list extension is better behaved in a type theory
setting.
-}


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


open import Cubical.Foundations.Prelude

open import Agda.Primitive
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc;
            Rel to BinRel)
open import Cubical.Data.List.Base
open import Cubical.Data.List.Properties

open import squier.accessibility
open import squier.graphclosures

module squier.listextension {ℓ₀ ℓ₁ : Level}
                            (M : Type ℓ₀) (_<_ : M → M → Type ℓ₁) where

greater-all : (n : M) → (ms : List M) → Type _
greater-all n ms = forall-in-list {ℓ₀ = ℓ₀} (_< n) ms -- ℓ₀ is required

-- Extending a relation < on M to lists on M:
data _<ᴸ_ : List M → List M → Type (ℓ-max ℓ₀ ℓ₁) where
  stp : ∀ {n ns ms} → greater-all n ns → (ns ++ ms) <ᴸ (n ∷ ms)
  add : ∀ {n ns ms} → ms <ᴸ ns → (n ∷ ms) <ᴸ (n ∷ ns)

-- If we know that a list is smaller than another list, we can present
-- it in a certain way:
<ᴸ-presentation : (ms ns : List M) → ms <ᴸ ns
                  → Σ[ ms₁ ∈ List M ]
                     Σ[ ms₂ ∈ List M ]
                     Σ[ ms₃ ∈ List M ]
                     Σ[ n ∈ M ]
                     (ms ≡ ms₁ ++ ms₂ ++ ms₃) × (ns ≡ ms₁ ++ [ n ] ++ ms₃)
<ᴸ-presentation .(ns ++ ms) .(n ∷ ms) (stp {n} {ns} {ms} ga) =
  [] , ns , ms , n , refl , refl
<ᴸ-presentation .(n ∷ ms) .(n ∷ ns) (add {n} {ns} {ms} ms<ns) =
  let
    (ms₁ , ms₂ , ms₃ , n' , p₁ , p₂) = <ᴸ-presentation ms ns ms<ns
  in
    n ∷ ms₁ , ms₂ , ms₃ , n' , cong (λ l → n ∷ l) p₁ , cong (λ l → n ∷ l) p₂

-- We show that wellfoundedness is preserved.
-- The proof is similar to an argument by Tobias Nipkov.

classify-<++ : (ms ns₁ ns₂ : List M) → ms <ᴸ (ns₁ ++ ns₂) →
                 (Σ[ ms₁ ∈ List M ] (ms ≡ ms₁ ++ ns₂) × (ms₁ <ᴸ ns₁)) ⊎
                 (Σ[ ms₂ ∈ List M ] (ms ≡ ns₁ ++ ms₂) × (ms₂ <ᴸ ns₂))
classify-<++ ms [] ns₂ ms<ns₂ = inr (ms , refl , ms<ns₂)
classify-<++ .(ns ++ (ns₁ ++ ns₂))
             (n ∷ ns₁) ns₂ (stp {n} {ns} {.(ns₁ ++ ns₂)} n>ns) =
                 inl ((ns ++ ns₁) , sym (++-assoc ns ns₁ ns₂) , stp n>ns)
classify-<++ .(n ∷ ms) (n ∷ ns₁) ns₂ (add {n} {.(ns₁ ++ ns₂)} {ms} ms<ns₁₊₂)
                 with classify-<++ ms ns₁ ns₂ ms<ns₁₊₂
... | inl (ms₁ , ms≡ms₁ns₂ , ms₁<ns₁) =
                 inl (n ∷ ms₁ , cong  (λ l → n ∷ l) ms≡ms₁ns₂ , add ms₁<ns₁)
... | inr (ms₂ , ms≡ns₁ms₂ , ms₂<ns₂) =
                 inr (ms₂ , cong  (λ l → n ∷ l) ms≡ns₁ms₂ , ms₂<ns₂)

-- The "elimination" form of classify-<++
module _ (Q : List M → Type (ℓ₀ ⊔ ℓ₁)) where
  elim-class-<++ : (ns₁ ns₂ : List M) →
                   ((ns₁' : List M) → ns₁' <ᴸ ns₁ → Q (ns₁' ++ ns₂)) →
                   ((ns₂' : List M) → ns₂' <ᴸ ns₂ → Q (ns₁ ++ ns₂')) →
                   (ms : List M) → (ms <ᴸ (ns₁ ++ ns₂)) → Q ms
  elim-class-<++ ns₁ ns₂ h₁ h₂ ms ms<ns with classify-<++ ms ns₁ ns₂ ms<ns
  ... | inl (ms₁ , ms≡ms₁ns₂ , ms₁<ns₁) = subst Q (sym ms≡ms₁ns₂) (h₁ ms₁ ms₁<ns₁)
  ... | inr (ms₂ , ms≡ns₁ms₂ , ms₂<ns₂) = subst Q (sym ms≡ns₁ms₂) (h₂ ms₂ ms₂<ns₂)

-- A lemma: If ns₁ and ns₂ are both accessible, then ns₁ ++ ns₂ is accessible
isAcc⟨++⟩ : ∀ ms → isAcc _<ᴸ_ ms → ∀ ns → isAcc _<ᴸ_ ns → isAcc _<ᴸ_ (ms ++ ns)
isAcc⟨++⟩ = double-acc-ind _<ᴸ_ _<ᴸ_
                          (λ {(l1 , l2) → isAcc _<ᴸ_ (l1 ++ l2)}) lemma where
  lemma : (ns₁ : List M) → isAcc _<ᴸ_ ns₁ →
          (ns₂ : List M) → isAcc _<ᴸ_ ns₂ →
          ((ms₁ : List M) → ms₁ <ᴸ ns₁ → isAcc _<ᴸ_ (ms₁ ++ ns₂)) →
          ((ms₂ : List M) → ms₂ <ᴸ ns₂ → isAcc _<ᴸ_ (ns₁ ++ ms₂)) →
          isAcc _<ᴸ_ (ns₁ ++ ns₂)
  lemma ns₁ _ ns₂ _ h₁ h₂ =
          acc (λ ms ms<ns₁₂ → elim-class-<++ (isAcc _<ᴸ_) ns₁ ns₂ h₁ h₂ ms ms<ns₁₂)

{- Note for later: where do we even need isAcc⟨ms⟩ and isAcc⟨ns⟩ above? -}

-- predicate: all elements of a list accessible
all-access : (ms : List M) → Type (ℓ₀ ⊔ ℓ₁)
all-access [] = Unit*
all-access (m ∷ ms) = (isAcc _<ᴸ_ [ m ]) × all-access ms

lemma : (n : M) → ((m : M) → m < n → isAcc _<ᴸ_ [ m ])
           → (ms : List M) → greater-all n ms → isAcc _<ᴸ_ ms
lemma _ _ [] _ = acc λ {_ ()}
lemma n h (m ∷ ms) (n>m , n>ms) = isAcc⟨++⟩ [ m ] (h m n>m) ms (lemma n h ms n>ms)

-- Lemma: [ m ] is accessible
isAcc⟨sglt⟩ : ∀ m → isAcc _<_ m → isAcc _<ᴸ_ [ m ]
isAcc⟨sglt⟩ = acc-ind M _<_ (λ n → isAcc _<ᴸ_ [ n ])
                     λ m isAcc⟨m⟩ ih → acc λ {.(ns ++ []) (stp {m} {ns} {[]} m>ns)
                                    → subst (isAcc _<ᴸ_)
                                             (sym (++-unit-r ns))
                                             (lemma m ih ns m>ns)}

-- Theorem: If < is wellfounded, then so is <ᴸ_
isWF⟨<⟩⇒isWF⟨<ᴸ⟩ : isWellFounded _<_ → isWellFounded _<ᴸ_
isWF⟨<⟩⇒isWF⟨<ᴸ⟩ isWF⟨<⟩ [] = acc λ {ms ()}
isWF⟨<⟩⇒isWF⟨<ᴸ⟩ isWF⟨<⟩ (m ∷ ms) =
  isAcc⟨++⟩ [ m ]
            (isAcc⟨sglt⟩ m (isWF⟨<⟩ m))
            ms
            (isWF⟨<⟩⇒isWF⟨<ᴸ⟩ isWF⟨<⟩ ms)

-- Lifting constructor to <ᴸ⁺, i.e. the transitive closure of <ᴸ
open import squier.graphclosures

-- Note that _<ᴸ⁺_ does NOT contain a reflexivity constructor.
private
  _<ᴸ⁺_ = TransClosure _<ᴸ_

add+ : ∀ {n ms ns} → ms <ᴸ⁺ ns → (n ∷ ms) <ᴸ⁺ (n ∷ ns)
add+ ([ ms<ns ]⁺) = [ add ms<ns ]⁺
add+ (ms<ks ∷⁺ ks<⁺ns) = add ms<ks ∷⁺ add+ ks<⁺ns

dda* : ∀ {ms ns ks} → ms <ᴸ ns → (ms ++ ks) <ᴸ (ns ++ ks)
dda* {ms} {ns} {ks} (stp {n₀} {ms₀} {ns₀} all) =
          subst (λ l → l <ᴸ _)
                (sym (++-assoc ms₀ ns₀ ks))
                (stp {n₀} {ms₀} {ns₀ ++ ks} all)
dda* {.(n ∷ ms)} {.(n ∷ ns)} {ks} (add {n} {ns} {ms} ms<ns) =
          add {n} (dda* ms<ns)

-- A useful lemma: We can concanenate with a list without
-- changing the order
cc-r : ∀ {ms ns ks} → ms <ᴸ⁺ ns → (ms ++ ks) <ᴸ⁺ (ns ++ ks)
cc-r [ ms<ns ]⁺ = [ dda* ms<ns ]⁺
cc-r (ms<ms₀ ∷⁺ ms₀<⁺ns) = (dda* ms<ms₀) ∷⁺ (cc-r ms₀<⁺ns)