The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On Tue, 13 Jan 2004 17:00:04 +0100
"Carlos.SIMPSON" 
<carlos AT math.unice.fr>
 wrote:
> ...
> My example in this direction is the following: suppose
> (bijective f) := (injective f) /\ (surjective f),
> and suppose we have a theorem
> thm1 : forall f, P f -> bijective f.
> Suppose we want to prove
> (injective g).
> Applying thm1 won't work.
> One could introduce it into the context by pose thm1,
> then unfold bijective, giving a context
> 
> H: forall f, Pf -> (injective f /\ surjective f)
> -------------------------------------------------------------------
> (injective g)
> 
> This is similar to the situation originating this thread.
> Does anybody know how to write in Ltac a tactic that transforms the above
> context to
> 
> H: forall f, Pf -> injective f
> H: forall f, Pf -> surjective f
> -------------------------------------------------------------------
> (injective g)
> ?

Using a lemma like this:

Lemma andimpl: forall A B C:Prop, (A->B/\C) -> ((A->B)/\(A->C)).
intros.
split;intro HA;elim (H HA);trivial.
Save.

you can define a tactic like the following, but I can't make it general
enough to apply to hypothesis of the form    forall ..., forall ...,
(A->B/\C). 


Ltac andimpl arghyp :=
 match type of arghyp with 
   | ?X1 -> (?X2 /\ ?X3) => cut ((X1 -> X2) /\ (X1 -> X3)) ;
            [(let nam := fresh in (intro nam; elim nam;intros))
              | apply (andimpl X1 X2 X3 arghyp)]
 end.

then just type andimpl H during the proof.

Hope this helps,

Pierre