The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi, Keiko and Benjamin
On the specific point of instantiation propagation :

Keiko Nakata wrote:

> - (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.
>  
I tried your example (with a very slight change : Focus was removed in 
order to display all subgoals) and after the
tactic call "eapply refl_equal" Coq instantiated the existential 
variable in the first subgoal.

Goal exists x:nat, exists y : nat, y*y = x /\ x = 9.
 eapply ex_intro.
 exists 3.
 split.
 (* 2 subgoals

 ============================
  3 * 3 = ?5

subgoal 2 is:
?5 = 9
*)
 2:  eapply refl_equal.
(*
1 subgoal

 ============================
  3 * 3 = 9
*)
 trivial.
Qed.

On the other points, you are right.

> - (minor) I may end up unawarely with a proof containing
> non-instantiated variable. 
>
>  
In the following example, the variable "i" is not used in the formulas 
(P /\ (exists j : nat, j = 3)) and (P /\ 3 = 3).
Therefore, solving suboals like (P /\ (exists j : nat, j = 3)) won't 
help to instantiate "i" ; this is the situation you
describe.

>  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...
>
>  
More generally, if you have an hypothesis of the form "exists i, P i " 
and a goal of the form "exists i, Q i", I must
(even using ex_intro) eliminate first H. (I think that's what Benjamin 
meant).  When I was experimenting with Isabelle, this was the way I had 
to work. On the other hand, it should be interesting to have a tactic 
for permuting nested quantifiers whenever possible,  but I am not very 
expert in writing tactics in Ltac.

> 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.
>  

If this situation occurs too often, it should be interesting to 
rearrange your lemmas in order to ensure that if
y depends on x, then the form (exists x, P x /\ exists y, Q x y)) is 
prefered to (exists y, exists x, P x /\ Q x y).

Cheers,

Pierre