module Fin where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; s≤s; z≤n; _<_; _⊓_)
open import Data.Nat.Properties
  -- don't use the library version of ≤-<-connex
  -- use m≤n⇒m≤1+n instead of ≤-step
  using (suc-injective; ≤-reflexive; ≤-refl; ≤-trans; <-irrefl; <⇒≤; 
        m≤n⇒m≤1+n; <-transˡ; <-transʳ; 
        ≤∧≢⇒<; +-monoˡ-<; m≤m+n; m≤n+m; m≤n⇒m≤o+n; +-mono-≤; 
        m<n⇒m⊓o<n; m≤n⇒m⊓n≡m; ⊓-comm; -- ≤-total; 
        m⊓n≤m)
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)
open import Function using (_∘_; id)
open import Data.List using (List; []; _∷_; _++_; length; sum; _ʳ++_)
import Data.Fin as F
open F using (Fin; toℕ; fromℕ<)
open import Data.Fin.Properties using 
  (pigeonhole; toℕ-mono-<; toℕ<n; fromℕ<-toℕ; fromℕ<-cong; toℕ-fromℕ<; 
  toℕ-injective; fromℕ<-injective)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Properties using (just-injective)
open import Relation.Binary.Core using (_⇒_)

open import Miscellaneous

-- open import Classical

open import WQO

-- open import MinimalBadSeq

-- import Higman as H

private
  variable
    A : Set
    n : ℕ

module Fin-≡ where
  almostFull : {n : ℕ} → AlmostFull {Fin n} _≡_
  almostFull {n} f = toℕ i , toℕ j , toℕ-mono-< i<j , g[i]≡g[j] -- toℕ-mono-< i<j is not in stdlib 1.7.2
    where
    g : Fin (suc n) → Fin n
    g = f ∘ toℕ
    [1] : ∃₂ (λ i j → i F.< j × g i ≡ g j) -- i ≢ j instead of i < j in stdlib 1.7.1
    [1] = pigeonhole ≤-refl g 
    i = proj₁ [1]
    j = proj₁ (proj₂ [1])
    i<j : i F.< j
    i<j = proj₁ (proj₂ (proj₂ [1]))
    g[i]≡g[j] : g i ≡ g j
    g[i]≡g[j] = proj₂ (proj₂ (proj₂ [1]))

  isWQO : (n : ℕ) → IsWQO {A = Fin n} _≡_
  isWQO n =
    record
    { isQO = record { reflexive = refl ; transitive = trans }
    ; almostFull = almostFull
    }

module _ {n : ℕ} where
  _≤′_ : Maybe (Fin n) → Maybe (Fin n) → Set
  just i ≤′ just j  = i F.≤ j
  just _ ≤′ nothing = ⊥
  nothing ≤′ _ = ⊤
  -- nothing ≤′ just _ = ⊤
  -- nothing ≤′ nothing = ⊤

  ≤′-refl : Reflexive _≤′_
  ≤′-refl {x = just x}  = ≤-refl
  ≤′-refl {x = nothing} = tt

  ≤′-reflexive : _≡_ ⇒ _≤′_
  ≤′-reflexive refl = ≤′-refl

  ≤′-trans : Transitive _≤′_
  ≤′-trans {x = just x}  {y = just y}  {z = just z}  xy yz = ≤-trans xy yz
  ≤′-trans {x = nothing} {y = just y}  {z = just z}  xy yz = tt
  ≤′-trans {x = nothing} {y = nothing} {z = just z}  xy yz = tt
  ≤′-trans {x = nothing} {y = nothing} {z = nothing} xy yz = tt

  ≤′-just-just : (i : Fin n) (m : Maybe (Fin n)) → just i ≤′ m → 
                 ∃[ j ] m ≡ just j
  ≤′-just-just i (just j) h = j , refl

Funny minimum operator on Fin n. This will be used in the definition of min below.

  _⊓′_ : Maybe (Fin n) → Maybe (Fin n) → Maybe (Fin n)
  just i ⊓′ just j = just (fromℕ< (m<n⇒m⊓o<n (toℕ j) (toℕ<n i)))
  just i ⊓′ nothing = just i
  nothing ⊓′ just j = just j
  nothing ⊓′ nothing = nothing

  ⊓′-⊓ : (i j : Fin n) → ∃[ k ] (just i ⊓′ just j) ≡ just k × toℕ k ≡ toℕ i ⊓ toℕ j
  ⊓′-⊓ i j = (fromℕ< (m<n⇒m⊓o<n (toℕ j) (toℕ<n i))) , refl , 
              toℕ-fromℕ< ((m<n⇒m⊓o<n (toℕ j) (toℕ<n i)))

  ⊓′-comm : (x y : Maybe (Fin n)) → x ⊓′ y ≡ y ⊓′ x
  -- ⊓′-comm (just i) (just j) = cong just (fromℕ<-cong (toℕ i ⊓ toℕ j) (toℕ j ⊓ toℕ i) (⊓-comm (toℕ i) (toℕ j)) (m<n⇒m⊓o<n (toℕ j) (toℕ<n i)) (m<n⇒m⊓o<n (toℕ i) (toℕ<n j)))
  ⊓′-comm (just i) (just j) with ⊓′-⊓ i j | ⊓′-⊓ j i
  ... | k , eq₁ , eq₂ | l , eq₃ , eq₄ = trans eq₁ (trans (cong just [3]) (sym eq₃))
    where
    [1] : toℕ k ≡ toℕ j ⊓ toℕ i
    [1] = trans eq₂ (⊓-comm (toℕ i) (toℕ j))

    [2] : toℕ k ≡ toℕ l
    [2] = trans [1] (sym eq₄)

    [3] : k ≡ l
    [3] = toℕ-injective [2]
  ⊓′-comm (just i) nothing = refl
  ⊓′-comm nothing (just j) = refl
  ⊓′-comm nothing nothing = refl

  ≤-⊓′ : {i j : Fin n} → toℕ i ≤ toℕ j → just i ⊓′ just j ≡ just i
  ≤-⊓′ {i} {j} i≤j = [4]
    where
    [1] : toℕ i ⊓ toℕ j ≡ toℕ i
    [1] = m≤n⇒m⊓n≡m i≤j

    [2] : fromℕ< (toℕ<n i) ≡ i
    [2] = fromℕ<-toℕ i (toℕ<n i)

    [3] : fromℕ< (m<n⇒m⊓o<n (toℕ j) (toℕ<n i)) ≡ i
    [3] = trans (fromℕ<-cong (toℕ i ⊓ toℕ j) (toℕ i) [1] (m<n⇒m⊓o<n (toℕ j) (toℕ<n i)) (toℕ<n i)) 
          (fromℕ<-toℕ i (toℕ<n i))

    [4] : just i ⊓′ just j ≡ just i
    [4] = cong just [3]

  ≥-⊓′ : {i j : Fin n} → toℕ j ≤ toℕ i → just i ⊓′ just j ≡ just j
  ≥-⊓′ {i} {j} j≤i = trans (⊓′-comm (just i) (just j)) (≤-⊓′ j≤i)

  ⊓′-≤′₁ : (i j : Fin n) → (just i ⊓′ just j) ≤′ just i
  ⊓′-≤′₁ i j with ⊓′-⊓ i j
  ... | k , eq₁ , eq₂ = [3]
    where
    [1] : toℕ k ≤ toℕ i
    [1] rewrite eq₂ = m⊓n≤m (toℕ i) (toℕ j)

    [2] : just k ≤′ just i
    [2] = [1]

    [3] : (just i ⊓′ just j) ≤′ just i
    [3] = subst (_≤′ just i) (sym eq₁) [2]

  ⊓′-≤′₂ : (i j : Fin n) → (just i ⊓′ just j) ≤′ just j
  ⊓′-≤′₂ i j = subst (_≤′ just j) (⊓′-comm (just j) (just i)) (⊓′-≤′₁ j i)

  ⊓′-≤′₃ : (i : Fin n) (m : Maybe (Fin n)) → (just i ⊓′ m) ≤′ just i
  ⊓′-≤′₃ i (just j) = ⊓′-≤′₁ i j
  ⊓′-≤′₃ i nothing  = ≤-refl

  ⊓′-≤′₄ : (m : Maybe (Fin n)) (j : Fin n) → (m ⊓′ just j) ≤′ just j
  ⊓′-≤′₄ (just i) j = ⊓′-≤′₂ i j
  ⊓′-≤′₄ nothing  j = ≤-refl

  ⊓′-nothing₁ : (m₁ m₂ : Maybe (Fin n)) → (m₁ ⊓′ m₂) ≡ nothing → m₁ ≡ nothing
  ⊓′-nothing₁ (just i) (just j) ()
  ⊓′-nothing₁ (just i) nothing  ()
  ⊓′-nothing₁ nothing  (just j) ()
  ⊓′-nothing₁ nothing  nothing  refl = refl

  ⊓′-nothing₂ : (m₁ m₂ : Maybe (Fin n)) → (m₁ ⊓′ m₂) ≡ nothing → m₂ ≡ nothing
  ⊓′-nothing₂ (just i) (just j) ()
  ⊓′-nothing₂ (just i) nothing  ()
  ⊓′-nothing₂ nothing  (just j) ()
  ⊓′-nothing₂ nothing  nothing  refl = refl

  ⊓′-nothing-just : (m : Maybe (Fin n)) (i : Fin n) → 
    (nothing ⊓′ m) ≡ just i → m ≡ just i
  ⊓′-nothing-just (just i) .i refl = refl

module MaybeFin-≡ {n : ℕ} where
  open M {Fin n} _≡_

  ≡-≼′ : (x y : Maybe (Fin n)) → (x ≡ y) ⇔ (x ≼′ y)
  ≡-≼′ (just x) (just y) = (λ {refl → refl}) , (λ {refl → refl})
  ≡-≼′ (just x) nothing = (λ {()}) , λ {()}
  ≡-≼′ nothing (just y) = (λ {()}) , λ {()}
  ≡-≼′ nothing nothing = (λ {refl → tt}) , λ _ → refl

  almostFull : AlmostFull {Maybe (Fin n)} _≡_
  almostFull f with maybe-almostFull Fin-≡.almostFull f
  ... | i , j , i<j , h = i , j , i<j , proj₂ (≡-≼′ (f i) (f j)) h