Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Feb 13, 2019
Embed
What would you like to do?
Using a View makes proving easier
open import Relation.Nullary
open import Agda.Builtin.Equality
data X : Set where
a b c : X
firstA : (x y z : X) X
firstA a y z = a
firstA x a z = a
firstA x y a = a
firstA x y z = a
firstA-id : x y z firstA x y z ≡ a
firstA-id a y z = refl
-- firstA-id x a z = refl -- doesn't work
firstA-id b a z = refl
firstA-id c a z = refl
-- firstA-id x y a = {!refl!} -- doesn't work
firstA-id b b a = refl
firstA-id b c a = refl
firstA-id c b a = refl
firstA-id c c a = refl
firstA-id b b b = refl
firstA-id b b c = refl
firstA-id b c b = refl
firstA-id b c c = refl
firstA-id c b b = refl
firstA-id c b c = refl
firstA-id c c b = refl
firstA-id c c c = refl
-- rather than matching on the LHS on a, we can use a function
-- distinguishing two cases: a and not a.
isA : x Dec (x ≡ a)
isA a = yes refl
isA b = no (λ ())
isA c = no (λ ())
-- The function is just as long:
firstA' : (x y z : X) X
firstA' x y z with isA x | isA y | isA z
... | yes _ | _ | _ = a
... | _ | yes _ | _ = a
... | _ | _ | yes _ = a
... | _ | _ | _ = a
-- But the proof is vastly shorter:
firstA'-id : x y z firstA' x y z ≡ a
firstA'-id x y z with isA x | isA y | isA z
... | yes _ | _ | _ = refl
... | no _ | yes _ | _ = refl
... | no _ | no _ | yes _ = refl
... | no _ | no _ | no _ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment