TL;DR: I'd like an example or two of using cong in the Idris REPL to help me understand it better.
The generic equality type is conceptually defined like so:
data (=) : a -> b -> Type where
Refl : x = x
When I first encountered this, I was very confused by the syntax. (I kept thinking of = as an operator rather than a type.) But playing around with it in the REPL helped me to understand. For example, we can declare types to represent false equalities:
λ> 2 + 2 = 5
4 = 5 : Type
λ> 2 = "wombat"
2 = "wombat" : Type
However, the only constructor for the = is Refl, and we can only use it when the two arguments are equal.
λΠ> the (4 = 4) Refl
Refl : 4 = 4
λΠ> the (4 = 5) Refl
... type mismatch
So now I'm trying to understand cong by experimenting with it in the REPL.
The function cong proves that if two values are equal, applying a
function to them produces an equal result. I found the definition.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl
So, for example, if I define...
λ> :let twoEqTwo = the (2 = 2) Refl
defined
...then I expected to be able to show that adding 1 to both sides results in another equality.
λΠ> :let ty = (S 2 = S 2)
defined
λΠ> the ty (cong twoEqTwo)
...type mismatch
Can anyone show me an example or two of using cong in the REPL?
The 2s are of the wrong type. They have defaulted to the type Integer in twoEqTwo, because they have no other constraints. See, an unconstrained 2:
idris> 2
2 : Integer
Yet, in ty, you say S 2. The S forces the whole thing to work in Nat:
idris> S 2
3 : Nat
Make twoEqTwo work in Nat, too:
idris> :let twoEqTwo = the (the Nat 2 = 2) Refl
idris> the (S 2 = S 2) twoEqTwo
Refl : 3 = 3
Note that type inference can sort this out itself if you let it see the entire expression:
idris> the (S 2 = S 2) (cong (the (2 = 2) Refl))
Refl : 3 = 3