diff options
Diffstat (limited to 'theories/NArith/Ndist.v')
| -rw-r--r-- | theories/NArith/Ndist.v | 110 |
1 files changed, 54 insertions, 56 deletions
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 586c1114..ce4f7663 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndist.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Arith. Require Import Min. Require Import BinPos. @@ -35,12 +33,12 @@ Definition Nplength (a:N) := Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0. Proof. simple induction a; trivial. - unfold Nplength in |- *; intros; discriminate H. + unfold Nplength; intros; discriminate H. Qed. Lemma Nplength_zeros : forall (a:N) (n:nat), - Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false. + Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false. Proof. simple induction a; trivial. simple induction p. simple induction n. intros. inversion H1. @@ -48,33 +46,33 @@ Proof. intros. simpl in H1. discriminate H1. simple induction k. trivial. generalize H0. case n. intros. inversion H3. - intros. simpl in |- *. unfold Nbit in H. apply (H n0). simpl in H1. inversion H1. reflexivity. + intros. simpl. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity. exact (lt_S_n n1 n0 H3). - simpl in |- *. intros n H. inversion H. intros. inversion H0. + simpl. intros n H. inversion H. intros. inversion H0. Qed. Lemma Nplength_one : - forall (a:N) (n:nat), Nplength a = ni n -> Nbit a n = true. + forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true. Proof. simple induction a. intros. inversion H. simple induction p. intros. simpl in H0. inversion H0. reflexivity. - intros. simpl in H0. inversion H0. simpl in |- *. unfold Nbit in H. apply H. reflexivity. + intros. simpl in H0. inversion H0. simpl. unfold N.testbit_nat in H. apply H. reflexivity. intros. simpl in H. inversion H. reflexivity. Qed. Lemma Nplength_first_one : forall (a:N) (n:nat), - (forall k:nat, k < n -> Nbit a k = false) -> - Nbit a n = true -> Nplength a = ni n. + (forall k:nat, k < n -> N.testbit_nat a k = false) -> + N.testbit_nat a n = true -> Nplength a = ni n. Proof. simple induction a. intros. simpl in H0. discriminate H0. simple induction p. intros. generalize H0. case n. intros. reflexivity. - intros. absurd (Nbit (Npos (xI p0)) 0 = false). trivial with bool. + intros. absurd (N.testbit_nat (Npos (xI p0)) 0 = false). trivial with bool. auto with bool arith. intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. - intros. simpl in |- *. unfold Nplength in H. + intros. simpl. unfold Nplength in H. cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity. - apply H. intros. change (Nbit (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4. + apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4. exact H3. intro. case n. trivial. intros. simpl in H0. discriminate H0. @@ -92,10 +90,10 @@ Definition ni_min (d d':natinf) := Lemma ni_min_idemp : forall d:natinf, ni_min d d = d. Proof. simple induction d; trivial. - unfold ni_min in |- *. + unfold ni_min. simple induction n; trivial. intros. - simpl in |- *. + simpl. inversion H. rewrite H1. rewrite H1. @@ -107,7 +105,7 @@ Proof. simple induction d. simple induction d'; trivial. simple induction d'; trivial. elim n. simple induction n0; trivial. intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). - intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity. + intro. unfold ni_min. simpl. rewrite H1. reflexivity. cut (ni (min n0 n2) = ni (min n2 n0)). intros. inversion H1; trivial. exact (H n2). @@ -118,11 +116,11 @@ Lemma ni_min_assoc : Proof. simple induction d; trivial. simple induction d'; trivial. simple induction d''; trivial. - unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)). + unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)). intro. rewrite H. reflexivity. generalize n0 n1. elim n; trivial. simple induction n3; trivial. simple induction n5; trivial. - intros. simpl in |- *. auto. + intros. simpl. auto. Qed. Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0. @@ -154,42 +152,42 @@ Qed. Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'. Proof. - unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. + unfold ni_le. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. Qed. Lemma ni_le_trans : forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''. Proof. - unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. + unfold ni_le. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. Qed. Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d. Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. + unfold ni_le. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. Qed. Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'. Proof. - unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. + unfold ni_le. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. Qed. Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. Proof. simple induction d. intro. right. exact (ni_min_inf_l d'). simple induction d'. left. exact (ni_min_inf_r (ni n)). - unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). + unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). intros. case (H n0). intro. left. rewrite H0. reflexivity. intro. right. rewrite H0. reflexivity. elim n. intro. left. reflexivity. simple induction n1. right. reflexivity. - intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity. - intro. right. simpl in |- *. rewrite H1. reflexivity. + intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity. + intro. right. simpl. rewrite H1. reflexivity. Qed. Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case. + unfold ni_le. intros. rewrite (ni_min_comm d' d). apply ni_min_case. Qed. Lemma ni_le_min_induc : @@ -203,7 +201,7 @@ Proof. apply ni_le_antisym. apply H1. apply ni_le_refl. exact H2. exact H. - intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2. + intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le. rewrite ni_min_comm. exact H2. apply ni_le_refl. exact H0. Qed. @@ -211,40 +209,40 @@ Qed. Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). Proof. cut (forall m n:nat, m <= n -> min m n = m). - intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity. + intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity. simple induction m. trivial. simple induction n0. intro. inversion H0. - intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. + intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. Qed. Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. Proof. - unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r. + unfold ni_le. unfold ni_min. intros. inversion H. apply le_min_r. Qed. Lemma Nplength_lb : forall (a:N) (n:nat), - (forall k:nat, k < n -> Nbit a k = false) -> ni_le (ni n) (Nplength a). + (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a). Proof. simple induction a. intros. exact (ni_min_inf_r (ni n)). - intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial. - intro. absurd (Nbit (Npos p) (Pplength p) = false). + intros. unfold Nplength. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial. + intro. absurd (N.testbit_nat (Npos p) (Pplength p) = false). rewrite (Nplength_one (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p)))). + (eq_refl (Nplength (Npos p)))). discriminate. apply H. exact H0. Qed. Lemma Nplength_ub : - forall (a:N) (n:nat), Nbit a n = true -> ni_le (Nplength a) (ni n). + forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n). Proof. simple induction a. intros. discriminate H. - intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial. - intro. absurd (Nbit (Npos p) n = true). + intros. unfold Nplength. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial. + intro. absurd (N.testbit_nat (Npos p) n = true). rewrite (Nplength_zeros (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p))) n H0). + (eq_refl (Nplength (Npos p))) n H0). discriminate. exact H. Qed. @@ -257,26 +255,26 @@ Qed. Instead of working with $d$, we work with $pd$, namely [Npdist]: *) -Definition Npdist (a a':N) := Nplength (Nxor a a'). +Definition Npdist (a a':N) := Nplength (N.lxor a a'). (** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that $pd(a,a')=infty$ iff $a=a'$: *) Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty. Proof. - intros. unfold Npdist in |- *. rewrite Nxor_nilpotent. reflexivity. + intros. unfold Npdist. rewrite N.lxor_nilpotent. reflexivity. Qed. Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'. Proof. - intros. apply Nxor_eq. apply Nplength_infty. exact H. + intros. apply N.lxor_eq. apply Nplength_infty. exact H. Qed. (** $d$ is a distance, so $d(a,a')=d(a',a)$: *) Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a. Proof. - unfold Npdist in |- *. intros. rewrite Nxor_comm. reflexivity. + unfold Npdist. intros. rewrite N.lxor_comm. reflexivity. Qed. (** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq @@ -294,21 +292,21 @@ Qed. Lemma Nplength_ultra_1 : forall a a':N, ni_le (Nplength a) (Nplength a') -> - ni_le (Nplength a) (Nplength (Nxor a a')). + ni_le (Nplength a) (Nplength (N.lxor a a')). Proof. simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H. rewrite (ni_min_inf_l (Nplength a')) in H. - rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl. - intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros. - cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false). + rewrite (Nplength_infty a' H). simpl. apply ni_le_refl. + intros. unfold Nplength at 1. apply Nplength_lb. intros. + cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). intros. apply H1. reflexivity. intro a''. case a''. intro. reflexivity. - intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). unfold xorf in |- *. + intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p))) k H0). + (eq_refl (Nplength (Npos p))) k H0). generalize H. case a'. trivial. - intros. cut (Nbit (Npos p1) k = false). intros. rewrite H3. reflexivity. + intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity. apply Nplength_zeros with (n := Pplength p1). reflexivity. apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0. apply ni_le_le. exact H2. @@ -316,14 +314,14 @@ Qed. Lemma Nplength_ultra : forall a a':N, - ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (Nxor a a')). + ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')). Proof. intros. case (ni_le_total (Nplength a) (Nplength a')). intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a). intro. rewrite H0. apply Nplength_ultra_1. exact H. exact H. intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a'). - intro. rewrite H0. rewrite Nxor_comm. apply Nplength_ultra_1. exact H. + intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H. rewrite ni_min_comm. exact H. Qed. @@ -331,8 +329,8 @@ Lemma Npdist_ultra : forall a a' a'':N, ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a'). Proof. - intros. unfold Npdist in |- *. cut (Nxor (Nxor a a'') (Nxor a'' a') = Nxor a a'). + intros. unfold Npdist. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a'). intro. rewrite <- H. apply Nplength_ultra. - rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent. - rewrite Nxor_neutral_left. reflexivity. -Qed.
\ No newline at end of file + rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent. + rewrite N.lxor_0_l. reflexivity. +Qed. |