The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

Axiom param : nat -> Type.
Axiom val : ∀ n, param n.

Inductive Laws : nat -> Prop :=
  | law_1 : Laws 1
  | law_6 : Laws 6
  | law_7 : Laws 7.
Definition appl {n} (_:Laws n) := match n return match n with 0 => param (S 
n) | S n => param n end with
                                    | 0 => val 1
                                    | S n => val n
                                  end.

Record rec := { m1 : param 0; m7: param 6; m6: param 5 }.

Goal rec.
constructor.
(* This following three tactics solve the goal, but are very verbose *)
let n:= fresh in (evar (n:nat); assert (Laws n) as P; subst n; [ constructor 
1 | apply (appl P)]).
let n:= fresh in (evar (n:nat); assert (Laws n) as P; subst n; [ constructor 
3 | apply (appl P)]).
let n:= fresh in (evar (n:nat); assert (Laws n) as P; subst n; [ constructor 
2 | apply (appl P)]).
Defined.

Goal rec.
(* I would think the following would also work, but "constuctor" seems
   to be ignoring its argument. Anyway, I have a number of theorems that
   can be proved like this that I would like automate. *)
Ltac TAC k := (let n:= fresh "n" in (evar (n:nat); assert (Laws n) as P; 
subst n); [ constructor k | apply (appl P) ]).
constructor; [TAC 1 | TAC 3 | TAC 2].