Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

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.