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 ?

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

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:

- https://github.com/affeldt-aist/monae / https://github.com/affeldt-aist/infotheo
- https://github.com/coq-community/alea

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.

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`

.

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.

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).
```

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)

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

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.

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).
```

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.

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

ok so Pierre solution is the right one :wink:

Last updated: Oct 04 2023 at 23:01 UTC