Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem of "exclusive proof"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem of "exclusive proof"


chronological Thread 
  • From: harke AT cs.pdx.edu
  • To: Fr�d�ric Gava <gava AT univ-paris12.fr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Problem of "exclusive proof"
  • Date: Thu, 19 Jun 2008 11:06:39 -0700
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page