The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.