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

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

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

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

```
```

Please ignore, the previous suggestion is indeed correct.

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: Apr 14 2024 at 09:39 UTC