diff options
Diffstat (limited to 'src/BoundedArithmetic')
13 files changed, 41 insertions, 41 deletions
diff --git a/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v b/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v index 048b83887..9d5b409f8 100644 --- a/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v +++ b/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v @@ -16,7 +16,7 @@ Section bitwise_or. Global Instance is_bitwise_or_double : is_bitwise_or or_double. - Proof. + Proof using Type*. constructor; intros x y. destruct n as [|p|]. { rewrite !(tuple_decoder_n_O (W:=W) 2); easy. } diff --git a/src/BoundedArithmetic/Double/Proofs/Decode.v b/src/BoundedArithmetic/Double/Proofs/Decode.v index 1c5a6495a..e3d57bdfc 100644 --- a/src/BoundedArithmetic/Double/Proofs/Decode.v +++ b/src/BoundedArithmetic/Double/Proofs/Decode.v @@ -26,7 +26,7 @@ Section decode. Lemma decode_bounded {isdecode : is_decode decode} w : 0 <= n -> bounded limb_widths (List.map decode (rev (to_list k w))). - Proof. + Proof using Type. intro. eapply bounded_uniform; try solve [ eauto using repeat_spec ]. { distr_length. } @@ -38,7 +38,7 @@ Section decode. (** TODO: Clean up this proof *) Global Instance tuple_is_decode {isdecode : is_decode decode} : is_decode (tuple_decoder (k := k)). - Proof. + Proof using Type. unfold tuple_decoder; hnf; simpl. intro w. destruct (zerop k); [ subst | ]. @@ -59,7 +59,7 @@ Section decode. Local Arguments repeat : simpl never. Local Arguments Z.mul !_ !_. Lemma tuple_decoder_S {k} w : 0 <= n -> (tuple_decoder (k := S (S k)) w = tuple_decoder (k := S k) (fst w) + (decode (snd w) << (S k * n)))%Z. - Proof. + Proof using Type. intro Hn. destruct w as [? w]; simpl. replace (decode w) with (decode w * 1 + 0)%Z by omega. @@ -70,16 +70,16 @@ Section decode. reflexivity. Qed. Global Instance tuple_decoder_O w : tuple_decoder (k := 1) w =~> decode w. - Proof. + Proof using Type. unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', accumulate, base_from_limb_widths, repeat. simpl; hnf. omega. Qed. Global Instance tuple_decoder_m1 w : tuple_decoder (k := 0) w =~> 0. - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Lemma tuple_decoder_n_neg k w {H : is_decode decode} : n <= 0 -> tuple_decoder (k := k) w =~> 0. - Proof. + Proof using Type. pose proof (tuple_is_decode w) as H'; hnf in H'. intro; assert (k * n <= 0) by nia. assert (2^(k * n) <= 2^0) by (apply Z.pow_le_mono_r; omega). @@ -91,7 +91,7 @@ Section decode. (P_ext : forall n (a b : decoder n W), (forall x, a x = b x) -> P _ a -> P _ b) : (P _ (tuple_decoder (k := 1)) -> P _ decode) * (P _ decode -> P _ (tuple_decoder (k := 1))). - Proof. + Proof using Type. unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', accumulate, base_from_limb_widths, repeat. simpl; hnf. rewrite Z.mul_1_l. @@ -99,12 +99,12 @@ Section decode. Qed. Global Instance tuple_decoder_2' w : (0 <= n)%bounded_rewrite -> tuple_decoder (k := 2) w <~= (decode (fst w) + decode (snd w) << (1%nat * n))%Z. - Proof. + Proof using Type. intros; rewrite !tuple_decoder_S, !tuple_decoder_O by assumption. reflexivity. Qed. Global Instance tuple_decoder_2 w : (0 <= n)%bounded_rewrite -> tuple_decoder (k := 2) w <~= (decode (fst w) + decode (snd w) << n)%Z. - Proof. + Proof using Type. intros; rewrite !tuple_decoder_S, !tuple_decoder_O by assumption. autorewrite with zsimplify_const; reflexivity. Qed. diff --git a/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v b/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v index 155845760..9c00b728f 100644 --- a/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v +++ b/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v @@ -18,7 +18,7 @@ Section load_immediate. Global Instance is_load_immediate_double : is_load_immediate (ldi_double n). - Proof. + Proof using Type*. intros x H; hnf in H. pose proof (decode_exponent_nonnegative decode (ldi x)). assert (0 <= x mod 2^n < 2^n) by auto with zarith. diff --git a/src/BoundedArithmetic/Double/Proofs/Multiply.v b/src/BoundedArithmetic/Double/Proofs/Multiply.v index bb09f8b2b..6d2f72c25 100644 --- a/src/BoundedArithmetic/Double/Proofs/Multiply.v +++ b/src/BoundedArithmetic/Double/Proofs/Multiply.v @@ -73,7 +73,7 @@ Section tuple2. Lemma decode_mul_double_mod x y : (tuple_decoder (mul_double half_n x y) = (decode x * decode y) mod (2^(2 * half_n) * 2^(2*half_n)))%Z. - Proof. + Proof using Type*. assert (0 <= 2 * half_n) by eauto using decode_exponent_nonnegative. assert (0 <= half_n) by omega. unfold mul_double, Let_In. @@ -94,13 +94,13 @@ Section tuple2. Lemma decode_mul_double_function x y : tuple_decoder (mul_double half_n x y) = (decode x * decode y)%Z. - Proof. + Proof using Type*. rewrite decode_mul_double_mod; generalize_decode_var. simpl in *; Z.rewrite_mod_small; reflexivity. Qed. Global Instance mul_double_is_multiply_double : is_mul_double mul_double_multiply. - Proof. + Proof using Type*. apply decode_mul_double_iff; apply decode_mul_double_function. Qed. End full_from_half. @@ -123,10 +123,10 @@ Section tuple2. try reflexivity. Global Instance mul_double_is_multiply_low_low : is_mul_low_low n mul_double_multiply_low_low. - Proof. t. Qed. + Proof using Type*. t. Qed. Global Instance mul_double_is_multiply_high_low : is_mul_high_low n mul_double_multiply_high_low. - Proof. t. Qed. + Proof using Type*. t. Qed. Global Instance mul_double_is_multiply_high_high : is_mul_high_high n mul_double_multiply_high_high. - Proof. t. Qed. + Proof using Type*. t. Qed. End half_from_full. End tuple2. diff --git a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v index 672a62685..5d9443a91 100644 --- a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -71,7 +71,7 @@ Section carry_sub_is_good. Lemma carry_sub_is_good_carry : ((z1 - if z0 <? 0 then 1 else 0) <? 0) = ((z0 + z1 << k) <? 0). - Proof. + Proof using Hk Hz0. clear n Hn Hz1. assert (0 < 2 ^ k) by auto with zarith. autorewrite with Zshift_to_pow. @@ -88,7 +88,7 @@ Section carry_sub_is_good. Lemma carry_sub_is_good_value : (z0 mod 2 ^ k + ((z1 - if z0 <? 0 then 1 else 0) mod 2 ^ n) << k)%Z = (z0 + z1 << k) mod (2 ^ k * 2 ^ n). - Proof. + Proof using Type*. assert (0 < 2 ^ n) by auto with zarith. assert (0 < 2 ^ k) by auto with zarith. assert (0 < 2^n * 2^k) by nia. @@ -119,14 +119,14 @@ Section ripple_carry_adc. let '(carry, zs) := eta (ripple_carry_adc (k := S k) adc xs ys carry) in let '(carry, z) := eta (adc x y carry) in (carry, (zs, z)). - Proof. apply ripple_carry_tuple_SS. Qed. + Proof using Type. apply ripple_carry_tuple_SS. Qed. Local Opaque Z.of_nat. Global Instance ripple_carry_is_add_with_carry {k} {isdecode : is_decode decode} {is_adc : is_add_with_carry adc} : is_add_with_carry (ripple_carry_adc (k := k) adc). - Proof. + Proof using Type. destruct k as [|k]. { constructor; simpl; intros; autorewrite with zsimplify; reflexivity. } { induction k as [|k IHk]. @@ -163,14 +163,14 @@ Section ripple_carry_subc. let '(carry, zs) := eta (ripple_carry_subc (k := S k) subc xs ys carry) in let '(carry, z) := eta (subc x y carry) in (carry, (zs, z)). - Proof. apply ripple_carry_tuple_SS. Qed. + Proof using Type. apply ripple_carry_tuple_SS. Qed. Local Opaque Z.of_nat. Global Instance ripple_carry_is_sub_with_carry {k} {isdecode : is_decode decode} {is_subc : is_sub_with_carry subc} : is_sub_with_carry (ripple_carry_subc (k := k) subc). - Proof. + Proof using Type. destruct k as [|k]. { constructor; repeat (intros [] || intro); autorewrite with simpl_tuple_decoder zsimplify; reflexivity. } { induction k as [|k IHk]. diff --git a/src/BoundedArithmetic/Double/Proofs/SelectConditional.v b/src/BoundedArithmetic/Double/Proofs/SelectConditional.v index 41ae9dc3b..8dd12e0bc 100644 --- a/src/BoundedArithmetic/Double/Proofs/SelectConditional.v +++ b/src/BoundedArithmetic/Double/Proofs/SelectConditional.v @@ -12,7 +12,7 @@ Section select_conditional. Global Instance is_select_conditional_double : is_select_conditional selc_double. - Proof. + Proof using Type*. intros b x y. destruct n. { rewrite !(tuple_decoder_n_O (W:=W) 2); now destruct b. } diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v index 193dc59bf..759c05e6e 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v @@ -26,7 +26,7 @@ Section shl. {isor : is_bitwise_or or}. Global Instance is_shift_left_immediate_double : is_shift_left_immediate (shl_double n). - Proof. + Proof using Type*. intros r count H; hnf in H. assert (0 < 2^count) by auto with zarith. assert (0 < 2^(n+count)) by auto with zarith. diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v index dde19595e..f2509927f 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v @@ -26,7 +26,7 @@ Section shr. {isor : is_bitwise_or or}. Global Instance is_shift_right_immediate_double : is_shift_right_immediate (shr_double n). - Proof. + Proof using Type*. intros r count H; hnf in H. assert (0 < 2^count) by auto with zarith. assert (0 < 2^(n+count)) by auto with zarith. diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v index dce9940d5..7e9f5ddcd 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v @@ -24,7 +24,7 @@ Section shrd. Local Ltac zutil_arith ::= solve [ auto with nocore omega ]. Global Instance is_shift_right_doubleword_immediate_double : is_shift_right_doubleword_immediate (shrd_double n). - Proof. + Proof using isdecode isshrd. intros high low count Hcount; hnf in Hcount. unfold shrd_double, shift_right_doubleword_immediate_double; simpl. generalize (decode_range low). diff --git a/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v b/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v index f2061bafe..84f24eef5 100644 --- a/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v +++ b/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v @@ -61,7 +61,7 @@ Section tuple2. r count (H : 0 < count < n) : (decode (shl r count) + decode (shr r (n - count)) << n = decode r << count mod (2^n*2^n))%Z. - Proof. + Proof using isdecode isshl isshr. assert (0 <= count < n) by lia. assert (0 <= n - count < n) by lia. assert (0 < 2^(n-count)) by auto with zarith. @@ -80,7 +80,7 @@ Section tuple2. Global Instance is_spread_left_from_shift : is_spread_left_immediate (sprl_from_shift n). - Proof. + Proof using Type*. apply is_spread_left_immediate_alt. intros r count; intros. pose proof (decode_range r). @@ -124,7 +124,7 @@ Section tuple2. r : (decode (shl r half_n) + decode (shr r half_n) * (2^half_n * 2^half_n) = (decode r * 2^half_n) mod (2^half_n*2^half_n*2^half_n*2^half_n))%Z. - Proof. + Proof using Type*. destruct (0 <? half_n) eqn:Hn; Z.ltb_to_lt. { pose proof (spread_left_from_shift_correct (2*half_n) r half_n) as H. specialize_by lia. diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v index 2c7a0ad1b..a00e0c891 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v @@ -64,7 +64,7 @@ Section multiply. : (is_mul_low_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_low_low_repeated_double (exp:=exp)) * is_mul_high_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_low_repeated_double (exp:=exp)) * is_mul_high_high (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_high_repeated_double (exp:=exp)))%type. - Proof. + Proof using Type*. destruct exp as [|exp']; [ clear is_multi_multiply_repeated_double | specialize (is_multi_multiply_repeated_double exp') ]. { destruct decode; generalize ismulhwll, ismulhwhl, ismulhwhh. simpl. diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v index 401e3a015..acda67158 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v @@ -32,7 +32,7 @@ Section shift_left_right. Fixpoint is_shift_left_right_immediate_repeated_double {exp : nat} : (is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) * is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp)))%type. - Proof. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. + Proof using Type*. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. Global Instance is_shift_left_immediate_repeated_double {exp : nat} : is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) := fst (@is_shift_left_right_immediate_repeated_double exp). diff --git a/src/BoundedArithmetic/InterfaceProofs.v b/src/BoundedArithmetic/InterfaceProofs.v index 25cd09e85..85120f50c 100644 --- a/src/BoundedArithmetic/InterfaceProofs.v +++ b/src/BoundedArithmetic/InterfaceProofs.v @@ -48,7 +48,7 @@ Section InstructionGallery. {isdecode : is_decode Wdecoder} : is_spread_left_immediate sprl <-> (forall r count, 0 <= count < n -> decode (fst (sprl r count)) + decode (snd (sprl r count)) << n = (decode r << count) mod (2^n*2^n))%Z. - Proof. + Proof using Type. split; intro H; [ | apply Build_is_spread_left_immediate' ]; intros r count Hc; [ | specialize (H r count Hc); revert H ]; @@ -70,7 +70,7 @@ Section InstructionGallery. {isdecode : is_decode Wdecoder} : is_mul_double muldw <-> (forall x y, decode (fst (muldw x y)) + decode (snd (muldw x y)) << n = (decode x * decode y) mod (2^n*2^n)). - Proof. + Proof using Type. split; intro H; [ | apply Build_is_mul_double' ]; intros x y; [ | specialize (H x y); revert H ]; @@ -136,19 +136,19 @@ Section adc_subc. {issubc : is_sub_with_carry subc}. Global Instance bit_fst_add_with_carry_false : forall x y, bit (fst (adc x y false)) <~=~> (decode x + decode y) >> n. - Proof. + Proof using isadc. intros; erewrite bit_fst_add_with_carry by assumption. autorewrite with zsimplify_const; reflexivity. Qed. Global Instance bit_fst_add_with_carry_true : forall x y, bit (fst (adc x y true)) <~=~> (decode x + decode y + 1) >> n. - Proof. + Proof using isadc. intros; erewrite bit_fst_add_with_carry by assumption. autorewrite with zsimplify_const; reflexivity. Qed. Global Instance fst_add_with_carry_leb : forall x y c, fst (adc x y c) <~= (2^n <=? (decode x + decode y + bit c)). - Proof. + Proof using isadc isdecode. intros x y c; hnf. assert (0 <= n)%Z by eauto using decode_exponent_nonnegative. pose proof (decode_range x); pose proof (decode_range y). @@ -165,25 +165,25 @@ Section adc_subc. Qed. Global Instance fst_add_with_carry_false_leb : forall x y, fst (adc x y false) <~= (2^n <=? (decode x + decode y)). - Proof. + Proof using isadc isdecode. intros; erewrite fst_add_with_carry_leb by assumption. autorewrite with zsimplify_const; reflexivity. Qed. Global Instance fst_add_with_carry_true_leb : forall x y, fst (adc x y true) <~=~> (2^n <=? (decode x + decode y + 1)). - Proof. + Proof using isadc isdecode. intros; erewrite fst_add_with_carry_leb by assumption. autorewrite with zsimplify_const; reflexivity. Qed. Global Instance fst_sub_with_carry_false : forall x y, fst (subc x y false) <~=~> ((decode x - decode y) <? 0). - Proof. + Proof using issubc. intros; erewrite fst_sub_with_carry by assumption. autorewrite with zsimplify_const; reflexivity. Qed. Global Instance fst_sub_with_carry_true : forall x y, fst (subc x y true) <~=~> ((decode x - decode y - 1) <? 0). - Proof. + Proof using issubc. intros; erewrite fst_sub_with_carry by assumption. autorewrite with zsimplify_const; reflexivity. Qed. |