The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Here's a much easier, more complete, and perhaps even semi-respectable 
approach.

Consider parametrized shapes to be sig types, and make a variant of sigT 
for just this purpose so as not to confuse any naturally appearing 
sigT's with it.  Make a nice nested notation for it.  The shape tactic 
then just tries to solve the shape type from a multimatch of hyps:

Inductive sig_shape {A} (P:A -> Type) : Type :=
    exist_shape : forall x:A, P x -> sig_shape P.

Notation "'xsh' x .. y , p" :=
  (sig_shape (fun x => .. (sig_shape (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity).

Ltac shape type tac :=
  multimatch goal with
    H:_ |- _ =>
    let z:=constr:($(repeat eapply exist_shape; exact H)$ : type) in
    tac H z
  end.

Ltac nthxsh n x :=
  match x with
    (exist_shape _ ?X ?T) =>
    match n with 0 => constr:(X) | S ?N => nthxsh N T end
  end.

In this approach, tac takes 2 args: the hyp that matched, and the 
exist_shape that resulted from the match.  The tac can then use nthxsh 
to get the nth binding (0-based) of the shape type from that second 
arg.  One could even try to get the binding out by name, I guess.  Or type.

Goal True.
assert (True \/ False \/ True) as P1 by tauto.
assert (True \/ True \/ False) as P2 by tauto.
assert (False \/ False \/ True) as P3 by tauto.
assert (True \/ False \/ False) as P4 by tauto.
Fail shape (xsh x y, x \/ x \/ y)
  ltac:(fun H X => hypntype H; idtac X; let Y:=nthxsh 1 X in idtac Y); 
fail.
repeat shape (xsh x y, x \/ x \/ y)
  ltac:(fun H X => hypntype H; clear H; let Y:=nthxsh 0 X in idtac Y).

-- Jonathan