list & its members · Coq users · Zulip Chat Archive

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?

Laurent Théry (Apr 18 2023 at 13:03):

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) [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: Oct 04 2023 at 20:01 UTC

Stream: Coq users

Topic: list & its members