## Stream: Coq users

### Topic: Finding min not used number in list

#### Adrián García (Nov 21 2021 at 21:28):

Is there a way to find a new minimum number in a not necessarily sorted list? For instance, given [6, 4, 3, 5, 0, 1], then the answer is 2

#### Li-yao (Nov 21 2021 at 22:27):

Sure, the length of the list is an upper bound on that number, so the search is finite.

#### Adrián García (Nov 23 2021 at 00:36):

Then is there a way to "substract" a list from another one? If the upper bound is the length of the list, I can create a list with `seq 0 (len L)` and then substract that from my original list, something like this?

``````Definition diff (l1 l2 :  list nat) :=
foldr (fun x l => if x \in l2 then l else x :: l]) nil l1.
``````

#### Laurent Théry (Nov 23 2021 at 12:07):

Are you using `mathcomp`? if so you can use `iota` and `find` to do the trick

``````From mathcomp Require Import all_ssreflect.

Definition find_new_min l := find (fun i => i \notin l) (iota 0 (size l)).

Compute find_new_min [:: 6; 4; 2; 5; 0; 1].
``````
``````
``````

#### Gleb (Nov 23 2021 at 13:20):

Please ignore, the previous suggestion is indeed correct.

#### Adrián García (Nov 24 2021 at 00:27):

I ended up with these two definitions, diff that removes elements if they exist in the same list, and then using it with the list from 0 to the length of the list:

``````Definition diff (l1 l2 : list nat) : list nat :=
List.filter (fun n => negb (List.existsb (Nat.eqb n) l2)) l1.

Definition minIndex (l2 : list nat): nat :=
let l1  := seq 0 (length l1) in
match diff l G' with
| nil => slist_length G
| n :: _ => n
end.
``````

Last updated: Oct 03 2023 at 19:01 UTC