The Coq mailing list

["Carlos.SIMPSON" <carlos AT math1.unice.fr>]

Hi.
Does anybody know how to write a tactic which would do the following
thing?

If there is a hypothesis in the context

H:(x1 : T1)(x2 : T2) ... (Xn : Tn)((P x1...xn) /\ (Q x1 ... xn)),

add to the context the two statements

H0 :(x1 : T1)(x2 : T2) ... (Xn : Tn)(P x1...xn)
and
H1 :(x1 : T1)(x2 : T2) ... (Xn : Tn)(Q x1 ... xn)


In general Ti could depend on x1 ... x(i-1). A special case which would
be of interest
is when T1 ... Tk are constant types, and then T(k+1) ... Tn are
propositions depending on x1 ... xk (but
independent of each other).

Also the same question with  /\ replaced by <->   (then you want to add
P-> Q and Q -> P).

Thanks----
Carlos Simpson