Stream: Coq users

Topic: How to use list


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 (?).

view this post on Zulip 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.

view this post on Zulip 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