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:
> Remnants of some other avenues I explored are in comments at the end.

Okay, I took a closer look.

You need to expose (commute (up, uq)) before taking cases on it. Also,
you cannot extract the hypothesis if you are going to case on a
subexpression.

proof.
let p : NamedPatch,
    q : NamedPatch,
    p' : NamedPatch,
    q' : NamedPatch.
consider np:Name, up:UnnamedPatch from p.
consider nq:Name, uq:UnnamedPatch from q.
consider np':Name, up':UnnamedPatch from p'.
consider nq':Name, uq':UnnamedPatch from q'.
reconsider thesis as (
   match commute (up, uq) with
   | Some (pair q'0 p'0) => Some (MkNamedPatch nq q'0, MkNamedPatch np p'0)
   | None => None (A:=NamedPatch * NamedPatch)
   end = Some (MkNamedPatch nq' uq', MkNamedPatch np' up') ->
   match commute (uq', up') with
   | Some (pair q'0 p'0) => Some (MkNamedPatch np' q'0, MkNamedPatch nq' p'0)
   | None => None (A:=NamedPatch * NamedPatch)
   end = Some (MkNamedPatch np up, MkNamedPatch nq uq)).
per cases on (commute (up, uq)).
suppose it is None.
thus thesis.
suppose it is (Some (uq'', up'')).

At this point I got annoyed at having to extract out the injection
equalities and gave up.

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