Library probsa.util.misc
(* --------------------------- Reals and SSReflect -------------------------- *)
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype.
(* --------------------------------- Prosa ---------------------------------- *)
From prosa.util Require Import list.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export boolp.
Local Open Scope nat_scope.
(* ---------------------------------- Main ---------------------------------- *)
Definition min_option (xs : seq nat) : option nat :=
match xs with
| [::] ⇒ None
| h::tl ⇒ Some (foldl minn h tl)
end.
Definition min_default (d : nat) (xs : seq nat) : nat := foldl minn d xs.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype.
(* --------------------------------- Prosa ---------------------------------- *)
From prosa.util Require Import list.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export boolp.
Local Open Scope nat_scope.
(* ---------------------------------- Main ---------------------------------- *)
Definition min_option (xs : seq nat) : option nat :=
match xs with
| [::] ⇒ None
| h::tl ⇒ Some (foldl minn h tl)
end.
Definition min_default (d : nat) (xs : seq nat) : nat := foldl minn d xs.
We prove that any monotone function f : nat → bool falls into one of
the following cases:
(1) f n is false for any n,
(2) there exists t0 such that ∀ t, t > t0 ↔ f t,
(3) or f n is always true.
We note that this lemma uses the classical excluded middle axiom
∀ P : Prop, P ∨ ¬ P.