Merge PR#279: A few lemmas about iff and about orders on positive and Z

5 files changed, 99 insertions, 5 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index ddaf08bf7..11d80dbc3 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -262,6 +262,11 @@ Inductive comparison : Set :=
   | Lt : comparison
   | Gt : comparison.
 
+Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
+Proof.
+  destruct c, c'; intro H; reflexivity || destruct H; discriminate.
+Qed.
+
 Definition CompOpp (r:comparison) :=
   match r with
     | Eq => Eq
@@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
  CompSpec eq lt x y c -> CompSpecT eq lt x y c.
 Proof. intros. apply CompareSpec2Type; assumption. Defined.
 
-
 (******************************************************************)
 (** * Misc Other Datatypes *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 85123cc44..fb1a7ab1c 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -125,6 +125,25 @@ Proof.
   [apply Hl | apply Hr]; assumption.
 Qed.
 
+Theorem imp_iff_compat_l : forall A B C : Prop,
+  (B <-> C) -> ((A -> B) <-> (A -> C)).
+Proof.
+  intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption.
+Qed.
+
+Theorem imp_iff_compat_r : forall A B C : Prop,
+  (B <-> C) -> ((B -> A) <-> (C -> A)).
+Proof.
+  intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption.
+Qed.
+
+Theorem not_iff_compat : forall A B : Prop,
+  (A <-> B) -> (~ A <-> ~B).
+Proof.
+  intros; apply imp_iff_compat_r; assumption.
+Qed.
+
+
 (** Some equivalences *)
 
 Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 7baf102aa..d6385ee31 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -813,6 +813,34 @@ Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
 
+Lemma compare_cont_Lt_not_Lt p q :
+  compare_cont Lt p q <> Lt <-> p > q.
+Proof.
+  rewrite compare_cont_Lt_Lt.
+  unfold gt, le, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
+Lemma compare_cont_Lt_not_Gt p q :
+  compare_cont Lt p q <> Gt <-> p <= q.
+Proof.
+  apply not_iff_compat, compare_cont_Lt_Gt.
+Qed.
+
+Lemma compare_cont_Gt_not_Lt p q :
+  compare_cont Gt p q <> Lt <-> p >= q.
+Proof.
+  apply not_iff_compat, compare_cont_Gt_Lt.
+Qed.
+
+Lemma compare_cont_Gt_not_Gt p q :
+  compare_cont Gt p q <> Gt <-> p < q.
+Proof.
+  rewrite compare_cont_Gt_Gt.
+  unfold ge, lt, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
 (** We can express recursive equations for [compare] *)
 
 Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q).
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 5aa397f8a..1e3ab6687 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
 Proof. apply Z.testbit_Zpos. Qed.
 
-(** Some results concerning Z.neg *)
+(** Some results concerning Z.neg and Z.pos *)
 
 Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q.
 Proof. now injection 1. Qed.
@@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed.
 Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q.
 Proof. split. apply inj_neg. intros; now f_equal. Qed.
 
+Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q.
+Proof. now injection 1. Qed.
+
+Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q.
+Proof. split. apply inj_pos. intros; now f_equal. Qed.
+
 Lemma neg_is_neg p : Z.neg p < 0.
 Proof. reflexivity. Qed.
 
 Lemma neg_is_nonpos p : Z.neg p <= 0.
 Proof. easy. Qed.
 
+Lemma pos_is_pos p : 0 < Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_is_nonneg p : 0 <= Z.pos p.
+Proof. easy. Qed.
+
+Lemma neg_le_pos p q : Zneg p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_lt_pos p q : Zneg p < Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q.
+Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q.
+Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q.
+Proof. easy. Qed.
+
 Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p.
 Proof. reflexivity. Qed.
 
 Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1.
 Proof. reflexivity. Qed.
 
+Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1.
+Proof. reflexivity. Qed.
+
 Lemma opp_neg p : - Z.neg p = Z.pos p.
 Proof. reflexivity. Qed.
 
@@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed.
 Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.
 Proof. reflexivity. Qed.
 
+Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q).
+Proof. reflexivity. Qed.
+
 Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).
 Proof. apply Z.divide_Zpos_Zneg_r. Qed.
 
@@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n ->
  Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).
 Proof. apply Z.testbit_Zneg. Qed.
 
+Lemma testbit_pos a n : 0<=n ->
+ Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
+Proof. apply Z.testbit_Zpos. Qed.
+
 End Pos2Z.
 
 Module Z2Pos.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 73dee0cf2..18915216a 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
-  easy.
+  exact Pos2Z.neg_le_pos.
 Qed.
 
 Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.
@@ -350,12 +350,12 @@ Qed.
 (* weaker but useful (in [Z.pow] for instance) *)
 Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
 Proof.
- easy.
+  exact Pos2Z.pos_is_nonneg.
 Qed.
 
 Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.
 Proof.
- easy.
+  exact Pos2Z.neg_is_neg.
 Qed.
 
 Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.