Permalink
Browse files

Implemented the bit shift operations on ZType_integers using Pierre's…

… new implementations in Zsig. Introduced the notion of notion of order preserving maps. Cancellation on rings revised.
  • Loading branch information...
1 parent b21e0c3 commit 5ecc59d4c539479e9509cee7c93c0caa09df4cde @robbertkrebbers robbertkrebbers committed Dec 7, 2010
View
@@ -7,3 +7,5 @@ src/deps
src/.sconsign.dblite
coqidescript
coqdoc
+*#
+
View
@@ -1,6 +1,6 @@
Compilation
- Known to compile with Coq trunk 13650.
+ Known to compile with Coq trunk 13689.
Warning: This development assumes a case sensitive file system.
@@ -123,14 +123,14 @@ Lemma to_Z_sr_precedes_Zle x y : x ≤ y → (to_Z x <= to_Z y)%Z.
Proof.
intro E.
apply signed_binary_positive_integers.sr_precedes_Zle.
- apply (integers.preserve_sr_order to_Z). assumption.
+ pose proof (order_preserving to_Z). auto.
Qed.
Lemma to_Z_Zle_sr_precedes x y : (to_Z x <= to_Z y)%Z → x ≤ y.
Proof.
intro.
rewrite <-(jections.surjective_applied' of_Z x), <-(jections.surjective_applied' of_Z y).
- apply (integers.preserve_sr_order of_Z).
+ apply (order_preserving of_Z).
apply signed_binary_positive_integers.Zle_sr_precedes. assumption.
Qed.
@@ -156,15 +156,15 @@ Program Instance: ∀ x y: t, Decision (x ≤ y) := λ x y, match (compare x y)
Next Obligation.
rewrite spec_compare in *.
destruct (Zcompare_spec (to_Z x) (to_Z y)); try discriminate.
- apply orders.not_precedes_precedes_neq.
+ apply orders.not_precedes_strictly_precedes.
apply to_Z_Zlt_sr_precedes. assumption.
Qed.
Next Obligation with intuition.
rewrite spec_compare in *.
destruct (Zcompare_spec (to_Z x) (to_Z y)); try discriminate...
apply to_Z_Zle_sr_precedes, Zeq_le...
- apply orders.precedes_neq_weaken, to_Z_Zlt_sr_precedes...
+ apply orders.strictly_precedes_weaken, to_Z_Zlt_sr_precedes...
Qed.
Program Instance: IntAbs t (Pos t) := abs.
@@ -262,4 +262,20 @@ Next Obligation with auto.
rewrite ZType_succ_plus_1, commutativity in E2...
Qed.
+(* Efficient shiftl *)
+Program Instance: ShiftLeft t (Pos t) := λ x y, shiftl x y.
+Next Obligation.
+ intros x [y Ey].
+ unfold additional_operations.pow, nat_pow, nat_pow_sig, ZType_pow.
+ unfold_equiv. simpl.
+ rewrite rings.preserves_mult, spec_pow.
+ rewrite spec_shiftl, Z.shiftl_mul_pow2.
+ rewrite <-ZType_two_2, spec_2. reflexivity.
+ apply to_Z_sr_precedes_Zle in Ey. rewrite preserves_0 in Ey. assumption.
+Qed.
+(* This proof could possibly be much shorter by using the correctness of shiftl on Z *)
+
+Program Instance: ShiftRight t (Pos t) := λ x y, shiftr x y.
+Next Obligation. Admitted.
+
End ZType_Integers.
@@ -388,7 +388,7 @@ Section dyadics.
Next Obligation with intuition.
intros E.
apply (shiftl_nonzero 1 n).
- apply not_symmetry. apply zero_ne_one.
+ apply (ne_zero 1).
apply (injective ZtoQ).
rewrite rings.preserves_0...
Qed.
@@ -7,54 +7,3 @@ Module BigZ_Integers := ZType_Integers BigZ.
Definition fastZ: Type := BigZ.t.
-(* The following definition and lemma should be added to stdlib *)
-Definition fastZ_shiftl (p x : fastZ) :=
- match p with
- | BigZ.Pos p => match x with
- | BigZ.Pos x => BigZ.Pos (BigN.shiftl p x)
- | BigZ.Neg x => BigZ.Neg (BigN.shiftl p x)
- end
- | BigZ.Neg p => x
- end.
-
-Lemma BigN_neg_is_zero p : (BigZ.le 0 (BigZ.Neg p) -> BigN.to_Z p = 0)%Z.
-Proof.
- intros E.
- apply Zle_antisym.
- apply Z.opp_nonneg_nonpos. trivial.
- apply BigN.spec_pos.
-Qed.
-
-Lemma spec_shiftl (p x : fastZ) : (BigZ.le 0 p -> BigZ.to_Z (fastZ_shiftl p x) = BigZ.to_Z x * 2 ^(BigZ.to_Z p))%Z.
-Proof with auto.
- intros E. case_eq p; intros p' Ep'.
- case_eq x; intros x' Ex'; simpl.
- apply BigN.spec_shiftl.
- rewrite BigN.spec_shiftl. rewrite Z.mul_opp_l. reflexivity.
- subst. simpl. rewrite (BigN_neg_is_zero p')...
- simpl. rewrite Z.mul_1_r. reflexivity.
-Qed.
-
-Program Instance: ShiftLeft fastZ (Pos fastZ) := λ x y, fastZ_shiftl y x.
-Next Obligation.
- intros x y.
- BigZ_Integers.unfold_equiv.
- rewrite spec_shiftl.
- rewrite rings.preserves_mult.
- unfold pow, nat_pow, nat_pow_sig, BigZ_Integers.ZType_pow. simpl.
- rewrite BigZ.spec_pow.
- reflexivity.
- apply BigZ_Integers.to_Z_sr_precedes_Zle. destruct y. trivial.
-Qed.
-
-Definition fastZ_shiftr (p x : fastZ) :=
- match p with
- | BigZ.Pos p => match x with
- | BigZ.Pos x => BigZ.Pos (BigN.shiftr p x)
- | BigZ.Neg x => BigZ.Neg (BigN.shiftr p x)
- end
- | BigZ.Neg p => x
- end.
-
-Program Instance: ShiftRight fastZ (Pos fastZ) := λ x y, fastZ_shiftr y x.
-Next Obligation. Admitted.
@@ -46,7 +46,7 @@ Proof.
intros x. unfold id, compose, inverse, fastZ_to_fastQ.
destruct x as [x | x y]; simpl.
rewrite rings.preserves_1. field.
- apply not_symmetry. apply zero_ne_one.
+ apply (ne_zero 1).
unfold equiv, BigQ_Rationals.qev, BigQ.eq.
rewrite rings.preserves_mult, fields.preserves_dec_mult_inv,
@@ -24,7 +24,7 @@ Instance: Transitive frac_equiv.
Proof with auto.
unfold frac_equiv. intros [] [] [] V W.
simpl in *.
- apply (left_cancellation ring_mult den1)...
+ apply (left_cancellation_ne_zero ring_mult den1)...
do 2 rewrite associativity.
do 2 rewrite (commutativity den1).
rewrite V, <- W. ring.
@@ -38,7 +38,7 @@ Global Instance: ∀ x y: Frac, Decision (x = y) := λ x y, decide (num x * den
(* injection from R *)
Program Definition inject (r: R): Frac := frac r 1 _.
-Next Obligation. intro E. symmetry in E. apply zero_ne_one. assumption. Qed.
+Next Obligation. intro E. apply (ne_zero 1). assumption. Qed.
Instance: Proper (equiv ==> equiv) inject.
Proof. unfold inject, equiv, frac_equiv. intros x x' E. simpl. rewrite E. reflexivity. Qed.
@@ -127,9 +127,9 @@ Qed.
Global Instance: Field Frac.
Proof.
constructor; try apply _.
- unfold ZeroNeOne, equiv, frac_equiv.
+ unfold NeZero, equiv, frac_equiv.
simpl. do 2 rewrite mult_1_r.
- apply zero_ne_one.
+ apply (ne_zero 1).
unfold mult_inv, frac_inv, equiv, frac_equiv. intro. simpl. ring.
Qed.
@@ -214,7 +214,7 @@ Qed.
Next Obligation with auto.
case (decide (`x ≤ `y)); intros E; split; intros F.
rewrite left_identity. apply (antisymmetry (≤))...
- apply orders.precedes_neq_weaken... apply ZPos_int_nat_precedes...
+ apply orders.strictly_precedes_weaken... apply ZPos_int_nat_precedes...
reflexivity.
unfold equiv, ZPos_equiv. simpl.
rewrite rings.ring_minus_correct, <-associativity, rings.plus_opp_l, right_identity. reflexivity.
@@ -19,11 +19,11 @@ Instance: GroupInv BinInt.Z := BinInt.Zopp.
(* some day we'd like to do this with [Existing Instance] *)
(* propers: *)
-Instance: Proper (equiv ==> equiv ==> equiv) BinInt.Zplus.
+Instance: Proper ((=) ==> (=) ==> (=)) BinInt.Zplus.
Proof. unfold equiv, z_equiv. repeat intro. subst. reflexivity. Qed.
-Instance: Proper (equiv ==> equiv ==> equiv) BinInt.Zmult.
+Instance: Proper ((=) ==> (=) ==> (=)) BinInt.Zmult.
Proof. unfold equiv, z_equiv. repeat intro. subst. reflexivity. Qed.
-Instance: Proper (equiv ==> equiv) BinInt.Zopp.
+Instance: Proper ((=) ==> (=)) BinInt.Zopp.
Proof. unfold equiv, z_equiv. repeat intro. subst. reflexivity. Qed.
(* properties: *)
@@ -242,4 +242,12 @@ Next Obligation with try reflexivity; auto with zarith.
intros x1 n1. rewrite preserves_plus, preserves_1.
rewrite <-(Z.pow_1_r x1) at 2. apply Z.pow_add_r...
destruct n1. simpl. apply sr_precedes_Zle...
-Qed.
+Qed.
+
+(* Efficient shiftl *)
+Program Instance: ShiftLeft Z (Pos Z) := λ x y, Z.shiftl x y.
+Next Obligation.
+ intros x [y Ey].
+ apply Z.shiftl_mul_pow2.
+ simpl. apply sr_precedes_Zle. assumption.
+Qed.
@@ -64,7 +64,7 @@ Section upper_classes.
Class IntegralDomain: Prop :=
{ intdom_ring: Ring
- ; intdom_nontrivial:> ZeroNeOne A
+ ; intdom_nontrivial:> NeZero (1:A)
; intdom_nozeroes:> NoZeroDivisors A }.
(* For a strange reason Ring instances of Integers are sometimes obtained by
@@ -76,7 +76,7 @@ Section upper_classes.
Class Field {mult_inv: MultInv A}: Prop :=
{ field_ring:> Ring
- ; field_0neq1:> ZeroNeOne A
+ ; field_0neq1:> NeZero (1:A)
; mult_inv_proper:> Proper (sig_relation (=) _ ==> (=)) mult_inv
; mult_inverse: `(` x * // x = 1) }.
@@ -90,17 +90,14 @@ Implicit Arguments mult_inverse [[A] [e] [plus] [mult] [zero] [one] [inv] [mult_
Implicit Arguments sg_mor [[A] [e] [op] [SemiGroup]].
Section cancellation.
- Context `{e : Equiv A} (Rel : relation A) (P : A → Prop) (op : A → A → A).
+ Context `{e : Equiv A} (op : A → A → A) (z : A).
Class LeftCancellation :=
- left_cancellation : ∀ z, P z → ∀ {x y}, Rel (op z x) (op z y)Rel x y.
+ left_cancellation : `(op z x = op z y → x = y).
Class RightCancellation :=
- right_cancellation : ∀ z, P z → ∀ {x y}, Rel (op x z) (op y z)Rel x y.
+ right_cancellation : `(op x z = op y z → x = y).
End cancellation.
-Implicit Arguments left_cancellation [[A] [Rel] [P] [LeftCancellation] [x] [y]].
-Implicit Arguments right_cancellation [[A] [Rel] [P] [RightCancellation] [x] [y]].
-
Class PartialOrder `{e: Equiv A} (R: Order A): Prop :=
{ poset_setoid :> Equivalence e (* Setoid A introduces instance resolution bugs, todo: investigate *)
; poset_proper:> Proper (e ==> e ==> iff) R
@@ -217,3 +214,30 @@ Section jections.
End jections.
Implicit Arguments injective [[A] [ea] [B] [eb] [Injective]].
+
+Section order_maps.
+
+ Context `{Equiv A} `{oA : Order A} `{Equiv B} `{oB : Order B} (f : A → B).
+
+ (* It makes sense to require these maps to be [Setoid_Morphism]s, however,
+ Coq will become horribly slow then *)
+ Class OrderPreserving :=
+ { order_preserving : `(x ≤ y → f x ≤ f y)
+ ; order_preserving_proper_a :> Proper ((=) ==> (=) ==> iff) oA
+ ; order_preserving_proper_b :> Proper ((=) ==> (=) ==> iff) oB }.
+
+ Class OrderPreservingBack :=
+ { order_preserving_back : `(f x ≤ f y → x ≤ y)
+ ; order_preserving_back_proper_a :> Proper ((=) ==> (=) ==> iff) oA
+ ; order_preserving_back_proper_b :> Proper ((=) ==> (=) ==> iff) oB }.
+
+ Class OrderEmbedding :=
+ { order_embedding_preserving :> OrderPreserving
+ ; order_embedding_back :> OrderPreservingBack }.
+
+ Class StrictlyOrderPreserving :=
+ { strictly_order_preserving : `(x < y → f x < f y)
+ ; strictly_order_preserving_proper_a :> Proper ((=) ==> (=) ==> iff) oA
+ ; strictly_order_preserving_proper_b :> Proper ((=) ==> (=) ==> iff) oB }.
+
+End order_maps.
@@ -3,7 +3,8 @@ Require Import
Morphisms
abstract_algebra
canonical_names
- interfaces.integers.
+ interfaces.integers
+ interfaces.rationals.
(* Move to a separate module *)
Class Ball A B := ball : B → relation A.
@@ -41,15 +41,15 @@ Infix "⟶" := Arrow (at level 90, right associativity).
Class CatId O `{Arrows O} := cat_id: `(x ⟶ x).
Class CatComp O `{Arrows O} := comp: ∀ {x y z}, (y ⟶ z) → (x ⟶ y) → (x ⟶ z).
Class Order A := precedes: relation A.
-Definition precedes_neq `{Equiv A} `{Order A} : Order A := λ (x y : A), precedes x y ∧ x ≠ y.
+Definition strictly_precedes `{Equiv A} `{Order A} : Order A := λ (x y : A), precedes x y ∧ x ≠ y.
Class RalgebraAction A B := ralgebra_action: A → B → B.
Class RingMultInverse {R} (x: R): Type := ring_mult_inverse: R.
Implicit Arguments ring_mult_inverse [[R] [RingMultInverse]].
Implicit Arguments cat_id [[O] [H] [CatId] [x]].
Implicit Arguments decide [[Decision]].
Instance: Params (@precedes) 2.
-Instance: Params (@precedes_neq) 3.
+Instance: Params (@strictly_precedes) 3.
Instance: Params (@ring_mult) 2.
Instance: Params (@ring_plus) 2.
Instance: Params (@equiv) 2.
@@ -75,8 +75,8 @@ Notation "- x" := (group_inv x).
Notation "// x" := (mult_inv x) (at level 35, right associativity).
Infix "≤" := precedes.
Notation "(≤)" := precedes (only parsing).
-Infix "<" := precedes_neq.
-Notation "(<)" := precedes_neq (only parsing).
+Infix "<" := strictly_precedes.
+Notation "(<)" := strictly_precedes (only parsing).
Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) (at level 70, y at next level).
Notation "x ≤ y < z" := (x ≤ y /\ y < z) (at level 70, y at next level).
Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
@@ -126,11 +126,17 @@ Implicit Arguments antisymmetry [[A] [ea] [AntiSymmetric]].
(* Some things that hold in N, Z, Q, etc, and which we like to refer to by a common name: *)
Class ZeroProduct A `{Equiv A} `{!RingMult A} `{!RingZero A}: Prop :=
zero_product: `(x * y = 0 → x = 0 ∨ y = 0).
-Class ZeroNeOne A `{Equiv A} `{!RingOne A} `{!RingZero A}: Prop :=
- zero_ne_one: 0 ≠ 1.
-Class ZeroNeTwo A `{Equiv A} `{!RingOne A} `{!RingPlus A} `{!RingZero A}: Prop :=
- zero_ne_two: 0 ≠ 2.
- (* todo: this is silly *)
+
+Section compare_zero.
+ Context `{Equiv A} `{!Order A} `{!RingZero A} (x : A).
+ Class NeZero : Prop := ne_zero: x ≠ 0.
+ Class GeZero : Prop := ge_zero: 0 ≤ x.
+End compare_zero.
+
+Section compare_one.
+ Context `{Equiv A} `{!Order A} `{!RingOne A} (x : A).
+ Class GeOne : Prop := ge_one: 1 ≤ x.
+End compare_one.
Class ZeroDivisor {R} `{Equiv R} `{RingZero R} `{RingMult R} (x: R): Prop
:= zero_divisor: x ≠ 0 ∧ ∃ y, y ≠ 0 ∧ x * y = 0.
View
@@ -6,7 +6,8 @@ Require Import
Relation_Definitions Morphisms Ring Field
abstract_algebra interfaces.naturals theory.fields theory.rings.
-Section decfield_order. Context `{Field F} `{∀ x y: F, Decision (x = y)}.
+Section decfield_order.
+ Context `{Field F} `{∀ x y: F, Decision (x = y)}.
Add Ring F: (stdlib_ring_theory F).
(* Trying to register F as a field fails with an obscure error. Looks like a Coq bug.
@@ -53,7 +54,7 @@ Section decfield_order. Context `{Field F} `{∀ x y: F, Decision (x = y)}.
destruct (decide (den = 0)) as [A|A].
exists (0:nat), (1:nat).
rewrite preserves_1, preserves_0.
- split. apply not_symmetry. apply zero_ne_one.
+ split. apply (ne_zero 1).
rewrite <- E, A, preserves_0, dec_mult_inv_0.
ring.
exists num, den. split... intro. apply A.
Oops, something went wrong.

0 comments on commit 5ecc59d

Please sign in to comment.