Commit e7d2a65b authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add more lemmas about min/max

parent d73b801d
...@@ -444,6 +444,17 @@ Section MinMaxSeq. ...@@ -444,6 +444,17 @@ Section MinMaxSeq.
Definition max_nat_cond P (a b: nat) := Definition max_nat_cond P (a b: nat) :=
seq_max_nat (filter P (values_between a b)). seq_max_nat (filter P (values_between a b)).
Lemma min_nat_cond_exists:
forall (P: nat -> bool) (a b: nat) x,
a <= x < b ->
P x ->
min_nat_cond P a b != None.
Proof.
intros P a b x LE HOLDS.
apply seq_argmin_exists with (x0 := x).
by rewrite mem_filter mem_values_between HOLDS LE.
Qed.
Lemma min_nat_cond_in_seq: Lemma min_nat_cond_in_seq:
forall P a b x, forall P a b x,
min_nat_cond P a b = Some x -> min_nat_cond P a b = Some x ->
...@@ -465,6 +476,17 @@ Section MinMaxSeq. ...@@ -465,6 +476,17 @@ Section MinMaxSeq.
by rewrite mem_filter Py andTb mem_values_between. by rewrite mem_filter Py andTb mem_values_between.
Qed. Qed.
Lemma max_nat_cond_exists:
forall (P: nat -> bool) (a b: nat) x,
a <= x < b ->
P x ->
max_nat_cond P a b != None.
Proof.
intros P a b x LE HOLDS.
apply seq_argmax_exists with (x0 := x).
by rewrite mem_filter mem_values_between HOLDS LE.
Qed.
Lemma max_nat_cond_in_seq: Lemma max_nat_cond_in_seq:
forall P a b x, forall P a b x,
max_nat_cond P a b = Some x -> max_nat_cond P a b = Some x ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment