Skip to content

Instantly share code, notes, and snippets.

@JLimperg
Last active February 22, 2017 18:40
Show Gist options
  • Save JLimperg/372665e774f4f73748ea388aba5418b3 to your computer and use it in GitHub Desktop.
Save JLimperg/372665e774f4f73748ea388aba5418b3 to your computer and use it in GitHub Desktop.
Agda solution to member_heq_eq
{-# 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')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment