The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Thank you for giving me several ways of solving my question. 

As Benjamin wrote, Pierre's answer may not be very precise, but is
useful to my situation. Indeed I first tried Pierre's suggestion
because it seemed to require the least overhead and it worked well for
my particular subgoal.  At the same time, I found a few disadvantages
of ex_intro: 

- (major) Instantiations may not propagate into other subgoals. 
For instance, 

  Goal exists x:nat, exists y : nat, y*y = x /\ x = 9.
  eapply ex_intro.
  exists 3.
  split.
  Focus 2.
  apply refl_equal.
 
 At this point, I get a subgoal containing a non-instantiated variable, which
 must have been instantiated by the last command "apply refl_equal.".
 This is quite unhelpful.

- (minor) I may end up unawarely with a proof containing
non-instantiated variable. 

- (minor) Successive uses of ex_intro can produce hard-to-read subgoals
containing several occurrences of ?11, ?12, ?13, etc..

- (As Benjamin pointed out) 

  Parameters P Q R : Prop.
  Parameter H : exists i : nat, (P /\ 3 = 3).
  Goal exists i : nat, (P /\ (exists j : nat, j = 3)).
  eapply ex_intro.

 I cannot use H anymore...


Many of my Lemmas contain deeply nested existentials and more than 5
conjunctions. So I will choose a better one among your suggestions, 
depending on the complexity of my subgoals.

Thank you.

With best regards,
Keiko.