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.

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

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 (?).

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

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