From 93a35165079204b57d5e28a22781de18beb9f446 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 24 Feb 2014 18:07:48 +0100 Subject: Pos.compare_cont takes the comparison as first argument Helps cbn tactic refolding --- theories/PArith/BinPos.v | 28 ++++++++++++++-------------- theories/PArith/BinPosDef.v | 12 ++++++------ theories/PArith/Pnat.v | 10 +++++----- 3 files changed, 25 insertions(+), 25 deletions(-) (limited to 'theories/PArith') diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 7f478546e..d576c3eb4 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -766,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 @@ -785,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. @@ -874,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; @@ -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)). diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 61bee69f8..6674943a6 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -255,20 +255,20 @@ Fixpoint size p := (** ** Comparison on binary positive numbers *) -Fixpoint compare_cont (x y:positive) (r:comparison) {struct y} : comparison := +Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison := match x, y with - | p~1, q~1 => compare_cont p q r - | p~1, q~0 => compare_cont p q Gt + | p~1, q~1 => compare_cont r p q + | p~1, q~0 => compare_cont Gt p q | p~1, 1 => Gt - | p~0, q~1 => compare_cont p q Lt - | p~0, q~0 => compare_cont p q r + | p~0, q~1 => compare_cont Lt p q + | p~0, q~0 => compare_cont r p q | p~0, 1 => Gt | 1, q~1 => Lt | 1, q~0 => Lt | 1, 1 => r end. -Definition compare x y := compare_cont x y Eq. +Definition compare x y := compare_cont Eq x y. Infix "?=" := compare (at level 70, no associativity) : positive_scope. diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 33505ccb3..12042f76c 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -410,24 +410,24 @@ Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3"). Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3"). Lemma nat_of_P_minus_morphism p q : - Pos.compare_cont p q Eq = Gt -> + Pos.compare_cont Eq p q = Gt -> Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q. Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)). Lemma nat_of_P_lt_Lt_compare_morphism p q : - Pos.compare_cont p q Eq = Lt -> Pos.to_nat p < Pos.to_nat q. + Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q. Proof (proj1 (Pos2Nat.inj_lt p q)). Lemma nat_of_P_gt_Gt_compare_morphism p q : - Pos.compare_cont p q Eq = Gt -> Pos.to_nat p > Pos.to_nat q. + Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q. Proof (proj1 (Pos2Nat.inj_gt p q)). Lemma nat_of_P_lt_Lt_compare_complement_morphism p q : - Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont p q Eq = Lt. + Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt. Proof (proj2 (Pos2Nat.inj_lt p q)). Definition nat_of_P_gt_Gt_compare_complement_morphism p q : - Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont p q Eq = Gt. + Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt. Proof (proj2 (Pos2Nat.inj_gt p q)). (** Old intermediate results about [Pmult_nat] *) -- cgit v1.2.3