diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/BoolEqual.v | 8 | ||||
| -rw-r--r-- | lib/Decidableplus.v | 28 | ||||
| -rw-r--r-- | lib/Floats.v | 69 | ||||
| -rw-r--r-- | lib/Integers.v | 177 | ||||
| -rw-r--r-- | lib/Maps.v | 18 |
5 files changed, 230 insertions, 70 deletions
diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index a5b543e1..c9e7bad5 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -17,7 +17,7 @@ (** The [decide equality] tactic can generate a term of type [forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type. -This term is a decidable equality function. +This term is a decidable equality function. Similarly, this module defines a [boolean_equality] tactic that generates a term of type [A -> A -> bool]. This term is a Boolean-valued equality @@ -33,7 +33,7 @@ a decidable equality of type [forall (x y: A), {x=y} + {x<>y}]. The advantage of the present tactics over the standard [decide equality] tactic is that the former produce smaller transparent definitions than -the latter. +the latter. For a type [A] that has N constructors, [decide equality] produces a single term of size O(N^3), which must be kept transparent so that @@ -91,7 +91,7 @@ Ltac bool_eq := end. Lemma proj_sumbool_is_true: - forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), + forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), proj_sumbool (f x x) = true. Proof. intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto. @@ -119,7 +119,7 @@ Lemma proj_sumbool_true: forall (A: Type) (x y: A) (a: {x=y} + {x<>y}), proj_sumbool a = true -> x = y. Proof. - intros. destruct a. auto. discriminate. + intros. destruct a. auto. discriminate. Qed. Ltac bool_eq_sound_case := diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 3bb6eee7..6383794d 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -30,14 +30,14 @@ Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := Decidable_witness := negb (@Decidable_witness P dP) }. Next Obligation. - rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. + rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. Qed. Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := { Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ) }. Next Obligation. - rewrite eqb_true_iff. + rewrite eqb_true_iff. split; intros. split; intros; eapply Decidable_sound; [rewrite <- H | rewrite H]; eapply Decidable_complete; eauto. destruct (@Decidable_witness Q dQ) eqn:D. @@ -65,7 +65,7 @@ Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Next Obligation. split. - intros. rewrite Decidable_complete in H by auto. eapply Decidable_sound; eauto. -- intros. destruct (@Decidable_witness P dP) eqn:WP; auto. +- intros. destruct (@Decidable_witness P dP) eqn:WP; auto. eapply Decidable_complete. apply H. eapply Decidable_sound; eauto. Qed. @@ -75,7 +75,7 @@ Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y Decidable_witness := proj_sumbool (eqdec x y) |}. Next Obligation. - split; intros. InvBooleans. auto. subst y. apply dec_eq_true. + split; intros. InvBooleans. auto. subst y. apply dec_eq_true. Qed. Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { @@ -112,14 +112,14 @@ Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := { Decidable_witness := Z.leb x y }. Next Obligation. - apply Z.leb_le. + apply Z.leb_le. Qed. Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := { Decidable_witness := Z.ltb x y }. Next Obligation. - apply Z.ltb_lt. + apply Z.ltb_lt. Qed. Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { @@ -142,8 +142,8 @@ Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { Next Obligation. split. intros. apply Z.eqb_eq in H. exists (y / x). auto. - intros [k EQ]. apply Z.eqb_eq. - destruct (Z.eq_dec x 0). + intros [k EQ]. apply Z.eqb_eq. + destruct (Z.eq_dec x 0). subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. assert (k = y / x). { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } @@ -152,7 +152,7 @@ Qed. (** Deciding properties over lists *) -Program Instance Decidable_forall_in_list : +Program Instance Decidable_forall_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (forall x:A, In x l -> P x) := { Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l @@ -160,10 +160,10 @@ Program Instance Decidable_forall_in_list : Next Obligation. rewrite List.forallb_forall. split; intros. - eapply Decidable_sound; eauto. -- eapply Decidable_complete; eauto. +- eapply Decidable_complete; eauto. Qed. -Program Instance Decidable_exists_in_list : +Program Instance Decidable_exists_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (exists x:A, In x l /\ P x) := { Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l @@ -188,8 +188,8 @@ Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Pro }. Next Obligation. rewrite List.forallb_forall. split; intros. -- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec. -- eapply Decidable_complete; eauto. +- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec. +- eapply Decidable_complete; eauto. Qed. Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := { @@ -198,7 +198,7 @@ Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Pro Next Obligation. rewrite List.existsb_exists. split. - intros (x & A & B). exists x. eapply Decidable_sound; eauto. -- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto. +- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto. Qed. (** Some examples of finite types. *) diff --git a/lib/Floats.v b/lib/Floats.v index 51b0c415..aa52b197 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -820,6 +820,75 @@ Proof. - omega. Qed. +(** Conversions to/from 32-bit integers can be implemented by going through 64-bit integers. *) + +Remark ZofB_range_widen: + forall (f: float) n min1 max1 min2 max2, + ZofB_range _ _ f min1 max1 = Some n -> + min2 <= min1 -> max1 <= max2 -> + ZofB_range _ _ f min2 max2 = Some n. +Proof. + intros. exploit ZofB_range_inversion; eauto. intros (A & B & C). + unfold ZofB_range; rewrite C. + replace (min2 <=? n) with true. replace (n <=? max2) with true. auto. + symmetry; apply Z.leb_le; omega. + symmetry; apply Z.leb_le; omega. +Qed. + +Theorem to_int_to_long: + forall f n, to_int f = Some n -> to_long f = Some (Int64.repr (Int.signed n)). +Proof. + unfold to_int, to_long; intros. + destruct (ZofB_range 53 1024 f Int.min_signed Int.max_signed) as [z|] eqn:Z; inv H. + exploit ZofB_range_inversion; eauto. intros (A & B & C). + replace (ZofB_range 53 1024 f Int64.min_signed Int64.max_signed) with (Some z). + simpl. rewrite Int.signed_repr; auto. + symmetry; eapply ZofB_range_widen; eauto. compute; congruence. compute; congruence. +Qed. + +Theorem to_intu_to_longu: + forall f n, to_intu f = Some n -> to_longu f = Some (Int64.repr (Int.unsigned n)). +Proof. + unfold to_intu, to_longu; intros. + destruct (ZofB_range 53 1024 f 0 Int.max_unsigned) as [z|] eqn:Z; inv H. + exploit ZofB_range_inversion; eauto. intros (A & B & C). + replace (ZofB_range 53 1024 f 0 Int64.max_unsigned) with (Some z). + simpl. rewrite Int.unsigned_repr; auto. + symmetry; eapply ZofB_range_widen; eauto. omega. compute; congruence. +Qed. + +Theorem to_intu_to_long: + forall f n, to_intu f = Some n -> to_long f = Some (Int64.repr (Int.unsigned n)). +Proof. + unfold to_intu, to_long; intros. + destruct (ZofB_range 53 1024 f 0 Int.max_unsigned) as [z|] eqn:Z; inv H. + exploit ZofB_range_inversion; eauto. intros (A & B & C). + replace (ZofB_range 53 1024 f Int64.min_signed Int64.max_signed) with (Some z). + simpl. rewrite Int.unsigned_repr; auto. + symmetry; eapply ZofB_range_widen; eauto. compute; congruence. compute; congruence. +Qed. + +Theorem of_int_of_long: + forall n, of_int n = of_long (Int64.repr (Int.signed n)). +Proof. + unfold of_int, of_long. intros. f_equal. rewrite Int64.signed_repr. auto. + generalize (Int.signed_range n). compute_this Int64.min_signed. compute_this Int64.max_signed. smart_omega. +Qed. + +Theorem of_intu_of_longu: + forall n, of_intu n = of_longu (Int64.repr (Int.unsigned n)). +Proof. + unfold of_intu, of_longu. intros. f_equal. rewrite Int64.unsigned_repr. auto. + generalize (Int.unsigned_range n). smart_omega. +Qed. + +Theorem of_intu_of_long: + forall n, of_intu n = of_long (Int64.repr (Int.unsigned n)). +Proof. + unfold of_intu, of_long. intros. f_equal. rewrite Int64.signed_repr. auto. + generalize (Int.unsigned_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; smart_omega. +Qed. + End Float. (** * Single-precision FP numbers *) diff --git a/lib/Integers.v b/lib/Integers.v index b1fa982d..c44fa55f 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1224,9 +1224,9 @@ Proof. { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. } rewrite E2. rewrite zle_true. auto. assert (unsigned d <> 0). - { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } + { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } assert (0 < D). - { unfold D. generalize (unsigned_range d); intros. omega. } + { unfold D. generalize (unsigned_range d); intros. omega. } assert (0 <= Q <= max_unsigned). { unfold Q. apply Zdiv_interval_2. rewrite <- E1; apply unsigned_range_2. @@ -1262,7 +1262,7 @@ Proof. set (Q := Z.quot N D); set (R := Z.rem N D). assert (E2: Z.quotrem N D = (Q, R)). { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. } - rewrite E2. + rewrite E2. assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range). assert (min_signed <= Q <= max_signed). { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))]. @@ -1284,7 +1284,7 @@ Proof. rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } rewrite Z.abs_lt in H4. - unfold min_signed, max_signed; omega. + unfold min_signed, max_signed; omega. } unfold proj_sumbool; rewrite ! zle_true by omega; simpl. unfold Q, R; rewrite H2; auto. @@ -2186,6 +2186,16 @@ Proof. + omega. Qed. +Theorem sub_ltu: + forall x y, + ltu x y = true -> + 0 <= unsigned y - unsigned x <= unsigned y. +Proof. + intros. + generalize (ltu_inv x y H). intros . + split. omega. omega. +Qed. + Theorem shru_zero: forall x, shru x zero = x. Proof. bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega. @@ -4036,8 +4046,13 @@ Definition shru' (x: int) (y: Int.int): int := repr (Z.shiftr (unsigned x) (Int.unsigned y)). Definition shr' (x: int) (y: Int.int): int := repr (Z.shiftr (signed x) (Int.unsigned y)). +Definition rol' (x: int) (y: Int.int): int := + rol x (repr (Int.unsigned y)). Definition shrx' (x: int) (y: Int.int): int := divs x (shl' one y). +Definition shr_carry' (x: int) (y: Int.int): int := + if lt x zero && negb (eq (and x (sub (shl' one y) one)) zero) + then one else zero. Lemma bits_shl': forall x y i, @@ -4082,7 +4097,7 @@ Lemma shl'_mul_two_p: shl' x y = mul x (repr (two_p (Int.unsigned y))). Proof. intros. unfold shl', mul. apply eqm_samerepr. - rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. + rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. generalize (Int.unsigned_range y); omega. Qed. @@ -4099,11 +4114,50 @@ Proof. intros. rewrite shl'_one_two_p. apply shl'_mul_two_p. Qed. +Theorem shl'_zero: + forall x, shl' x Int.zero = x. +Proof. + intros. unfold shl'. rewrite Int.unsigned_zero. unfold Z.shiftl. + apply repr_unsigned. +Qed. + +Theorem shru'_zero : + forall x, shru' x Int.zero = x. +Proof. + intros. unfold shru'. rewrite Int.unsigned_zero. unfold Z.shiftr. + apply repr_unsigned. +Qed. + +Theorem shr'_zero : + forall x, shr' x Int.zero = x. +Proof. + intros. unfold shr'. rewrite Int.unsigned_zero. unfold Z.shiftr. + apply repr_signed. +Qed. + Theorem shrx'_zero: forall x, shrx' x Int.zero = x. Proof. - intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto. -Qed. + intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto. +Qed. + +Theorem shrx'_carry: + forall x y, + Int.ltu y (Int.repr 63) = true -> + shrx' x y = add (shr' x y) (shr_carry' x y). +Proof. + intros. apply Int.ltu_inv in H. change (Int.unsigned (Int.repr 63)) with 63 in H. + set (y1 := Int64.repr (Int.unsigned y)). + assert (U: unsigned y1 = Int.unsigned y). + { apply unsigned_repr. assert (63 < max_unsigned) by reflexivity. omega. } + transitivity (shrx x y1). +- unfold shrx', shrx, shl', shl. rewrite U; auto. +- rewrite shrx_carry. ++ f_equal. + unfold shr, shr'. rewrite U; auto. + unfold shr_carry, shr_carry', shl, shl'. rewrite U; auto. ++ unfold ltu. apply zlt_true. rewrite U; tauto. +Qed. Theorem shrx'_shr_2: forall x y, @@ -4119,7 +4173,7 @@ Proof. { unfold z; apply unsigned_repr; omega. } assert (B: unsigned (sub (repr 64) z) = Int.unsigned (Int.sub (Int.repr 64) y)). { unfold z. unfold sub, Int.sub. - change (unsigned (repr 64)) with 64. + change (unsigned (repr 64)) with 64. change (Int.unsigned (Int.repr 64)) with 64. rewrite (unsigned_repr (Int.unsigned y)) by omega. rewrite unsigned_repr, Int.unsigned_repr by omega. @@ -4172,7 +4226,7 @@ Proof. replace (shl' x y) with (shl x (repr (Int.unsigned y))). replace (shru' x z) with (shru x (repr (Int.unsigned z))). apply or_ror; auto. rewrite F, H1. reflexivity. - unfold shru, shru'; rewrite <- B; auto. + unfold shru, shru'; rewrite <- B; auto. unfold shl, shl'; rewrite <- A; auto. Qed. @@ -4190,7 +4244,7 @@ Proof. replace (shl' x y) with (shl x y'). replace (shl' (shl x y') z) with (shl (shl x y') z'). replace (shl' x (Int.add y z)) with (shl x (add y' z')). - apply shl_shl; auto. apply zlt_true. rewrite <- E. + apply shl_shl; auto. apply zlt_true. rewrite <- E. change (unsigned iwordsize) with zwordsize. tauto. unfold shl, shl'. rewrite E; auto. unfold shl at 1, shl'. rewrite <- B; auto. @@ -4211,7 +4265,7 @@ Proof. replace (shru' x y) with (shru x y'). replace (shru' (shru x y') z) with (shru (shru x y') z'). replace (shru' x (Int.add y z)) with (shru x (add y' z')). - apply shru_shru; auto. apply zlt_true. rewrite <- E. + apply shru_shru; auto. apply zlt_true. rewrite <- E. change (unsigned iwordsize) with zwordsize. tauto. unfold shru, shru'. rewrite E; auto. unfold shru at 1, shru'. rewrite <- B; auto. @@ -4232,7 +4286,7 @@ Proof. replace (shr' x y) with (shr x y'). replace (shr' (shr x y') z) with (shr (shr x y') z'). replace (shr' x (Int.add y z)) with (shr x (add y' z')). - apply shr_shr; auto. apply zlt_true. rewrite <- E. + apply shr_shr; auto. apply zlt_true. rewrite <- E. change (unsigned iwordsize) with zwordsize. tauto. unfold shr, shr'. rewrite E; auto. unfold shr at 1, shr'. rewrite <- B; auto. @@ -4256,8 +4310,8 @@ Proof. intros. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. exploit Z_one_bits_range; eauto. intros R. - unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. - change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. + unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. + change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. Qed. @@ -4276,13 +4330,13 @@ Proof. { induction l; simpl; intros. - auto. - rewrite IHl by eauto. apply eqm_samerepr; apply eqm_add. - + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr. + + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr. exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. - + apply eqm_sym; apply eqm_unsigned_repr. + + apply eqm_sym; apply eqm_unsigned_repr. } - intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. + intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. rewrite <- Z_one_bits_powerserie. auto. apply unsigned_range. - apply Z_one_bits_range. + apply Z_one_bits_range. Qed. Lemma is_power2'_rng: @@ -4290,7 +4344,7 @@ Lemma is_power2'_rng: is_power2' n = Some logn -> 0 <= Int.unsigned logn < zwordsize. Proof. - unfold is_power2'; intros n logn P2. + unfold is_power2'; intros n logn P2. destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv P2. assert (0 <= i < zwordsize). { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. } @@ -4303,7 +4357,7 @@ Theorem is_power2'_range: forall n logn, is_power2' n = Some logn -> Int.ltu logn iwordsize' = true. Proof. - intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize. + intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. generalize (is_power2'_rng _ _ H). tauto. Qed. @@ -4321,13 +4375,13 @@ Proof. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. Qed. - + Theorem mul_pow2': forall x n logn, is_power2' n = Some logn -> mul x n = shl' x logn. Proof. - intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p. + intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p. rewrite <- (repr_unsigned n). f_equal. apply is_power2'_correct; auto. Qed. @@ -4855,6 +4909,43 @@ Proof. rewrite zlt_true by omega; auto. Qed. +(** Utility proofs for mixed 32bit and 64bit arithmetic *) + +Remark int_unsigned_range: + forall x, 0 <= Int.unsigned x <= max_unsigned. +Proof. + intros. + unfold max_unsigned. unfold modulus. + generalize (Int.unsigned_range x). + unfold Int.modulus in *. + change (wordsize) with 64%nat in *. + change (Int.wordsize) with 32%nat in *. + unfold two_power_nat. simpl. + omega. +Qed. + +Remark int_unsigned_repr: + forall x, unsigned (repr (Int.unsigned x)) = Int.unsigned x. +Proof. + intros. rewrite unsigned_repr. auto. + apply int_unsigned_range. +Qed. + +Lemma int_sub_ltu: + forall x y, + Int.ltu x y= true -> + Int.unsigned (Int.sub y x) = unsigned (sub (repr (Int.unsigned y)) (repr (Int.unsigned x))). +Proof. + intros. generalize (Int.sub_ltu x y H). intros. unfold Int.sub. unfold sub. + rewrite Int.unsigned_repr. rewrite unsigned_repr. + rewrite unsigned_repr by apply int_unsigned_range. rewrite int_unsigned_repr. reflexivity. + rewrite unsigned_repr by apply int_unsigned_range. + rewrite int_unsigned_repr. generalize (int_unsigned_range y). + omega. + generalize (Int.sub_ltu x y H). intros. + generalize (Int.unsigned_range_2 y). intros. omega. +Qed. + End Int64. Strategy 0 [Wordsize_64.wordsize]. @@ -4899,7 +4990,7 @@ Hypothesis _32: Archi.ptr64 = false. Lemma modulus_eq32: modulus = Int.modulus. Proof. - unfold modulus, wordsize. + unfold modulus, wordsize. change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat). rewrite _32. reflexivity. Qed. @@ -4923,8 +5014,8 @@ Qed. Lemma agree32_signed: forall a b, agree32 a b -> Ptrofs.signed a = Int.signed b. Proof. - unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus. - rewrite modulus_eq32. rewrite H. auto. + unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus. + rewrite modulus_eq32. rewrite H. auto. Qed. Lemma agree32_of_int: @@ -4932,7 +5023,7 @@ Lemma agree32_of_int: Proof. unfold of_int; intros. rewrite <- (Int.repr_unsigned b) at 2. apply agree32_repr. Qed. - + Lemma agree32_of_ints: forall b, agree32 (of_ints b) b. Proof. @@ -4942,7 +5033,7 @@ Qed. Lemma agree32_of_int_eq: forall a b, agree32 a b -> of_int b = a. Proof. - unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned. + unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned. Qed. Lemma agree32_of_ints_eq: @@ -4954,7 +5045,7 @@ Qed. Lemma agree32_to_int: forall a, agree32 a (to_int a). Proof. - unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). + unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). rewrite repr_unsigned; auto. Qed. @@ -4974,21 +5065,21 @@ Lemma agree32_add: forall a1 b1 a2 b2, agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.add a1 a2) (Int.add b1 b2). Proof. - unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr. + unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr. Qed. Lemma agree32_sub: forall a1 b1 a2 b2, agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2). Proof. - unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr. + unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr. Qed. Lemma agree32_mul: forall a1 b1 a2 b2, agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.mul a1 a2) (Int.mul b1 b2). Proof. - unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr. + unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr. Qed. Lemma agree32_divs: @@ -5004,7 +5095,7 @@ Lemma of_int_to_int: Proof. intros; unfold of_int, to_int. apply eqm_repr_eq. rewrite <- eqm32. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. -Qed. +Qed. End AGREE32. @@ -5014,7 +5105,7 @@ Hypothesis _64: Archi.ptr64 = true. Lemma modulus_eq64: modulus = Int64.modulus. Proof. - unfold modulus, wordsize. + unfold modulus, wordsize. change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat). rewrite _64. reflexivity. Qed. @@ -5038,8 +5129,8 @@ Qed. Lemma agree64_signed: forall a b, agree64 a b -> Ptrofs.signed a = Int64.signed b. Proof. - unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus. - rewrite modulus_eq64. rewrite H. auto. + unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus. + rewrite modulus_eq64. rewrite H. auto. Qed. Lemma agree64_of_int: @@ -5051,13 +5142,13 @@ Qed. Lemma agree64_of_int_eq: forall a b, agree64 a b -> of_int64 b = a. Proof. - unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned. + unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned. Qed. Lemma agree64_to_int: forall a, agree64 a (to_int64 a). Proof. - unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)). + unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)). rewrite repr_unsigned; auto. Qed. @@ -5077,21 +5168,21 @@ Lemma agree64_add: forall a1 b1 a2 b2, agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.add a1 a2) (Int64.add b1 b2). Proof. - unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr. + unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr. Qed. Lemma agree64_sub: forall a1 b1 a2 b2, agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.sub a1 a2) (Int64.sub b1 b2). Proof. - unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr. + unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr. Qed. Lemma agree64_mul: forall a1 b1 a2 b2, agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.mul a1 a2) (Int64.mul b1 b2). Proof. - unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr. + unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr. Qed. Lemma agree64_divs: @@ -5107,16 +5198,16 @@ Lemma of_int64_to_int64: Proof. intros; unfold of_int64, to_int64. apply eqm_repr_eq. rewrite <- eqm64. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. -Qed. +Qed. End AGREE64. -Hint Resolve +Hint Resolve agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs agree64_repr agree64_of_int agree64_of_int_eq agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs : ptrofs. - + End Ptrofs. Strategy 0 [Wordsize_Ptrofs.wordsize]. @@ -819,8 +819,8 @@ Module PTree <: TREE. (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (elements m) (elements n). Proof. - intros. apply elements_canonical_order'. - intros. destruct (get i m) as [x|] eqn:GM. + intros. apply elements_canonical_order'. + intros. destruct (get i m) as [x|] eqn:GM. exploit H; eauto. intros (y & P & Q). rewrite P; constructor; auto. destruct (get i n) as [y|] eqn:GN. exploit H0; eauto. intros (x & P & Q). congruence. @@ -1265,7 +1265,7 @@ Module ITree(X: INDEXED_TYPE). | _, _ => False end. Proof. - unfold beq, get. intros. rewrite PTree.beq_correct in H. apply H. + unfold beq, get. intros. rewrite PTree.beq_correct in H. apply H. Qed. Definition combine: forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C := PTree.combine. @@ -1636,8 +1636,8 @@ Proof. { induction l as [ | [k1 v1] l]; simpl; intros. - tauto. - apply IHl in H. unfold f in H. simpl in H. rewrite T.gsspec in H. - destruct H; auto. - destruct (T.elt_eq k k1). inv H. auto. auto. + destruct H; auto. + destruct (T.elt_eq k k1). inv H. auto. auto. } intros. apply REC in H. rewrite T.gempty in H. intuition congruence. Qed. @@ -1650,7 +1650,7 @@ Proof. exists v, T.get k (fold_left f l m) = Some v). { induction l as [ | [k1 v1] l]; simpl; intros. - tauto. - - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1). + - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1). right; econstructor; eauto. intuition congruence. } @@ -1669,7 +1669,7 @@ Lemma of_list_unique: forall k v l1 l2, ~In k (map fst l2) -> T.get k (of_list (l1 ++ (k, v) :: l2)) = Some v. Proof. - intros. unfold of_list. rewrite fold_left_app. simpl. + intros. unfold of_list. rewrite fold_left_app. simpl. rewrite of_list_unchanged by auto. unfold f; apply T.gss. Qed. @@ -1683,8 +1683,8 @@ Proof. { induction l as [ | [k1 v1] l]; simpl; intros. contradiction. inv H. destruct H0. - inv H. rewrite of_list_unchanged by auto. apply T.gss. - apply IHl; auto. + inv H. rewrite of_list_unchanged by auto. apply T.gss. + apply IHl; auto. } intros; apply REC; auto. Qed. |