CODEWITHSUNDEEP
equalityidrisreferential-transparency
Kevin Meredith
Kevin Meredith

Reputation: 41909

List Equality w/ `cong`

Following my other question, I tried to implement the actual exercise in Type-Driven Development with Idris for same_cons to prove that, given two equal lists, prepending the same element to each list results in two equal lists.

Example:

prove that 1 :: [1,2,3] == 1 :: [1,2,3]

So I came up with the following code that compiles:

sameS : {xs : List a} -> {ys : List a} -> (x: a) -> xs = ys -> x :: xs = x :: ys
sameS {xs} {ys} x prf = cong prf

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = sameS _ prf

I can call it via:

> same_cons {x=5} {xs = [1,2,3]} {ys = [1,2,3]} Refl
Refl : [5, 1, 2, 3] = [5, 1, 2, 3]

Regarding the cong function, my understanding is that it takes a proof, i.e. a = b, but I don't understand its second argument: f a.

> :t cong
cong : (a = b) -> f a = f b

Please explain.

Upvotes: 0

Views: 101

Answers (1)

Cactus
Cactus

Reputation: 27626

If you have two values u : c and v : c, and a function f : c -> d, then if you know that u = v, it has to follow that f u = f v, following simply from referential transparency.

cong is the proof of the above statement.

In this particular use case, you are setting (via unification) c and d to List a, u to xs, v to ys, and f to (:) x, since you want to prove that xs = ys -> (:) x xs = (:) x ys.

Upvotes: 1

Related Questions