coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Data structures

From: Taral <taralx AT gmail.com>
To: dimitrisg7 <dvekris AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Data structures
Date: Mon, 16 Mar 2009 10:07:33 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=iQX8sV7s4Agh8RFS1veRquuJQrJxnqGNPyw4shQuV86mb7jkCXwp3pzOjoOVR/c3OI rQYyYFtFjvDx1DZRWnbFhVEDQI48iayfnsOyVY+JkVRljNguU02f+vl7ped2B6FFFRkh Jq9HAjpDOO7iKQehvIQy1/6cIclmBrd1k3iK4=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Mar 16, 2009 at 2:14 AM, dimitrisg7
<dvekris AT hotmail.com>
wrote:
> Hypothesis hypothesis_1 :
> �forall (m : nat)(dummy : Data)(d : list Data),
> � �let n := List.length d in
> � � �exists l , l <= n ->
> � � � �(forall (i : nat) , i < l -> func (nth i d dummy) = m) ->
> � � � �(forall (i : nat) , i >= l /\ i < n -> func (nth i d dummy) < m) .

Wow. This is trivially true by setting l = n + 1. I don't think that's
what you wanted.

Even the corrected version is not true for all func (set func to
always return 1).

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

Re: [Coq-Club] Data Structures, (continued)
- [Coq-Club] Data structures, dimitrisg7
  - Re: [Coq-Club] Data structures, Taral