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?

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

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

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

...

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. :(

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`

.

@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) [4] /\ 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: Jun 25 2024 at 15:02 UTC