## Stream: Coq users

### Topic: Random selection

#### zohaze (Jan 22 2023 at 12:25):

I am writing a function which gives true in case of existence of same values between two provided indexes of list nat.
For example index[3] ,index[7] & l=[4,8,1,2,2,2,2,2,2,2,8]. I am performing patteren matching on list and function work well only for index 0 & index 1 because list start from head position. How i can select indexed randomly ?

#### Lessness (Jan 22 2023 at 12:55):

Imho, you don't. Because Coq has no built-in randomness.

#### Karl Palmskog (Jan 22 2023 at 13:52):

as a pure language, Coq indeed has no built-in random selection, but most people do it via some probability monad like Haskell, some examples:

#### Paolo Giarrusso (Jan 22 2023 at 19:20):

I am writing a function which gives true in case of existence of same values between two provided indexes of list nat.

it's hard to tell, but the question might be about deciding `exists i1 i2 v. nth_error i1 l = Some v /\ nth_error i2 l = Some v` — if so, the point is not that `i1` and `i2` must be random, but that one needs a complete search.

#### Pierre Castéran (Jan 23 2023 at 08:03):

Not clear what "provided index" means.
If only `l`is given, as Paolo says, you may want to prove that the following predicate is decidable:

``````Definition has_duplicates (l: list nat) :=
exists i1 i2 v: nat, nth_error l i1 = Some v /\ nth_error l i2 = Some v /\ i1 <> i2.
``````

If `l`, `i1` and `i2`are "provided", you just have to compare `nth_error l i1`with `nth_error l i2`.

#### Michael Soegtrop (Jan 23 2023 at 08:03):

Maybe "random" is meant here in the sense of "random access memory" and not in the sense of "random number generator". In this case: accessing lists e.g. via the `nth` function is always O(n), but since a while Coq has support for native arrays which have O(1) access. This comes at the price of a few axioms.

#### Laurent Théry (Jan 23 2023 at 13:13):

Here it is

``````Require Import List.

Definition index (n : nat) (l : list nat) := nth 0 l n.

Definition check_index n1 n2 l :=  Nat.eqb (index n1 l) (index n2 l).

Compute check_index 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).
``````

#### zohaze (Jan 24 2023 at 13:29):

sorry, i have not clearly mentioned it. l[i][j] i shows index which is 0 and j shows value that is 4, next 1 index and value is 8.... (above Laurent Thery's example)

#### Laurent Théry (Jan 24 2023 at 14:09):

Yes

``````Compute index 0 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).
``````

returns 4
and

``````Compute index 1 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).
``````

returns 8

#### zohaze (Jan 24 2023 at 14:27):

Above definition checks two values at two provided indexes. But i want to find true when values between two provided index is same. Like l[i][j] for i=3 to i=7(index) l[3] , l[7] (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil)=true
l[3] ,l[7] (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 22 :: 2 :: 2 :: 2 ::8 :: nil)=false. Secondly,in two dimentional array i should omit j for finding equal values between two indexes.

#### Laurent Théry (Jan 24 2023 at 15:22):

Something like this?

``````Require Import List.

Definition index (n : nat) (l : list nat) := nth 0 l n.

Definition check_index n1 n2 l := Nat.eqb (index n1 l) (index n2 l).

(* Build m :: m + 1 :: m + n *)
Fixpoint iota (m n : nat) : list nat :=
match n with
| 0 => nil
| S n' => m :: iota (S m) n'
end.

Compute iota 3 5.

(* Build m :: m + 1 :: n *)
Definition range m n := iota m (S n - m).

Compute range 3 7.

(* Build list of list of pairs *)
Definition all_pairs (l1 l2 : list nat) :=
map (fun x => map (fun y => (x, y)) l1) l2.

(* Build list of list for range *)
Definition range_pairs m n := all_pairs (range m n) (range m n).

Compute range_pairs 3 7.

Definition check_range_pairs m n l :=
map (fun l1  =>
filter (fun p : (nat * nat) => let (x, y) := p in
andb (Nat.ltb x y) (check_index x y l)) l1)
(range_pairs m n).

Compute check_range_pairs 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).

Definition test m n l := Nat.ltb 0 (length (check_range_pairs m n l)).

Compute test 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).
``````

#### Pierre Castéran (Jan 24 2023 at 16:02):

Another solution (with Laurent's helpers):

``````Definition select from to (l : list nat) :=
map (fun i =>  nth_error l i) (range from to).

Compute select 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).

Fixpoint same_value (n : nat) (l: list (option nat)) : bool :=
match l with
| nil => true
| Some m  :: l' =>  andb (Nat.eqb n m) (same_value n l')
| _ => false
end.

Definition test from to l :=
match    select from to l with
nil => true
| Some n :: l' => same_value n l'
| _ => false
end.

Compute test 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).

Compute test 2 7 (4 :: 8 :: 1 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).

Compute test 3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 22 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).
``````

Note there was a misunderstanding on the initial specification :
"existence of same values between two provided indexes of list nat."
It would have been better to say "all the values between index i and j are equal".
Or did you mean "there exist at least two equal values between index i and j" ?

If I take the example with `3 7 (4 :: 8 :: 1 :: 2 :: 2 :: 22 :: 2 :: 2 :: 2 :: 2 ::8 :: nil).`, I could say there exist some equal values between index 3 and 7.

#### zohaze (Jan 25 2023 at 04:22):

Yes. "all the values between index i and j are equal".

#### Laurent Théry (Jan 25 2023 at 04:27):

ok so Pierre solution is the right one :wink:

Last updated: Jun 24 2024 at 00:02 UTC