From d73b801d8aada0e1f04740a3a65f7ccd9e8a9761 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 10 Jan 2017 11:01:30 +0100
Subject: [PATCH] Implement simple version of k-min
---
util/minmax.v | 32 +++++++++++++++++++++++++++++++-
1 file changed, 31 insertions(+), 1 deletion(-)
diff --git a/util/minmax.v b/util/minmax.v
index 9541ed6e6..2dad52842 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -570,4 +570,34 @@ Section ExtraLemmas.
}
Qed.
-End ExtraLemmas.
\ No newline at end of file
+End ExtraLemmas.
+
+Section Kmin.
+
+ Context {T1 T2: eqType}.
+
+ Variable rel: T2 -> T2 -> bool.
+ Variable F: T1 -> T2.
+
+ Fixpoint seq_argmin_k (l: seq T1) (k: nat) :=
+ if k is S k' then
+ if (seq_argmin rel F l) is Some min_x then
+ let l_without_min := rem min_x l in
+ min_x :: seq_argmin_k l_without_min k'
+ else [::]
+ else [::].
+
+ Lemma seq_argmin_k_exists:
+ forall k l x,
+ k > 0 ->
+ x \in l ->
+ seq_argmin_k l k != [::].
+ Proof.
+ induction k; first by done.
+ move => l x _ IN /=.
+ destruct (seq_argmin rel F l) as [|] eqn:MIN; first by done.
+ suff NOTNONE: seq_argmin rel F l != None by rewrite MIN in NOTNONE.
+ by apply seq_argmin_exists with (x0 := x).
+ Qed.
+
+End Kmin.
\ No newline at end of file
--
GitLab