The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

here is the proof script to .... 

Tactic Definition imp_and_and_imp :=
Match Context With [H:(a:?1)(?2 a)->(?3 a)/\(?4 a)|- ?5] ->
  Assert (a:?1)(?2 a) -> (?3 a);
    [Intros a Pa;NewDestruct (H a Pa);Trivial | Idtac];
  Assert (a:?1)(?2 a) -> (?4 a);
    [Intros a Pa;NewDestruct (H a Pa);Trivial | Clear H].

Variable F:Set.
Variables injective, surjective, P: F -> Prop.
Definition bijective [f:F]:= (injective f) /\ (surjective f).

Goal ((f:F) (P f) -> (bijective f)) -> (g:F)(injective g).
Unfold bijective;Intros thm1 g; imp_and_and_imp.

(* Or you can do directly *)
Restart.
Unfold bijective;Intros thm1 g.
Match Context With [H:(a:?1)(?2 a)->(?3 a)/\(?4 a)|- ?5] ->
   Assert (a:?1)(?2 a) -> (?3 a);
       [Intros a Pa;NewDestruct (H a Pa);Trivial |
   Assert (a:?1)(?2 a) -> (?4 a);
       [Intros a Pa;NewDestruct (H a Pa);Trivial | Clear H]].


Hope this help and  sorry for the syntax :).

Benjamin Gregoire



Carlos.SIMPSON wrote:

> > Au debut j'ai :
> >    
>       H : Ex c1 c2 : P(c1,c2) /\ Q(c1,c2)
>       -------------------------
>        Ex c3 c4 :  P'(c3,c4) /\ Q(c3,c4)
>
> Il se trouve que j'ai dans mes definitions qq part une regle qui dit :
> R1 :     P(a,b) ->  P'(a,b)
>
>
>
> It seems to me that the replies of the form: here is the proof script to
> prove ...,
> miss the important point that is raised here. Namely, Ltac doesn't let us
> write tactics
> which operate on the right part of an expression.
> 'And" is one of the essential parts of creating mathematical expressions,
> and Coq doesn't
> seem to have enough tools to deal with it.
> 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)
>
>
> ?
>
> ---Carlos
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>