Agda: proving that, when values are equal, their constructor arguments are equal

2
votes

I'm trying to write the following function:

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}

I don't know how to write this. To me, it is intuitive to the point of being axiomatic, but the compiler doesn't accept refl as a proof of it.

I'm routinely having to prove these sorts of things, for example, showing that if two non-empty lists are equal, then their heads are equal.

What is the general approach to this? Is this related to Conor McBride's "green-goo" of having functions in the return of Constructors?

1
typeslogicagdadependent-typeformal-verification
Have you tried pattern matching on pf? – Vitus
emacs just expands it to refl... I'm probably missing the obvious, but I don't see how that helps. – jmite
I feel like cong would be useful here, but I don't know how to write a function that takes just x to x, since it would inherently be partial. – jmite
Here is how justEq can be defined via cong. – user3237465
@user3237465: I suspected there would be a nice solution with heterogeneous equality. Nice one! – Vitus

1 Answers

3
votes

The basis of the solution is to pattern match on pf being refl together with using a dotted pattern for y being equal to x (because of the type of refl!).

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x .x refl = {!!}

At this point, the type of the hole on the right-hand side has been unified to (x ≡ x) because of the y = .x equality from the pattern match, meaning you can use refl as a well-typed value, giving

justEq x .x refl = refl