The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 7 avr. 2010 à 18:08, Adam Koprowski a écrit :

> I have a new (but related) question:
> 
>      P : nat -> Prop
>      H : {x : nat | P x}
>      ============================
>       {y : nat | P y}
> 
> This example is too simple and can be proved by "assumption", but let's
> forget about it.  Here,
>  * "destruct H; eexists; eassumption" succeeds, but
>  * "eexists; destruct H; eassumption" fails
> because of the reason above.  But visually, the results of
>  * "destruct H; eexists" and
>  * "eexists; destruct H"
> look the same, and it's somewhat confusing:
> 
>      P : nat -> Prop
>      x : nat
>      p : P x
>      ============================
>       P ?6
> 
> Does Coq have any command or configuration option to enable some kind of
> 'visual indication' on the context?  
>   I believe that 'Show Existentials' is what you are looking for: 
> http://coq.inria.fr/refman/Reference-Manual010.html#@command192.
>   Adam

The command [Set Printing Existential Instances] might be useful too,
it prints the substitution applied to the existential.
In that case, [destruct H; eexists] gives

  P : nat -> Prop
  x : nat
  p : P x
  ============================
   P ?15 (* [P, x, p] *)

while [eexists; destruct H] gives:
  
  P : nat -> Prop
  x : nat
  p : P x
  ============================
   P ?16 (* [P, exist (fun x0 : nat => P x0) x p] *)

-- Matthieu