The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I'm trying to construct a tactic that rewrites with a lemma [nat_assoc] repeatedly, and tries to solve the resulting goal after each rewrite.  (That is, I'm trying to create a tactic that tries to solve the goal with a particular tactic in every possible permutation of parenthetizations).

Lemma nat_assoc a b c : (a + b) + c = a + (b + c).

  induction a; simpl; try reflexivity.

  rewrite IHa; reflexivity.

Qed.

However, it seems that [Tactic Notation]s can't be recursive, and I can't figure out a way to [rewrite nat_assoc at n] if [n] is passed into a standard tactic; none of the following work:

Goal forall (a b c d e f g : nat), a + b + c + d + e + f = g.

  Ltac stepAssociativity' n := rewrite nat_assoc at n.

  (* stepAssociativity' 1.  *) (* In nested Ltac calls to "stepAssociativity'" and

"rewrite nat_assoc in |- * at n", last call failed.

Error: Ltac variable n is bound to a term which cannot be coerced to

an integer. *)

  (* Tactic Notation "stepAssociativity" integer(n) :=

      rewrite nat_assoc at n; try stepAssociativity (S n). *) (* Error: The reference stepAssociativity was not found in the current

environment.*)

Does anyone have ideas/suggestions?

Thanks.

-Jason