coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT hcoop.net>
- To: Ian Lynagh <igloo AT earth.li>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] C-zar proof help
- Date: Mon, 02 Mar 2009 18:44:35 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Ian Lynagh wrote:
I'm very new to coq, and am trying to do some proofs with C-zar.
I've never heard of C-zar, but here's a normal Ltac proof.
Lemma NamedPatchCommuteSelfInverse : forall p q p' q',
namedCommute (p, q) = Some (q', p')
-> namedCommute (q', p') = Some (p, q).
simpl; intros;
repeat match goal with
| [ H : context[match ?p with MkNamedPatch _ _ => _ end] |- _ ] => destruct p
| [ H : context[match commute (?x, ?y) with Some _ => _ | None => _ end] |- _ ] =>
generalize (UnnamedPatchCommuteSelfInverse x y); intro;
destruct (commute (x, y)); try discriminate
| [ x : (_ * _)%type |- _ ] => destruct x
| [ H : Some _ = Some _ |- _ ] => injection H; clear H; intros; subst
| [ H : forall p' q' : UnnamedPatch, _ = _ -> _ = _ |- _ ] => rewrite H; reflexivity
end.
Qed.
- [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help, Adam Chlipala
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
- Re: [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help, Pierre Corbineau
- Re: [Coq-Club] C-zar proof help, Taral
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help, Adam Chlipala
Archive powered by MhonArc 2.6.16.