The Coq mailing list

[Holden Lee <holdenl AT princeton.edu>]

Hi,

I'm trying to write an "invariance principle" tactic. To illustrate, consider the following example.

(*You have 27 socks. Every day you take out 2 or put 2 in. Prove that you will never have 0 socks.*)

Inductive Socks : nat -> Prop :=

  | begin : Socks 27

  | putin : forall x, Socks x -> Socks (x+2)

  | takeout : forall x, x>=2 -> Socks x -> Socks (x-2).

Theorem NonzeroSocks :

  not (Socks 0).

Proof.

  assert (forall x:nat, Socks x -> even x = false) as H.

  intros x H.

  induction H; admit. (*omitted*)

  intro H0.

  apply H in H0.

  simpl in H0.

  inversion H0.

End.

I want to write a tactic that does the boilerplate for this kind of proof.

(*ind_prop:A -> Prop, f:A -> Prop*)

Ltac invariance ind_prop f:=

  let t := type of f in 

    let A := (match t with

                 | ?P -> ?Q => ?P

             end) in

      assert (forall x:A, ind_prop x -> f x) as H; [intros x H; induction H | intro H0; apply H in H0].

so that I can write "invariance Socks (fun n:nat => even n = false)."

However, Coq complains about the match statement in the middle.

Syntax error: [tactic:tactic_expr] expected after '=>' (in [match_rule]).

What's the proper way to write this?

Thanks,

Holden