{-# OPTIONS --without-K --safe #-}

module Lib where

open import Data.Empty public
open import Data.Unit using (⊤; tt) public
open import Data.Sum using (_⊎_; inj₁; inj₂) public
open import Data.Maybe using (Maybe; just; nothing) public
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤?_; _≤_; _<_) renaming (_⊔_ to max) public
open import Data.Nat.Induction
open import Data.Nat.Properties
open import Data.Product using (Σ; ∃; ∃₂; _×_; _,_; -,_; proj₁; proj₂) public
open import Data.List using (List; []; _∷_; _++_) public
open import Data.List.Properties
open import Data.List.Relation.Unary.Any using (here; there; _─_) public
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Relation.Unary.All using (All; []; _∷_) public
open import Data.List.Membership.Propositional hiding (_─_; find) public
open import Data.List.Relation.Binary.Sublist.Propositional using ([]; _∷_; _∷ʳ_; _⊆_; ⊆-refl; ⊆-trans) public

open import Induction.WellFounded as Wf
open import Relation.Nullary using (¬_; yes; no) public
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst; subst₂; module ≡-Reasoning) public

import Data.Fin
import Relation.Binary.Reasoning.Base.Triple as Triple

module L    = Data.List
module All′ = Data.List.Relation.Unary.All
module F    = Data.Fin
open _≤_ public

pattern rhere = here refl
pattern 1+ x = there x
pattern 0d = rhere
pattern 1d = 1+ 0d
pattern 2d = 1+ 1d
pattern 3d = 1+ 2d

module _ {a} {A : Set a} where

  private
    variable
      b c     : A
      l l′ l″ : List A

  ∈-⊆ : b ∈ l → l ⊆ l′ → b ∈ l′
  ∈-⊆ b∈l (y ∷ʳ l⊆l′)        = there (∈-⊆ b∈l l⊆l′)
  ∈-⊆ (here refl) (x ∷ l⊆l′) = here x
  ∈-⊆ (there b∈l) (x ∷ l⊆l′) = there (∈-⊆ b∈l l⊆l′)

  ∈-⊆-trans : ∀ (b∈l : b ∈ l) (l⊆l′ : l ⊆ l′) (l′⊆l″ : l′ ⊆ l″) →
                ∈-⊆ (∈-⊆ b∈l l⊆l′) l′⊆l″ ≡ ∈-⊆ b∈l (⊆-trans l⊆l′ l′⊆l″)
  ∈-⊆-trans b∈l (y ∷ʳ l⊆l′) (z ∷ʳ l′⊆l″)          = cong there (∈-⊆-trans b∈l (y ∷ʳ l⊆l′) l′⊆l″)
  ∈-⊆-trans b∈l (y ∷ʳ l⊆l′) (x ∷ l′⊆l″)           = cong there (∈-⊆-trans b∈l l⊆l′ l′⊆l″)
  ∈-⊆-trans b∈l (x ∷ l⊆l′) (y ∷ʳ l′⊆l″)           = cong there (∈-⊆-trans b∈l (x ∷ l⊆l′) l′⊆l″)
  ∈-⊆-trans (here refl) (refl ∷ l⊆l′) (z ∷ l′⊆l″) = refl
  ∈-⊆-trans (there b∈l) (x ∷ l⊆l′) (z ∷ l′⊆l″)    = cong there (∈-⊆-trans b∈l l⊆l′ l′⊆l″)

  ⊆-refl-trans : ∀ (l⊆l′ : l ⊆ l′) → ⊆-trans ⊆-refl l⊆l′ ≡ l⊆l′
  ⊆-refl-trans []                  = refl
  ⊆-refl-trans {[]} (y ∷ʳ l⊆l′)    = cong (y ∷ʳ_) (⊆-refl-trans l⊆l′)
  ⊆-refl-trans {x ∷ l} (y ∷ʳ l⊆l′) = cong (y ∷ʳ_) (⊆-refl-trans l⊆l′)
  ⊆-refl-trans (x ∷ l⊆l′)          = cong (x ∷_) (⊆-refl-trans l⊆l′)

  ⊆-trans-refl : ∀ (l⊆l′ : l ⊆ l′) → ⊆-trans l⊆l′ ⊆-refl ≡ l⊆l′
  ⊆-trans-refl []            = refl
  ⊆-trans-refl (y ∷ʳ l⊆l′)   = cong (y ∷ʳ_) (⊆-trans-refl l⊆l′)
  ⊆-trans-refl (refl ∷ l⊆l′) = cong (refl ∷_) (⊆-trans-refl l⊆l′)

  ⊆-trans-∷ʳ-refl : ∀ b (l⊆l′ : l ⊆ l′) → ⊆-trans l⊆l′ (b ∷ʳ ⊆-refl) ≡ b ∷ʳ l⊆l′
  ⊆-trans-∷ʳ-refl b []            = refl
  ⊆-trans-∷ʳ-refl b (y ∷ʳ l⊆l′)   = cong (λ l → b ∷ʳ (y ∷ʳ l)) (⊆-trans-refl l⊆l′)
  ⊆-trans-∷ʳ-refl b (refl ∷ l⊆l′) = cong (λ l → b ∷ʳ (refl ∷ l)) (⊆-trans-refl l⊆l′)

  ∈-⊆-refl : ∀ (b∈l : b ∈ l) → ∈-⊆ b∈l ⊆-refl ≡ b∈l
  ∈-⊆-refl {l = x ∷ l} (here refl) = refl
  ∈-⊆-refl {l = x ∷ l} (there b∈l) = cong there (∈-⊆-refl b∈l)

  infixr  _++ˡ_ _++ʳ_
  infixl  _++ʳ′_

  _++ˡ_ : ∀ l → l′ ⊆ l″ → l ++ l′ ⊆ l ++ l″
  [] ++ˡ l′⊆l″      = l′⊆l″
  (x ∷ l) ++ˡ l′⊆l″ = refl ∷ (l ++ˡ l′⊆l″)

  _++ʳ_ : ∀ l → l′ ⊆ l″ → l′ ⊆ l ++ l″
  [] ++ʳ l′⊆l″      = l′⊆l″
  (x ∷ l) ++ʳ l′⊆l″ = x ∷ʳ (l ++ʳ l′⊆l″)

  _++ʳ′_ : l′ ⊆ l″ → ∀ l → l′ ++ l ⊆ l″ ++ l
  [] ++ʳ′ l = ⊆-refl
  (x ∷ʳ l′⊆l″) ++ʳ′ l = x ∷ʳ (l′⊆l″ ++ʳ′ l)
  (eq ∷ l′⊆l″) ++ʳ′ l = eq ∷ (l′⊆l″ ++ʳ′ l)


  ⊆ʳ : ∀ (l l′ : List A) → l′ ⊆ l ++ l′
  ⊆ʳ [] l′      = ⊆-refl
  ⊆ʳ (x ∷ l) l′ = x ∷ʳ ⊆ʳ l l′

  ⊆-++ʳ : ∀ (l⊆l′ : l ⊆ l′) (l′⊆l″ : l′ ⊆ l″) l‴ → ⊆-trans l⊆l′ (l‴ ++ʳ l′⊆l″) ≡ l‴ ++ʳ ⊆-trans l⊆l′ l′⊆l″
  ⊆-++ʳ l⊆l′ l′⊆l″ []              = refl
  ⊆-++ʳ [] l′⊆l″ (x ∷ l‴)          = cong (x ∷ʳ_) (⊆-++ʳ [] l′⊆l″ l‴)
  ⊆-++ʳ (y ∷ʳ l⊆l′) l′⊆l″ (x ∷ l‴) = cong (x ∷ʳ_) (⊆-++ʳ (y ∷ʳ l⊆l′) l′⊆l″ l‴)
  ⊆-++ʳ (y ∷ l⊆l′) l′⊆l″ (x ∷ l‴)  = cong (x ∷ʳ_) (⊆-++ʳ (y ∷ l⊆l′) l′⊆l″ l‴)

  ⊆-++ʳ′ : ∀ (l⊆l′ : l ⊆ l′) l″ → ⊆-trans l⊆l′ (l″ ++ʳ ⊆-refl) ≡ l″ ++ʳ l⊆l′
  ⊆-++ʳ′ l⊆l′ l″
    rewrite ⊆-++ʳ l⊆l′ ⊆-refl l″ = cong (l″ ++ʳ_) (⊆-trans-refl _)

  ⊆-++ʳ-++ˡ : ∀ (l⊆l′ : l ⊆ l′) (l′⊆l″ : l′ ⊆ l″) l‴ → ⊆-trans (l‴ ++ʳ l⊆l′) (l‴ ++ˡ l′⊆l″) ≡ l‴ ++ʳ ⊆-trans l⊆l′ l′⊆l″
  ⊆-++ʳ-++ˡ l⊆l′ l′⊆l″ []       = refl
  ⊆-++ʳ-++ˡ l⊆l′ l′⊆l″ (x ∷ l‴) = cong (x ∷ʳ_) (⊆-++ʳ-++ˡ l⊆l′ l′⊆l″ l‴)

  ∈-⊆-++ : ∀ l‴ (b∈l : b ∈ l) (l⊆l′ : l ⊆ l′) → ∈-⊆ (++⁺ʳ l‴ b∈l) (l‴ ++ˡ l⊆l′) ≡ ++⁺ʳ l‴ (∈-⊆ b∈l l⊆l′)
  ∈-⊆-++ [] b∈l l⊆l′       = refl
  ∈-⊆-++ (c ∷ l‴) b∈l l⊆l′ = cong there (∈-⊆-++ l‴ b∈l l⊆l′)

  ++ˡ-assoc : ∀ l₁ l₂ {l₃ l₄ : List A} (l₃⊆l₄ : l₃ ⊆ l₄) →
    subst₂ _⊆_ (++-assoc l₁ l₂ l₃) (++-assoc l₁ l₂ l₄) ((l₁ ++ l₂) ++ˡ l₃⊆l₄) ≡ l₁ ++ˡ l₂ ++ˡ l₃⊆l₄
  ++ˡ-assoc [] l₂ l₃⊆l₄               = refl
  ++ˡ-assoc (x ∷ l₁) l₂ {l₃} {l₄} l₃⊆l₄
    with (l₁ ++ l₂) ++ l₃ | (l₁ ++ l₂) ++ l₄
       | (l₁ ++ l₂) ++ˡ l₃⊆l₄
       | ++-assoc l₁ l₂ l₃ | ++-assoc l₁ l₂ l₄
       | ++ˡ-assoc l₁ l₂ l₃⊆l₄
  ... | _ | _ | _ | refl | refl | rec = cong (refl ∷_) rec

  ++⁺ʳ-assoc : ∀ l₁ l₂ (b∈l : b ∈ l) → subst (b ∈_) (++-assoc l₁ l₂ l) (++⁺ʳ (l₁ ++ l₂) b∈l) ≡ ++⁺ʳ l₁ (++⁺ʳ l₂ b∈l)
  ++⁺ʳ-assoc [] l₂ b∈l     = refl
  ++⁺ʳ-assoc {l = l} (x ∷ l₁) l₂ b∈l
    with (l₁ ++ l₂)  ++ l | ++⁺ʳ (l₁ ++ l₂) b∈l | ++-assoc l₁ l₂ l | ++⁺ʳ-assoc l₁ l₂ b∈l
  ... | _ | _ | refl | rec = cong there rec

  find : List A → ℕ → Maybe A
  find [] n            = nothing
  find (x ∷ l) zero    = just x
  find (x ∷ l) (suc n) = find l n

  infix  _∶_∈_
  data _∶_∈_ : ℕ → A → List A → Set a where
    here : ∀ {x} →  ∶ x ∈ x ∷ l
    there : ∀ {n x y l} → n ∶ x ∈ l → suc n ∶ x ∈ y ∷ l

  find⇒∈ : ∀ {n} → find l n ≡ just b → n ∶ b ∈ l
  find⇒∈ {[]} ()
  find⇒∈ {x ∷ l} {_} {zero} refl = here
  find⇒∈ {x ∷ l} {_} {suc n} eq  = there (find⇒∈ eq)

  length-∈ : ∀ {a} l → L.length l ∶ a ∈ l ++ a ∷ l′
  length-∈ []      = here
  length-∈ (x ∷ l) = there (length-∈ l)

  split-∈ : ∀ {x a} → x ∶ a ∈ l → ∃₂ λ l′ l″ → l ≡ l′ ++ a ∷ l″ × x ≡ L.length l′
  split-∈ here              = [] , _ , refl , refl
  split-∈ (there a∈l)
    with split-∈ a∈l
  ...  | l′ , l″ , eq , eql = _ ∷ l′ , l″ , cong (_ ∷_) eq , cong suc eql

  ∈-++ʳ : ∀ {x a} → x ∶ a ∈ l → x ∶ a ∈ l ++ l′
  ∈-++ʳ here        = here
  ∈-++ʳ (there a∈l) = there (∈-++ʳ a∈l)

subst₃ : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c} (P : A → B → C → Set ℓ) {x y z u v w} → x ≡ u → y ≡ v → z ≡ w → P x y z → P u v w
subst₃ _ refl refl refl p = p

cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          (f : A → B → C → D) {x y u v w z} → x ≡ y → u ≡ v → w ≡ z → f x u w ≡ f y v z
cong₃ f refl refl refl = refl

≤-diff : ∀ {m n} → m ≤ n → ℕ
≤-diff {_} {n} z≤n = n
≤-diff (s≤s m≤n)   = ≤-diff m≤n

≤-diff-+ : ∀ {m n} (m≤n : m ≤ n) → m + ≤-diff m≤n ≡ n
≤-diff-+ z≤n       = refl
≤-diff-+ (s≤s m≤n) = cong suc (≤-diff-+ m≤n)

ap : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a} → f ≡ g → ∀ a → f a ≡ g a
ap refl a = refl


module Measure {a b ℓ} {A : Set a} {B : Set b} {_≺_ : Rel A ℓ}
               (≺-wf : WellFounded _≺_)
               (m : B → A) where

  open import Level using () renaming (zero to lzero)
  open Wf.Inverse-image {_<_ = _≺_} m using (wellFounded)

  open Wf.All (wellFounded ≺-wf) lzero using (wfRec) public

module <-Measure = Measure <-wellFounded (λ x → x)