The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

Dear Ian,

I will find some time to look into your work in some detail before the 
end of the week and try to come up with answers to your requests, in the
meantime some teaching duties keep me busy.

Pierre


Ian Lynagh a écrit :
> Hi all,
>
> I'm very new to coq, and am trying to do some proofs with C-zar. I'm
> currently largely stumbling in the dark, but I'm hoping that will
> improve once I've got a proof or two done.
>
> In the attached coq file I make an axiom:
>
>       (commute (p, q) = Some (q', p')
>     -> commute (q', p') = Some (p, q)).
>
> for UnnamedPatch's, and then I try to prove
>
>       (namedCommute (p, q) = Some (q', p')
>     -> namedCommute (q', p') = Some (p, q)).
>
> for NamedPatch's, where
>
>     Inductive NamedPatch : Set
>      := MkNamedPatch : Name -> UnnamedPatch -> NamedPatch.
>
> and namedCommute basically just does commute on the UnnamedPatch's. The
> proof is incomplete, and the last line goes orange (but I don't really
> understand why). Also, even if it was green, I'm not sure what would
> come next. "thus thesis."?
>
> Remnants of some other avenues I explored are in comments at the end.
>
> 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.
>
>
> Thanks
> Ian

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B2G2
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard