coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Problem of "exclusive proof", Frédéric Gava
- Re: [Coq-Club] Problem of "exclusive proof", harke
Archive powered by MhonArc 2.6.16.