pianke (Jan 12 2022 at 18:46): 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 l2would 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: Oct 03 2023 at 04:02 UTC