diff options
Diffstat (limited to 'theories/PArith/BinPos.v')
-rw-r--r-- | theories/PArith/BinPos.v | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 5129a3ca..921e2d67 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -23,8 +23,6 @@ Require Export BinPosDef. are now defined in [BinNums.v] *) Local Open Scope positive_scope. -Local Unset Boolean Equality Schemes. -Local Unset Case Analysis Schemes. (** Every definitions and early properties about positive numbers are placed in a module [Pos] for qualification purpose. *) @@ -578,21 +576,21 @@ Qed. Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B), (forall a, f (g a) = h (f a)) -> forall p a, - f (iter p g a) = iter p h (f a). + f (iter g a p) = iter h (f a) p. Proof. induction p; simpl; intros; now rewrite ?H, ?IHp. Qed. Theorem iter_swap : forall p (A:Type) (f:A -> A) (x:A), - iter p f (f x) = f (iter p f x). + iter f (f x) p = f (iter f x p). Proof. intros. symmetry. now apply iter_swap_gen. Qed. Theorem iter_succ : forall p (A:Type) (f:A -> A) (x:A), - iter (succ p) f x = f (iter p f x). + iter f x (succ p) = f (iter f x p). Proof. induction p as [p IHp|p IHp|]; intros; simpl; trivial. now rewrite !IHp, iter_swap. @@ -600,7 +598,7 @@ Qed. Theorem iter_add : forall p q (A:Type) (f:A -> A) (x:A), - iter (p+q) f x = iter p f (iter q f x). + iter f x (p+q) = iter f (iter f x q) p. Proof. induction p using peano_ind; intros. now rewrite add_1_l, iter_succ. @@ -610,7 +608,7 @@ Qed. Theorem iter_invariant : forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop), (forall x:A, Inv x -> Inv (f x)) -> - forall x:A, Inv x -> Inv (iter p f x). + forall x:A, Inv x -> Inv (iter f x p). Proof. induction p as [p IHp|p IHp|]; simpl; trivial. intros A f Inv H x H0. apply H, IHp, IHp; trivial. @@ -651,7 +649,7 @@ Theorem sub_mask_carry_spec p q : sub_mask_carry p q = pred_mask (sub_mask p q). Proof. revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl; - try reflexivity; try rewrite IHp; + try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. @@ -768,15 +766,15 @@ Definition switch_Eq c c' := end. Lemma compare_cont_spec p q c : - compare_cont p q c = switch_Eq c (p ?= q). + compare_cont c p q = switch_Eq c (p ?= q). Proof. unfold compare. revert q c. induction p; destruct q; simpl; trivial. intros c. - rewrite 2 IHp. now destruct (compare_cont p q Eq). + rewrite 2 IHp. now destruct (compare_cont Eq p q). intros c. - rewrite 2 IHp. now destruct (compare_cont p q Eq). + rewrite 2 IHp. now destruct (compare_cont Eq p q). Qed. (** From this general result, we now describe particular cases @@ -787,31 +785,31 @@ Qed. *) Theorem compare_cont_Eq p q c : - compare_cont p q c = Eq -> c = Eq. + compare_cont c p q = Eq -> c = Eq. Proof. rewrite compare_cont_spec. now destruct (p ?= q). Qed. Lemma compare_cont_Lt_Gt p q : - compare_cont p q Lt = Gt <-> p > q. + compare_cont Lt p q = Gt <-> p > q. Proof. rewrite compare_cont_spec. unfold gt. destruct (p ?= q); now split. Qed. Lemma compare_cont_Lt_Lt p q : - compare_cont p q Lt = Lt <-> p <= q. + compare_cont Lt p q = Lt <-> p <= q. Proof. rewrite compare_cont_spec. unfold le. destruct (p ?= q); easy'. Qed. Lemma compare_cont_Gt_Lt p q : - compare_cont p q Gt = Lt <-> p < q. + compare_cont Gt p q = Lt <-> p < q. Proof. rewrite compare_cont_spec. unfold lt. destruct (p ?= q); now split. Qed. Lemma compare_cont_Gt_Gt p q : - compare_cont p q Gt = Gt <-> p >= q. + compare_cont Gt p q = Gt <-> p >= q. Proof. rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'. Qed. @@ -876,13 +874,13 @@ Qed. (** Basic facts about [compare_cont] *) Theorem compare_cont_refl p c : - compare_cont p p c = c. + compare_cont c p p = c. Proof. now induction p. Qed. Lemma compare_cont_antisym p q c : - CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c). + CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p. Proof. revert q c. induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl; @@ -1840,6 +1838,8 @@ Qed. End Pos. +Bind Scope positive_scope with Pos.t positive. + (** Exportation of notations *) Infix "+" := Pos.add : positive_scope. @@ -1903,7 +1903,7 @@ Notation Pdiv2 := Pos.div2 (compat "8.3"). Notation Pdiv2_up := Pos.div2_up (compat "8.3"). Notation Psize := Pos.size_nat (compat "8.3"). Notation Psize_pos := Pos.size (compat "8.3"). -Notation Pcompare := Pos.compare_cont (compat "8.3"). +Notation Pcompare x y m := (Pos.compare_cont m x y) (compat "8.3"). Notation Plt := Pos.lt (compat "8.3"). Notation Pgt := Pos.gt (compat "8.3"). Notation Ple := Pos.le (compat "8.3"). @@ -2062,11 +2062,11 @@ Lemma Pplus_one_succ_r p : Pos.succ p = p + 1. Proof (eq_sym (Pos.add_1_r p)). Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p. Proof (eq_sym (Pos.add_1_l p)). -Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq. +Lemma Pcompare_refl p : Pos.compare_cont Eq p p = Eq. Proof (Pos.compare_cont_refl p Eq). -Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q. +Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont Eq p q = Eq -> p = q. Proof Pos.compare_eq. -Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq). +Lemma ZC4 p q : Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p). Proof (Pos.compare_antisym q p). Lemma Ppred_minus p : Pos.pred p = p - 1. Proof (eq_sym (Pos.sub_1_r p)). |