The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

You have both been really helpful! Thanks a lot.


>   As for building the property into list, if I understand you correctly,
> what would you say about this:
> 
> Inductive data_prop (m : nat) : nat -> Set :=
> | dp_nil : data_prop m 0
> | dp_cons : forall el, func el < m -> data_prop m 0 -> data_prop m 0
> | dp_consX : forall el i, func el = m -> data_prop m i -> data_prop m (S
> i).
> 
>   'data_prop m l' gives you a list with your property with parameters 'm'
> and 'l'.
> 

Especially your piece of advice has been really inspiring Adam. What I
actually need is

Variable func : nat -> nat.

Inductive data_prop (m : nat) : nat -> Set :=
| dp_nil : data_prop m 0
| dp_cons : forall el i, func el < m -> data_prop m i -> data_prop m (S i)
| dp_consX : forall el i, func el = m -> data_prop2 m i -> data_prop m (S i)
with data_prop2 (m : nat) : nat -> Set :=
| dp2_nil : data_prop2 m 0
| dp2_consX : forall el i, func el = m -> data_prop2 m i -> data_prop2 m (S
i).

where i and S i are indexes.
I changed the type of func to nat->nat, which is actually wrong just to help
Coq typecheck. What I need is a "func" dependent on data_prop. "func" uses
recursively data_prop. Is it possible to define a fixpoint dependent on an
inductive definition, which also calls this fixpoint? I hope I am clear. Am
I getting to "dependent"? The last question applies to the experienced users
of Coq.

-- 
View this message in context: 
http://www.nabble.com/Data-Structures-tp22535211p22540515.html
Sent from the Coq mailing list archive at Nabble.com.