## Stream: Coq users

### Topic: How to use list

#### pianke (Jan 12 2022 at 18:46):

I am using x y co-ordinates for point location. I have a l1 -list of points(x,y) and each point in the list havs different x & y values.I want to extract a list of points from l1 between any two provided points.First , i search for the match value then move forward in the list .But how to match second element and come to the end of list.

#### Julin S (Jan 13 2022 at 03:27):

It might be helpful if you post the code for making the list of points as well.

#### Pierre Castéran (Jan 13 2022 at 07:14):

I'm not sure I understand clearly your specification.
Do you really mean that for each point `(x,y)`in the list, `x <> y` ? or that the points of the list are pairwise different ?

About the use of "between", is the following specification OK for you?
" Given two points `A` and `B`, and a list `l`, try to decompose `l` as `l1 ++(A::(l2++(B::l3)))` "
If so, it is easy to define a function of type `point -> point -> list point -> option(list point )` which returns either `Some l2` or `None`.
Then `l2`would correspond to what you want to compute (?).

#### pianke (Jan 13 2022 at 14:20):

Points of the list are pairwise different .x y co-ordinates of each pair in the list are different.

#### Pierre Castéran (Jan 13 2022 at 18:15):

Concerning your question about moving in the list, is the following solution OK for you (still to be [im]proved) ?
I use the same function for the first and second occurrence. But It depends on wether I understood well what you wanted to compute.

``````Require Import List Arith.
Import ListNotations.

Definition decide (P:Prop):= sumbool P (~P).

Section decompose.
Variables (A:Type)(A_eq_dec : forall a b:A,  decide (a=b)).

Fixpoint decompose1_helper  (a:A) (l0 l:list A) :  option(list A * list A) :=
match l with
nil => None
| b::l' => if A_eq_dec a b
then Some (rev l0, l')
else decompose1_helper a (b::l0) l'
end.

(** try to decompose l into (l1 ++ (a :: l2)) *)
Definition decompose1 (a:A) (l:list A) :=
decompose1_helper a nil l.

(* to improve : use a monadic notation *)
Definition between (a b : A)(l:list A):=
match decompose1 a l with
None => None
| Some(_,l1) =>
match decompose1 b l1
with
Some (l2,_) => Some l2
| None => None
end
end.

End decompose.
Arguments between {A} _ _ _ _.

Compute between  Nat.eq_dec 5 7 [1;3;4;5;6;33;6;7;9;10].
Compute between  Nat.eq_dec 5 7 [1;3;4;5;7;9;10].

Compute between  Nat.eq_dec 5 7 [1;3;4;5;6;33;6;17;9;10].
Compute between  Nat.eq_dec 5 7 [1;3;4;7;42;5;6;33;6;17;9;10].

(* lists of points *)
Record point : Set :=  Point {x: nat; y: nat}.

Definition point_eq_dec (A B: point) : decide (A=B).
Proof.  red; repeat decide equality.  Defined.

Compute between point_eq_dec (Point 5 0) (Point 7 3)
[Point 0 10; Point 5 0; Point 4 3; Point 7 2; Point 7 24;
Point 7 3; Point 10 3].
``````

Last updated: Feb 06 2023 at 12:04 UTC