Library aux

Require Export LibTactics LibReflect LibRelation LibNat LibVar LibList LibListSorted LibFset Morphisms LibListExt LibFsetExt Utf8.

Fixpoint lt_dec (m n : nat) :=
  match m, n with
    | O, O ⇒ false
    | O, S _ ⇒ true
    | S _, O ⇒ false
    | S m´, S n´ ⇒ lt_dec m´ n´
  end.

Instance lt_decidable : ∀ (m n : nat), Decidable (m<n).
Proof. intros. applys¬ decidable_make (lt_dec m n).
  gen n. induction m; intros; destruct n; simpl.
  symmetry. apply¬ isTrue_false. nat_math.
  symmetry. apply¬ isTrue_true. nat_math.
  symmetry. apply¬ isTrue_false. nat_math.
  asserts_rewrite ((S m < S n) = (m < n)).
    extens. iff; nat_math.
  auto.
Qed.

Lemma min_same: ∀ n, (min n n) = n.
Proof.
  induction n; simpls¬.
Qed.

Hint Resolve min_same.

Definition max (m n : nat) := ifb (m < n) then n else m.

Lemma max0 : ∀ m n, max m n = 0 → m = 0 ∧ n = 0.
Proof.
  introv H. unfolds in H; cases_if~; nat_math.
Qed.

Lemma max0neutrall : ∀ m, max 0 m = m.
Proof.
  introv. unfolds. cases_if; nat_math.
Qed.

Lemma max0neutralr : ∀ m, max m 0 = m.
Proof.
  introv. unfolds. cases_if; nat_math.
Qed.

Lemma maxcomm : ∀ m n, max m n = max n m.
Proof.
  introv. unfolds; cases_if; cases_if~; nat_math.
Qed.

Lemma maxassoc : ∀ m n p, max m (max n p) = max (max m n) p.
Proof.
  introv. unfolds; repeat cases_if~; nat_math.
Qed.