The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Hi,

Although the shape of formula is not exactly what you wanted, an equivalent 
formulation would be:

Fixpoint gen (t t' : nat)(n:nat) : Prop :=
  match n with
  | 0 => True
  | 1 => t < t'
  | S n' => exists x, t < x /\ gen x t' n'
  end.

When n = 4, it generates this formula: 

exists x : nat, t < x /\ (exists x0 : nat, x < x0 /\ (exists x1 : nat, x0 < 
x1 < t'))

All the "x < y" propositions could also be pushed under the final exists. 
But, directly generating in such a form might be complicated because of the 
issue of passing arbitrary number of variables recursively. I think a simple 
ltac script can transform the the above goal into the desired form.

-- Duckki


On Saturday, August 10, 2013 at 2:15 AM, Bahman Sistany 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