module Miscellaneous where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; cong; subst; _≗_)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
  -- We don't use the library version of ≤-<-connex 
  using (n≤0⇒n≡0; ≤-refl; ≤-trans; <-trans; <-irrefl; <⇒≤; ≤-pred; <-transˡ; <-transʳ; 
        m≤n⇒m<n∨m≡n; _≤?_; _≟_; ≰⇒>; ≮⇒≥; <⇒≱; n≤1+n; ≤-antisym; +-identityʳ; +-suc)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_; _⊆_; _≐_; Satisfiable; Decidable)
open import Function using (_∘_; id)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_; _++_; length)

private
  variable
    A B C D : Set

Nonempty : List A → Set
-- Nonempty xs = ¬ xs ≡ []
Nonempty [] = ⊥
Nonempty (_ ∷ _) = ⊤

data _elem_ : A → List A → Set where
  here : {x : A} {xs : List A} → x elem (x ∷ xs)
  there : {x y : A} {xs : List A} → x elem xs → x elem (y ∷ xs)

elem-nonempty : {a : A} {xs : List A} → a elem xs → Nonempty xs
elem-nonempty here = tt
elem-nonempty (there h) = tt

nonempty-elem : {xs : List A} → Nonempty xs → Satisfiable (_elem xs)
nonempty-elem {xs = x ∷ xs} h = x , here

nonempty-cons : {xs : List A} → Nonempty xs → 
  ∃₂ λ x xs₁ → xs ≡ (x ∷ xs₁)
nonempty-cons {xs = x ∷ xs₁} h = x , xs₁ , refl

just≢nothing : {x : A} → just x ≢ nothing
just≢nothing ()

infixr  _⇔_
_⇔_ : Set → Set → Set
A ⇔ B = (A → B) × (B → A)

--- !! Rename either Nonempty or NonEmpty !!
-- Use Satisfiable instead.
-- NonEmpty : {A : Set} → (A → Set) → Set
-- -- NonEmpty P = ∃[ x ] P x
-- NonEmpty S = ∃[ x ] x ∈ S

-- image of S under f
_[_] : (A → B) → (A → Set) → B → Set
f [ S ] = λ y → ∃[ x ] (x ∈ S × f x ≡ y)

∘-assoc : (f : A → B) (g : B → C) (h : C → D) → (h ∘ g) ∘ f ≗ h ∘ (g ∘ f)
∘-assoc f g h x = refl

module _ (f : A → B) (S : A → Set) where

  member-image : {x : A} → x ∈ S → f x ∈ f [ S ]
  member-image {x} x∈S = x , x∈S , refl

  -- nonempty-image : NonEmpty S → NonEmpty (f [ S ])
  nonempty-image : Satisfiable S → Satisfiable (f [ S ])
  nonempty-image (x , x∈S) = f x , member-image x∈S

⊎-¬ˡ : A ⊎ B → ¬ A → B
⊎-¬ˡ (inj₁ x) h = ⊥-elim (h x)
⊎-¬ˡ (inj₂ y) h = y

⊎-¬ʳ : A ⊎ B → ¬ B → A
⊎-¬ʳ (inj₁ x) h = x
⊎-¬ʳ (inj₂ y) h = ⊥-elim (h y)

¬∃⟶∀¬ : {A : Set} {B : A → Set} → ¬ (Σ[ x ∈ A ] B x) → ∀ (x : A) → ¬ B x
¬∃⟶∀¬ ¬∃ x Bx = ¬∃ (x , Bx)

module _ (P : ℕ → Set) where

  Infinite : Set
  Infinite = (n : ℕ) → Σ[ m ∈ ℕ ] (n < m × P m)

  Cofinite : Set
  Cofinite = Σ[ n ∈ ℕ ] ((m : ℕ) → n < m → P m)

Finite : (ℕ → Set) → Set
Finite P = Cofinite (¬_ ∘ P)

Coinfinite : (ℕ → Set) → Set
Coinfinite P = Infinite (¬_ ∘ P)

≤-suc : {m n : ℕ} → m ≤ suc n → (m ≤ n ⊎ m ≡ suc n)
≤-suc {zero} {n} _ = inj₁ z≤n
≤-suc {suc m} {zero} (s≤s h) = inj₂ (cong suc (n≤0⇒n≡0 h))
≤-suc {suc m} {suc n} (s≤s h) with ≤-suc {m} {n} h
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ m≡1+n = inj₂ (cong suc m≡1+n)

-- n<⇒suc : {n m : ℕ} → n < m → ∃ (λ k → m ≡ suc k)
-- n<⇒suc {n} {suc m} (s≤s n<m) = m , refl

m≤n⇒∃[o]o+m≡n : {m n : ℕ} → m ≤ n → ∃[ o ] o + m ≡ n
m≤n⇒∃[o]o+m≡n {.zero} {n} z≤n = n , +-identityʳ n
m≤n⇒∃[o]o+m≡n {suc m} {suc n} (s≤s m≤n) with m≤n⇒∃[o]o+m≡n {m} {n} m≤n
... | o , o+m≡n = o , trans (+-suc o m) (cong suc o+m≡n)


m<n⇒∃[o]o+suc[m]≡n : {m n : ℕ} → m < n → ∃[ o ] o + suc m ≡ n
m<n⇒∃[o]o+suc[m]≡n {m} {suc n} (s≤s m≤n) with m≤n⇒∃[o]o+m≡n {m} {n} m≤n
... | o , o+m≡n = o , trans (+-suc o m) (cong suc o+m≡n)

≤-<-connex : (m n : ℕ) → m ≤ n ⊎ n < m
≤-<-connex zero n = inj₁ z≤n
≤-<-connex (suc m) zero = inj₂ (s≤s z≤n)
≤-<-connex (suc m) (suc n) with ≤-<-connex m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n<m = inj₂ (s≤s n<m)

≤-<-connex-≤ : (m n : ℕ) → (m≤n : m ≤ n) → ≤-<-connex m n ≡ inj₁ m≤n
≤-<-connex-≤ zero n z≤n = refl
≤-<-connex-≤ (suc m) (suc n) (s≤s m≤n) rewrite ≤-<-connex-≤ m n m≤n = refl

≤-<-connex-> : (m n : ℕ) → (n<m : n < m) → ≤-<-connex m n ≡ inj₂ n<m
≤-<-connex-> (suc m) zero (s≤s z≤n) = refl
≤-<-connex-> (suc m) (suc n) (s≤s n<m) rewrite ≤-<-connex-> m n n<m = refl

1+n∸n≡1 : (n : ℕ) → suc n ∸ n ≡ 
1+n∸n≡1 zero = refl
1+n∸n≡1 (suc n) = 1+n∸n≡1 n

case₃-⊎ : {A B C D : Set} → (A → D) → (B → D) → (C → D) → (A ⊎ B ⊎ C) → D
case₃-⊎ f g h = case-⊎ f (case-⊎ g h)

i<j-cmp : (i j n : ℕ) → i < j → ((i ≤ n × j ≤ n) ⊎ (i ≤ n × n < j) ⊎ (n < i × n < j))
i<j-cmp i j n i<j = case-⊎ (λ j≤n → inj₁ ((<⇒≤ (<-transˡ i<j j≤n)) , j≤n)) 
                           (λ n<j → case-⊎ (λ i≤n → inj₂ (inj₁ (i≤n , n<j))) 
                                           (λ n<i → inj₂ (inj₂ (n<i , n<j))) 
                                           (≤-<-connex i n))
                           (≤-<-connex j n)

module _ {A : Set} (f g : ℕ → A) where

  switch : ℕ → ℕ → A
  switch n x = case-⊎ (λ n≤x → g x) (λ x<n → f x) (≤-<-connex n x)

  switch-< : (n x : ℕ) → x < n → switch n x ≡ f x
  switch-< n x x<n rewrite ≤-<-connex-> n x x<n = refl

  switch-≥ : (n x : ℕ) → n ≤ x → switch n x ≡ g x
  switch-≥ n x x≥n rewrite ≤-<-connex-≤ n x x≥n = refl

  switch′ : ℕ → ℕ → A
  switch′ n x = case-⊎ (λ x≤n → f x) (λ n<x → g x) (≤-<-connex x n)

  switch′-≤ : (n x : ℕ) → x ≤ n → switch′ n x ≡ f x
  switch′-≤ n x x≤n rewrite ≤-<-connex-≤ x n x≤n = refl

  switch′-> : (n x : ℕ) → n < x → switch′ n x ≡ g x
  switch′-> n x n<x rewrite ≤-<-connex-> x n n<x = refl

Increasing : (A → A → Set) → (ℕ → A) → Set
Increasing _≼_ f = (m n : ℕ) → m < n → f m ≼ f n

step-increasing : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) → Increasing _<_ f
step-increasing f f-step m (suc n) m<1+n with ≤-suc m<1+n
... | inj₁ m<n = <-trans (step-increasing f f-step m n m<n) (f-step n)
... | inj₂ refl = f-step m

subseq-increasing : (_≼_ : A → A → Set) (f : ℕ → A) (r : ℕ → ℕ) 
  → Increasing _≼_ f
  → Increasing _<_ r
  ------------------------
  → Increasing _≼_ (f ∘ r)
subseq-increasing _≼_ f r f-increasing r-increasing m n m<n
  = f-increasing (r m) (r n) (r-increasing m n m<n)

id-increasing : Increasing _<_ id
id-increasing m n m<n = m<n

compose-increasing : 
  {f g : ℕ → ℕ} → Increasing _<_ f → Increasing _<_ g →
  Increasing _<_ (g ∘ f)
compose-increasing {f} {g} f-increasing g-increasing m n m<n = g-increasing (f m) (f n) (f-increasing m n m<n)

-- compose-increasing : 

module _ (f : ℕ → ℕ) (f-increasing : Increasing _<_ f) where

  increasing-≤ : (m n : ℕ) → m ≤ n → f m ≤ f n
  increasing-≤ m n m≤n = case-⊎ (λ m<n → <⇒≤ (f-increasing m n m<n)) 
                                    (λ {refl → ≤-refl})
                                    (m≤n⇒m<n∨m≡n m≤n)

  inverse-increasing : {m n : ℕ} → f m < f n → m < n
  inverse-increasing {m} {n} h = ≰⇒> n≰m
    where
    n≰m : ¬ (n ≤ m)
    n≰m n≤m = <⇒≱ h (increasing-≤ n m n≤m)

  inverse-nondecreasing : {m n : ℕ} → f m ≤ f n → m ≤ n
  inverse-nondecreasing {m} {n} h = ≮⇒≥ n≮m
    where
    n≮m : ¬ (n < m)
    n≮m n<m = <⇒≱ (f-increasing n m n<m) h

  increasing⇒injective : {m n : ℕ} → f m ≡ f n → m ≡ n
  increasing⇒injective {m} {n} h = ≤-antisym (≮⇒≥ n≮m) (≮⇒≥ m≮n)
    where
    f[m]≮f[n] : ¬ (f m < f n)
    f[m]≮f[n] = <-irrefl h
    m≮n : ¬ (m < n)
    m≮n m<n = f[m]≮f[n] (f-increasing m n m<n)
    f[n]≮f[m] : ¬ (f n < f m)
    f[n]≮f[m] = <-irrefl (sym h)
    n≮m : ¬ (n < m)
    n≮m n<m = f[n]≮f[m] (f-increasing n m n<m)
  
  increasing⇒expansive : (n : ℕ) →  n ≤ f n
  increasing⇒expansive zero = z≤n
  increasing⇒expansive (suc n) = 
    ≤-trans (s≤s (increasing⇒expansive n)) 
            (f-increasing n (suc n) ≤-refl)

  -- min[n≤f] n is the least m s.t. n ≤ f m
  min[n≤f] : ℕ → ℕ
  min[n≤f]  = 
  min[n≤f] (suc n) with f (min[n≤f] n) ≤? n
  ... | no ¬p = min[n≤f] n
  ... | yes p = suc (min[n≤f] n)

  min[n≤f]-spec₁ : (n : ℕ) → n ≤ f (min[n≤f] n)
  min[n≤f]-spec₁ zero = z≤n
  min[n≤f]-spec₁ (suc n) with f (min[n≤f] n) ≤? n
  ... | no ¬p = ≰⇒> ¬p
  ... | yes p = ≤-trans (s≤s (min[n≤f]-spec₁ n)) [1]
    where
    [1] : f (min[n≤f] n) < f (suc (min[n≤f] n))
    [1] = f-increasing (min[n≤f] n) (suc (min[n≤f] n)) ≤-refl

  min[n≤f]-spec₂ : (n m : ℕ) → n ≤ f m → min[n≤f] n ≤ m
  min[n≤f]-spec₂ zero m n≤f[m] = z≤n
  min[n≤f]-spec₂ (suc n) m 1+n≤f[m] with f (min[n≤f] n) ≤? n
  ... | no ¬p = min[n≤f]-spec₂ n m (≤-trans (n≤1+n n) 1+n≤f[m])
  ... | yes p = [2]
    where
    [1] : f (min[n≤f] n) < f m
    [1] = <-transʳ p 1+n≤f[m]
    [2] : min[n≤f] n < m
    [2] = inverse-increasing [1]

  min[n≤f]-spec₃ : (n : ℕ) → min[n≤f] (f n) ≡ n
  min[n≤f]-spec₃ n = ≤-antisym [1] [3]
    where
    [1] : min[n≤f] (f n) ≤ n
    [1] = min[n≤f]-spec₂ (f n) n ≤-refl
    [2] : f n ≤ f (min[n≤f] (f n))
    [2] = min[n≤f]-spec₁ (f n)
    [3] : n ≤ min[n≤f] (f n)
    [3] =  inverse-nondecreasing [2]

  increasing-range : ℕ → Set
  increasing-range n = n ≡ f (min[n≤f] n)

  increasing-range-spec : increasing-range ≐ λ n → ∃[ i ] f i ≡ n
  increasing-range-spec = ⟨⊆⟩ , ⟨⊇⟩
    where
    ⟨⊆⟩ : increasing-range ⊆ λ n → ∃[ i ] f i ≡ n
    ⟨⊆⟩ {x = n} h = min[n≤f] n , sym h
    ⟨⊇⟩ : (λ n → ∃[ i ] f i ≡ n) ⊆ increasing-range
    ⟨⊇⟩ {x = n} (i , refl) = [5]  -- f i ≡ n
      where
      [1] : n ≤ f (min[n≤f] n)
      [1] = min[n≤f]-spec₁ n
      [2] : n ≤ f i
      [2] = ≤-refl
      [3] : min[n≤f] n ≤ i
      [3] = min[n≤f]-spec₂ n i [2]
      [4] : f (min[n≤f] n) ≤ n
      [4] = increasing-≤ (min[n≤f] n) i [3]
      [5] : n ≡ f (min[n≤f] n)
      [5] = ≤-antisym [1] [4]

  increasing-range? : Decidable increasing-range
  increasing-range? n = n ≟ _

  inverse : (i : ℕ) → ∃[ x ] f x ≡ i → ℕ
  inverse i h = proj₁ h

  inverse-spec₁ : (x : ℕ) → inverse (f x) (x , refl) ≡ x
  inverse-spec₁ x = refl

  inverse-spec₂ : (i : ℕ) (h : ∃[ x ] f x ≡ i) → f (inverse i h) ≡ i
  inverse-spec₂ i h = proj₂ h


All : (A → Set) → (ℕ → A) → Set
All P f = (n : ℕ) → P (f n)

all-compose : {A : Set} {P : A → Set} {f : ℕ → A} (r : ℕ → ℕ) →
  All P f → All P (f ∘ r)
all-compose r h n = h (r n)

all-extensional : {A : Set} {P : A → Set} {f g : ℕ → A} → f ≗ g → 
                  All P f → All P g
all-extensional {P = P} f≗g h n = subst P (f≗g n) (h n)

AgreeUpTo : {A : Set} → ℕ → (ℕ → A) → (ℕ → A) → Set
AgreeUpTo n f g = {m : ℕ} → m ≤ n → f m ≡ g m

agreeUpTo-≤ : {A : Set} {n m : ℕ} {f g : ℕ → A}
  → AgreeUpTo n f g
  → m ≤ n
  -----------------
  → AgreeUpTo m f g
agreeUpTo-≤ h m≤n x≤m = h (≤-trans x≤m m≤n)

agreeUpTo-reflexive : {A : Set} (n : ℕ) (f : ℕ → A) → AgreeUpTo n f f
agreeUpTo-reflexive n f _ = refl

agreeUpTo-symmetric : {A : Set} (n : ℕ) (f g : ℕ → A) → AgreeUpTo n f g → AgreeUpTo n g f
agreeUpTo-symmetric n f g h x≤n = sym (h x≤n)

agreeUpTo-transitive : {A : Set} {n : ℕ} {f : ℕ → A} {g : ℕ → A} {k : ℕ → A}
  → AgreeUpTo n f g
  → AgreeUpTo n g k
  -----------------
  → AgreeUpTo n f k
agreeUpTo-transitive hfg hgk m≤n = trans (hfg m≤n) (hgk m≤n)

InitialSegmentProperty : {A : Set} (P : (ℕ → A) → Set) → Set
InitialSegmentProperty {A} P = (f : ℕ → A) → ((n : ℕ) → ∃[ g ] (g ∈ P × AgreeUpTo n f g)) → f ∈ P

ISP-closed-∩ : {A : Set} (P Q : (ℕ → A) → Set)
  → InitialSegmentProperty P
  → InitialSegmentProperty Q
  ------------------------------------------
  → InitialSegmentProperty (λ f → f ∈ P × f ∈ Q)
ISP-closed-∩ P Q P-isp Q-isp f h = 
  P-isp f (λ n → proj₁ (h n) , proj₁ (proj₁ (proj₂ (h n))) , proj₂ (proj₂ (h n))) , 
  Q-isp f (λ n →  proj₁ (h n) , proj₂ (proj₁ (proj₂ (h n))) , proj₂ (proj₂ (h n)))

TermByTerm : {A B : Set} (R : A → B → Set) → (ℕ → A) → (ℕ → B) → Set
TermByTerm R f g = (n : ℕ) → R (f n) (g n)

Sub : {A B : Set} → (A → B → Set) → (ℕ → B) → (ℕ → A) → Set
Sub R f g = Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × TermByTerm R g (f ∘ r))

equiv-Sub : {A B : Set} (R : A → B → Set) → 
            (f : ℕ → B) (g : ℕ → A) → Sub R f g → 
            (∀ i → Satisfiable (λ x → R x (f i))) →
            (Σ[ g′ ∈ (ℕ → A) ] TermByTerm R g′ f × Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × ((x : ℕ) → g′ (r x) ≡ g x)))
equiv-Sub R f g (r , r-increasing , h₁) h = g′ , [4] , r ,  r-increasing , g′∘r≗g
  where
  r⁻¹ = inverse r r-increasing
  r⁻¹-spec₁ : (i : ℕ) → r⁻¹ (r i) (i , refl) ≡ i
  r⁻¹-spec₁ = inverse-spec₁ r r-increasing
  r⁻¹-spec₂ : (i : ℕ) (h′ : ∃[ x ] r x ≡ i) → r (r⁻¹ i h′) ≡ i
  r⁻¹-spec₂ = inverse-spec₂ r r-increasing
  k : (i : ℕ) → ∃[ a ] R a (f i)
  k i with increasing-range? r r-increasing i
  ... | no ¬p = [1]
    where
    [1] : ∃[ a ] R a (f i)
    [1] = h i
  ... | yes p = (g (r⁻¹ i [2]) , [3])
    where
    [2] : ∃[ x ] r x ≡ i
    [2] = proj₁ (increasing-range-spec r r-increasing) p
    i′ = r⁻¹ i [2]
    r[i′]≡i : r i′ ≡ i
    r[i′]≡i = r⁻¹-spec₂ i [2]
    [3] : R (g i′) (f i)
    [3] = subst (λ z → R (g i′) (f z)) r[i′]≡i (h₁ i′)
  g′ = proj₁ ∘ k
  [4] : TermByTerm R g′ f
  [4] = proj₂ ∘ k
  g′∘r≗g : ∀ x → g′ (r x) ≡ g x
  g′∘r≗g x = [6]
    where
    [5] : min[n≤f] r r-increasing (r x) ≡ x
    [5] = min[n≤f]-spec₃ r r-increasing x

    [6] : g′ (r x) ≡ g x
    [6] with increasing-range? r r-increasing (r x)
    ... | no ¬p = ⊥-elim (¬p (cong r (sym [5])))
    ... | yes p rewrite r⁻¹-spec₁ x = cong g [5]


Sub-mono : {A B : Set} (_⊑₁_ _⊑₂_ : A → B → Set) (f : ℕ → B)
  → ((x : A) (y : B) → x ⊑₁ y → x ⊑₂ y)
  → (g : ℕ → A)
  → g ∈ Sub _⊑₁_ f
  ------------------
  → g ∈ Sub _⊑₂_ f
Sub-mono _⊑₁_ _⊑₂_ f ⊑₁⇒⊑₂ g (r , r-increasing , h) = 
  r , r-increasing , λ n → ⊑₁⇒⊑₂ (g n) (f (r n)) (h n)