The Coq mailing list

[harke AT cs.pdx.edu]

I'm not sure I follow your development exactly, but here are a few
simple observations.

On Wed, Jun 18, 2008 at 11:28:33PM +0200, Frédéric Gava wrote:
> Dear Coq-club,
>
> It is a little problem, perhaps just missing the good tactic...

[snip]

> | co_eval_glo_exists: forall e i,
>     (exists n, (0<=n<p) -> (co_eval_loc n (e n) (i n)))
>     -> co_eval_glo e i.

Are you sure it isn't the following, with a '/\' in place of the '->'?

   (exists n, (0<=n<p) /\ (co_eval_loc n (e n) (i n)))
    -> co_eval_glo e i.

The reasons I ask are
1. This is the idiom for a bounded existential (which is more common
   than what you've written)
2. In your second comment, you seem to expect the bound on ranges to hold 

>  (* Here I would like to have (e'0 n)=(e' n) forall n using 
> eval_loc_determinist *)

You can use the 'assert' tactic like so:

   assert (forall n, 0 <= n < p -> e'0 n = e' n).

It's easy to prove that extra obligation
(forall n, 0 <= n < p -> e'0 n = e' n), but offhand, I don't see
you'd use it.

>  (* Here I have x:Z but not 0<=x<p  and I can't use 
> eval_loc_and_co_eval_loc_exclusive *)

(see comment about /\ and ->)

-- 
Tom Harke