Agda solution to member_heq_eq

challenge.agda

{-# OPTIONS --without-K #-}

module challenge where

open import Data.List using (List ; _∷_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; inspect ; [_])


module _ {T : Set} where

  infix 4 _∈_

  data _∈_ (x : T) : List T → Set where
    here : ∀ {xs} → x ∈ x ∷ xs
    there : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs


  del-member : {ku : T} {ls : List T} → ku ∈ ls → List T
  del-member (here {xs}) = xs
  del-member (there {x} {_} pxs) = x ∷ del-member pxs


  member-heq : {l r : T} {ls : List T} (m : l ∈ ls) → r ∈ ls
    → r ∈ del-member m ⊎ l ≡ r
  member-heq here here = inj₂ refl
  member-heq here (there mr) = inj₁ mr
  member-heq (there ml) here = inj₁ here
  member-heq (there ml) (there mr) with member-heq ml mr
  ... | inj₁ r∈dmm = inj₁ (there r∈dmm)
  ... | inj₂ l≡r = inj₂ l≡r


  cast-∈ : ∀ {l r : T} {ls} → l ≡ r → l ∈ ls → r ∈ ls
  cast-∈ refl ml = ml


  cong-cast-∈ : ∀ {l r ls ls'} {l≡r : l ≡ r} {ml : l ∈ ls} {mr : r ∈ ls}
    → (f : ∀ {x} → x ∈ ls → x ∈ ls')
    → cast-∈ l≡r ml ≡ mr
    → cast-∈ l≡r (f ml) ≡ f mr
  cong-cast-∈ {l≡r = refl } _ refl = refl


  member-heq-eq : ∀ {l r ls} (ml : l ∈ ls) (mr : r ∈ ls) l≡r
    → member-heq ml mr ≡ inj₂ l≡r
    → cast-∈ l≡r ml ≡ mr
  member-heq-eq here here l≡r refl = refl
  member-heq-eq here (there mr) l≡r ()
  member-heq-eq (there ml) here l≡r ()
  member-heq-eq (there ml) (there mr) l≡r eq
    with member-heq ml mr
       | inspect (member-heq ml) mr
  member-heq-eq (there ml) (there mr) l≡r ()   | inj₁ _ | _
  member-heq-eq (there ml) (there mr) l≡r refl | inj₂ _ | [ eq' ]
      = cong-cast-∈ {l≡r = l≡r} there (member-heq-eq ml mr l≡r eq')