Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] C-zar proof help

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] C-zar proof help


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page