{-# OPTIONS --safe #-}

module Problem3 where

open import Data.List
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Empty
open import Data.Nat.Properties using (≤-step; n<1+n; <⇒≢; module ≤-Reasoning)

data _⊑_ {A : Set} : List A → List A → Set where
  ⊑-nil  : [] ⊑ []
  ⊑-cons : ∀{x}{xs ys} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys)
  ⊑-skip : ∀{x}{xs ys} → xs ⊑ ys → xs ⊑ (x ∷ ys)

⊑-refl : ∀{A : Set}(xs : List A) → xs ⊑ xs
⊑-refl []       = ⊑-nil
⊑-refl (x ∷ xs) = ⊑-cons (⊑-refl xs)

-- Induct on the second relation, then the first.
⊑-trans : ∀{A : Set}{xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
⊑-trans xs⊑ys          (⊑-skip ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
⊑-trans ⊑-nil          ⊑-nil          = ⊑-nil
⊑-trans (⊑-cons xs⊑ys) (⊑-cons ys⊑zs) = ⊑-cons (⊑-trans xs⊑ys ys⊑zs)
⊑-trans (⊑-skip xs⊑ys) (⊑-cons ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)

⊑-len : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → length xs ≤ length ys
⊑-len ⊑-nil          = z≤n
⊑-len (⊑-cons xs⊑ys) = s≤s (⊑-len xs⊑ys)
⊑-len (⊑-skip xs⊑ys) = ≤-step (⊑-len xs⊑ys)

∷-injectiveᵣ : {A : Set} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
∷-injectiveᵣ refl = refl

private
  lemma : {A : Set} {w : A} {xs ys zs ws : List A} → xs ≡ w ∷ ws → xs ⊑ ys → ys ≡ zs → zs ⊑ ws → ⊥
  lemma {w = w} {xs} {ys} {zs} {ws} xs≡w∷ws xs⊑ys ys≡zs zs⊑ws = <⇒≢ prf (cong length (xs≡w∷ws))
    where
    open ≤-Reasoning
    prf : length xs < length (w ∷ ws)
    prf = begin-strict
      length xs       ≤⟨ ⊑-len xs⊑ys ⟩
      length ys       ≡⟨ cong length ys≡zs ⟩
      length zs       ≤⟨ ⊑-len zs⊑ws ⟩
      length ws       <⟨ n<1+n (length ws) ⟩
      length (w ∷ ws) ∎

⊑-antisym-no-K :
  ∀{A : Set}{xs ys zs ws : List A} → xs ⊑ zs → ws ⊑ ys → xs ≡ ys → zs ≡ ws → xs ≡ zs
⊑-antisym-no-K ⊑-nil          ⊑-nil          []≡[]     []≡[]′    = refl
⊑-antisym-no-K (⊑-cons xs⊑zs) (⊑-cons ws⊑ys) x∷xs≡y∷ys x∷zs≡y∷ws = cong (_ ∷_) (⊑-antisym-no-K xs⊑zs ws⊑ys (∷-injectiveᵣ x∷xs≡y∷ys) (∷-injectiveᵣ x∷zs≡y∷ws))
⊑-antisym-no-K (⊑-skip xs⊑zs) ws⊑ys          xs≡ys     z∷zs≡ws   = ⊥-elim (lemma (sym z∷zs≡ws) ws⊑ys (sym xs≡ys) xs⊑zs)
⊑-antisym-no-K xs⊑zs          (⊑-skip ws⊑ys) xs≡y∷ys   zs≡ws     = ⊥-elim (lemma xs≡y∷ys       xs⊑zs zs≡ws       ws⊑ys)

⊑-antisym : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → ys ⊑ xs → xs ≡ ys
⊑-antisym xs⊑ys ys⊑xs = ⊑-antisym-no-K xs⊑ys ys⊑xs refl refl