aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Init/Datatypes.v6
-rw-r--r--theories/Init/Logic.v19
-rw-r--r--theories/PArith/BinPos.v28
-rw-r--r--theories/ZArith/BinInt.v45
-rw-r--r--theories/ZArith/Zorder.v6
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.