{-# 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; []; _∷_; _++_; unzip) 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₂; Reveal_·_is_; inspect; module ≡-Reasoning)
  renaming([_] to insp) 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 5 _++ˡ_ _++ʳ_
  infixl 5 _++ʳ′_

  _++ˡ_ :  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 2 _∶_∈_
  data _∶_∈_ :   A  List A  Set a where
    here :  {x}  0  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

lookup :  {a} {A : Set a}  List A    Maybe A
lookup [] n             = nothing
lookup (x  xs) zero    = just x
lookup (x  xs) (suc n) = lookup xs n

repeat :  {i} {A : Set i}  (A  A)    A  A
repeat f zero x    = x
repeat f (suc n) x = f (repeat f n x)

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)