coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] existentially quantified proposition

From: Bahman Sistany <bsistany AT yahoo.ca>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] existentially quantified proposition
Date: Fri, 9 Aug 2013 23:15:03 -0700 (PDT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.ca; h=X-YMail-OSG:Received:X-Rocket-MIMEInfo:X-Mailer:Message-ID:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type; b=rdJw6SrFchBPLKYI+15QD5DXQ6WFutD5trO4Cf4V9cz6SR/4sH2Ha//g/WB1ypdingSt6ideW0Ku7kuRFJOK5xXFrucS79eHckZPCErdFvv5dVqM6uTfgKh3KTuLpwecE+ezlLwjqbByelW9qAVLAF16AMHkadALQ9JCzL8dx6Y=;

Hi,

I am trying to come up with an existentially quantified proposition where I generate the witnesses (xi's here) and the property programmatically/dynamically.

Fixpoint gen (t t' : nat)(len:nat) : Prop := ???

(* When len=2, I need: *)

exists x2, (t < x2 < t')

(* When len=3, I need: *)

exists x2, x3 (t < x2 < x3 < t')

...

I have been working on various ways of extending 'ex' but nothing works so far. Any thoughts on the general problem would be appreciated.

--Bahman

[Coq-Club] existentially quantified proposition, Bahman Sistany, 08/10/2013
- Re: [Coq-Club] existentially quantified proposition, Duckki Oe, 08/10/2013
- Re: [Coq-Club] existentially quantified proposition, Rui Baptista, 08/10/2013
  - Re: [Coq-Club] existentially quantified proposition, Adam Chlipala, 08/10/2013
    - Re: [Coq-Club] existentially quantified proposition, Bahman Sistany, 08/10/2013
      - Re: [Coq-Club] existentially quantified proposition, Adam Chlipala, 08/10/2013