open import Equivalence

module Chain {a} {A : Set a}
             (_≈_ : A → A → Set a)
             (≈-equiv : IsEquivalence A _≈_)
             (_R_ : A → A → Set a)
             (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where

open import Data.Nat using (ℕ; suc; _+_; _≤_)
open import Data.Nat.Properties using (+-comm; m+1+n≰m)
open import Data.Product using (_×_; Σ; _,_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
open import Data.Empty as Empty using ()

open IsEquivalence ≈-equiv

module _  where

    data Chain : A → A → ℕ → Set a where
        done : ∀ {a a' : A} → a ≈ a' → Chain a a' 0
        step : ∀ {a₁ a₂ a₂' a₃ : A} {n : ℕ} → a₁ R a₂ → a₂ ≈ a₂' → Chain a₂' a₃ n → Chain a₁ a₃ (suc n)

    Chain-≈-cong₁ : ∀ {a₁ a₁' a₂} {n : ℕ} → a₁ ≈ a₁' → Chain a₁ a₂ n → Chain a₁' a₂ n
    Chain-≈-cong₁ a₁≈a₁' (done a₁≈a₂) = done (≈-trans (≈-sym a₁≈a₁') a₁≈a₂)
    Chain-≈-cong₁ a₁≈a₁' (step a₁Ra a≈a' a'a₂) = step (R-≈-cong a₁≈a₁' ≈-refl a₁Ra) a≈a' a'a₂

    Chain-≈-cong₂ : ∀ {a₁ a₂ a₂'} {n : ℕ} → a₂ ≈ a₂' → Chain a₁ a₂ n → Chain a₁ a₂' n
    Chain-≈-cong₂ a₂≈a₂' (done a₁≈a₂) = done (≈-trans a₁≈a₂ a₂≈a₂')
    Chain-≈-cong₂ a₂≈a₂' (step a₁Ra a≈a' a'a₂) = step a₁Ra a≈a' (Chain-≈-cong₂ a₂≈a₂' a'a₂)

    concat : ∀ {a₁ a₂ a₃ : A} {n₁ n₂ : ℕ} → Chain a₁ a₂ n₁ → Chain a₂ a₃ n₂ → Chain a₁ a₃ (n₁ + n₂)
    concat (done a₁≈a₂) a₂a₃ = Chain-≈-cong₁ (≈-sym a₁≈a₂) a₂a₃
    concat (step a₁Ra a≈a' a'a₂) a₂a₃ = step a₁Ra a≈a' (concat a'a₂ a₂a₃)

    empty-≡ : ∀ {a₁ a₂ : A} → Chain a₁ a₂ 0 → a₁ ≈ a₂
    empty-≡ (done a₁≈a₂) = a₁≈a₂

    Bounded : ℕ → Set a
    Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound

    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → Empty.⊥
    Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
        where
            n+1≤n : n + 1 ≤ n
            n+1≤n rewrite (+-comm n 1) = bounded c

    record Height (height : ℕ) : Set a where
        field
            ⊥ : A
            ⊤ : A

            longestChain : Chain ⊥ ⊤ height
            bounded : Bounded height