The Coq mailing list

[Bahman Sistany <bsistany AT yahoo.ca>]

Thanks to all. The equivalent formula works fine for me. 

I notice coq does some renaming of variables: n0, n1, ... which intuitively makes sense in this case. However, what is the general rule by which such renaming happens?  

--Bahman 

---

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Bahman Sistany <bsistany AT yahoo.ca>
Cc: Coq Club <coq-club AT inria.fr>
Sent: Saturday, August 10, 2013 9:37:59 AM
Subject: Re: [Coq-Club] existentially quantified proposition

If you're willing to tolerate a logically equivalent quantifier rearrangement, there's:

Fixpoint separated (t t' len : nat) : Prop :=
  match len with
    | O => t < t'
    | S len' => exists n, t < n /\ separated n t' len'
  end.

On 08/10/2013 08:39 AM, Rui Baptista wrote:

How about this?

Require Import Coq.Lists.List.

Fixpoint gen'' (l : list nat) : Prop :=
  match l with
  | nil => True
  | cons x l' =>
    match l' with
    | nil => True
    | cons x' _ => x < x' /\ gen'' l'
    end
  end.

Fixpoint gen' (t' len : nat) (l : list nat) : Prop :=
  match len with
  | 0 => gen'' (rev (cons t' l))
  | S len' => exists x, gen' t' len' (cons x l)
  end.

Definition gen (t t' len : nat) : Prop :=
  match len with
  | 0 => True
  | S len' => gen' t' len' (cons t nil)
  end.

Eval simpl in forall t t', gen t t' 0.
Eval simpl in forall t t', gen t t' 1.
Eval simpl in forall t t', gen t t' 2.
Eval simpl in forall t t', gen t t' 3.
Eval simpl in forall t t', gen t t' 4.

On Sat, Aug 10, 2013 at 7:15 AM, Bahman Sistany <bsistany AT yahoo.ca> wrote:

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