[Agda] Re: Matching problem at end of equational reasoning proof

[Samuel Gélineau]

> The problem is that at the end of the equational reasoning the matching
> with the right-hand side of the type does not seem to work, namely: [...]

No, the problem is that you're using refl too liberally.

Refl only works when the left-hand side is a function application with
arguments precise enough for pattern-matching to succeed, and for the
expression to be evaluated a few more steps, yielding the right-hand side.
That means you need to know how _+_ and other operations are defined; if you
did, I suspect you would have tried to prove (2 * sum a ≈ a * (1 + a)) or
even (2 * sum a ≈ a * suc a) instead of (2 * sum a ≈ a * (a + 1)), as it
would have made your proof much easier.

For reasons I don't fully understand yet, refl also works when the role of
the left- and right-hand sides are reversed (normally sym is needed in this
case), when the application is a sub-expression (normally cong is needed in
this case), and when there are multiple simultaneous function applications
in the reasoning step (normally multiple consecutive  ≈⟨ _ ⟩ lines are
needed). Using cong with refl, like you did, is unnecessary, and even
harmful as it causes an unsolved meta.

In all other cases, you need to supply an explicit proof term. You have used
refl at places where you needed to apply distrib, +-comm and *-comm. Example
usages are:

    a + b
  ≈⟨ +-comm a b ⟩
    b + a

    a * b
  ≈⟨ *-comm a b ⟩
    b * a

    a * (b + c)
  ≈⟨ proj₁ distrib a b c ⟩
    a * b + a * c

    (a + b) * c
  ≈⟨ proj₂ distrib c a b ⟩
    a * c + b * c

    a * c + b * c
  ≈⟨ sym (proj₂ distrib c a b) ⟩
    (a + b) * c


– Samuel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090527/6182cd3d/attachment.html