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 13 2024 at 01:02 UTC