## Stream: Coq users

### Topic: list & its members

#### zohaze (Apr 18 2023 at 12:07):

I have function f which take two natural numbers and gives a proposition. I want to use the result of this function to determine the presence of an element in the list. Problem is that f can handle two numbers only at a time. But i want to check the whole list.
Therefore in case of three or more elements , i am using transitive property. as
ff h1 h2 ff h2 h3 ff h1 h3 -> In h3 l
ff( ff h1 h2 ff h2 h3 ff h1 h3) h4... In h4 l.end. How to write it in Coq?

what is ff?

#### Lessness (Apr 19 2023 at 00:00):

ff seems to be that same binary relation on natural numbers that's mentioned in the start (or simply f).

#### Lessness (Apr 19 2023 at 00:01):

My try...

``````Require Import List.

Parameter f: nat -> nat -> Prop.
Parameter l: list nat.
Parameter this_is_not_transitive_property: forall h1 h2 h3, f h1 h2 -> f h2 h3 -> f h1 h3 -> In h3 l.
``````

#### Lessness (Apr 19 2023 at 00:04):

The last line seems to be some kind of generalization of `this_is_not_transitive_property`...

#### Lessness (Apr 19 2023 at 00:07):

Anyway, the OP's problem seems to be caused by problems in "pre-Coq" thinking. At least sometimes one should take time with paper and pen to find clearer understanding of the problem. I believe that hasn't happened here yet. :(

#### Lessness (Apr 19 2023 at 00:19):

Or maybe this is what the OP wants...

``````Require Import List.

Parameter f: nat -> nat -> Prop.

Fixpoint f_of_list (L: list nat) :=
match L with
| nil => True
| cons x nil => True
| cons x (cons y t as tail) => f x y /\ f_of_list tail
end.
``````

Then, for example, `Eval compute in (f_of_list (cons 1 (cons 2 (cons 3 nil)))).` results in `f 1 2 /\ f 2 3 /\ True`.

#### Pierre Castéran (Apr 19 2023 at 05:51):

@Lessness Or may be the OP was thinking about something like :

``````Fixpoint f_of_list' (L: list nat) :=
match L with
| nil => True
| x::tl => Forall (f x) tl  /\ f_of_list' tl
end.

Eval simpl in  f_of_list' [1;2;3;4].
(*   = Forall (f 1) [2; 3; 4] /\
Forall (f 2) [3; 4] /\ Forall (f 3)  /\ Forall (f 4) [] /\ True
: Prop
*)
``````

I believe that it's the OP's responsability to submit problems the most precisely as possible.
For instance, using some light mathematical language, like
`for all pair of indices i < j < length L, f x_i x_j ` or `for all i < length L -1, f x_i x_{i+1}`.

Last updated: Oct 04 2023 at 20:01 UTC