The Coq mailing list

[dimitrisg7 <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!
-- 
View this message in context: 
http://www.nabble.com/Data-structures-tp22534172p22534172.html
Sent from the Coq mailing list archive at Nabble.com.