The Coq mailing list

[Taral <taralx AT gmail.com>]

On Mon, Mar 2, 2009 at 3:21 PM, Ian Lynagh 
<igloo AT earth.li>
 wrote:
> I would be very grateful if anyone could shed any light. Suggestions for
> any other ways to improve the proof, or completely different ways to
> approach it, also welcome! Readability of the proof is very important to
> me.

Part of the problem here, in my opinion, is that you're having to do
way too much heavy lifting. C-zar is more of a compositional system --
you combine existing stuff to get what you want. It's not designed to
prove things like this.

Here's my proof:

intros; functional induction namedCommute (p, q).
injection H; clear H; intros; subst. (* I write this so often... *)
rewrite (UnnamedPatchCommuteSelfInverse p0 q0); auto.
discriminate.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown