The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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