The Coq mailing list

[Dimitris Vekris <dvekris AT hotmail.com>]

I have a list of objects with type Data  that has the property:

exists l: nat, such that:
if i < l, func d(i) = m
if i>= l and l < n, func d(i) < m

where n is the length of that list and func a function: Data ->  nat.

This property can be expressed in the hypothesis  following:

Require Import String.
Require Import List.

Inductive Data : Type :=  data : string -> Data.    
Variable func : Data -> nat.

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) .

What I am searching for is a way to express this property inside "list Data". I would also like to get rid of Variable dummy, which expresses nothing in my proof and is a pain in the ass for me when it comes to proving lemmas that are associated with Data.

Thanks in advance!

---

What can you do with the new Windows Live? Find out