summaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /theories/Arith
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Compare_dec.v138
-rw-r--r--theories/Arith/Div2.v24
2 files changed, 160 insertions, 2 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 3a87ee1a..d2eead86 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Compare_dec.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Compare_dec.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
Require Import Le.
Require Import Lt.
@@ -105,3 +105,139 @@ Qed.
Theorem not_lt : forall n m, ~ n < m -> n >= m.
intros x y H; exact (not_gt y x H).
Qed.
+
+
+(** A ternary comparison function in the spirit of [Zcompare]. *)
+
+Definition nat_compare (n m:nat) :=
+ match lt_eq_lt_dec n m with
+ | inleft (left _) => Lt
+ | inleft (right _) => Eq
+ | inright _ => Gt
+ end.
+
+Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m.
+Proof.
+ unfold nat_compare; intros.
+ simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto.
+Qed.
+
+Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
+Proof.
+ induction n; destruct m; simpl; auto.
+ unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H];
+ auto; intros; try discriminate.
+ unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H];
+ auto; intros; try discriminate.
+ rewrite nat_compare_S; auto.
+Qed.
+
+Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.
+Proof.
+ induction n; destruct m; simpl.
+ unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
+ split; auto with arith.
+ split; [inversion 1 |].
+ unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H];
+ auto; intros; try discriminate.
+ rewrite nat_compare_S.
+ generalize (IHn m); clear IHn; intuition.
+Qed.
+
+Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt.
+Proof.
+ induction n; destruct m; simpl.
+ unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
+ split; [inversion 1 |].
+ unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H];
+ auto; intros; try discriminate.
+ split; auto with arith.
+ rewrite nat_compare_S.
+ generalize (IHn m); clear IHn; intuition.
+Qed.
+
+Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt.
+Proof.
+ split.
+ intros.
+ intro.
+ destruct (nat_compare_gt n m).
+ generalize (le_lt_trans _ _ _ H (H2 H0)).
+ exact (lt_irrefl n).
+ intros.
+ apply not_gt.
+ swap H.
+ destruct (nat_compare_gt n m); auto.
+Qed.
+
+Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt.
+Proof.
+ split.
+ intros.
+ intro.
+ destruct (nat_compare_lt n m).
+ generalize (le_lt_trans _ _ _ H (H2 H0)).
+ exact (lt_irrefl m).
+ intros.
+ apply not_lt.
+ swap H.
+ destruct (nat_compare_lt n m); auto.
+Qed.
+
+(** A boolean version of [le] over [nat]. *)
+
+Fixpoint leb (m:nat) : nat -> bool :=
+ match m with
+ | O => fun _:nat => true
+ | S m' =>
+ fun n:nat => match n with
+ | O => false
+ | S n' => leb m' n'
+ end
+ end.
+
+Lemma leb_correct : forall m n:nat, m <= n -> leb m n = true.
+Proof.
+ induction m as [| m IHm]. trivial.
+ destruct n. intro H. elim (le_Sn_O _ H).
+ intros. simpl in |- *. apply IHm. apply le_S_n. assumption.
+Qed.
+
+Lemma leb_complete : forall m n:nat, leb m n = true -> m <= n.
+Proof.
+ induction m. trivial with arith.
+ destruct n. intro H. discriminate H.
+ auto with arith.
+Qed.
+
+Lemma leb_correct_conv : forall m n:nat, m < n -> leb n m = false.
+Proof.
+ intros.
+ generalize (leb_complete n m).
+ destruct (leb n m); auto.
+ intros.
+ elim (lt_irrefl _ (lt_le_trans _ _ _ H (H0 (refl_equal true)))).
+Qed.
+
+Lemma leb_complete_conv : forall m n:nat, leb n m = false -> m < n.
+Proof.
+ intros. elim (le_or_lt n m). intro. conditional trivial rewrite leb_correct in H. discriminate H.
+ trivial.
+Qed.
+
+Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt.
+Proof.
+ induction n; destruct m; simpl.
+ unfold nat_compare; simpl.
+ intuition; discriminate.
+ split; auto with arith.
+ unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H];
+ intuition; try discriminate.
+ inversion H.
+ split; try (intros; discriminate).
+ unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H];
+ intuition; try discriminate.
+ inversion H.
+ rewrite nat_compare_S; auto.
+Qed.
+
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 6e5d292f..ca1f39af 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Div2.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Div2.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
Require Import Lt.
Require Import Plus.
@@ -173,3 +173,25 @@ Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
Proof.
intros n H. exists (div2 n). auto with arith.
Qed.
+
+(** Doubling before dividing by two brings back to the initial number. *)
+
+Lemma div2_double : forall n:nat, div2 (2*n) = n.
+Proof.
+ induction n.
+ simpl; auto.
+ simpl.
+ replace (n+S(n+0)) with (S (2*n)).
+ f_equal; auto.
+ simpl; auto with arith.
+Qed.
+
+Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n.
+Proof.
+ induction n.
+ simpl; auto.
+ simpl.
+ replace (n+S(n+0)) with (S (2*n)).
+ f_equal; auto.
+ simpl; auto with arith.
+Qed.