diff options
Diffstat (limited to 'src/LegacyArithmetic')
-rw-r--r-- | src/LegacyArithmetic/BaseSystemProofs.v | 3 | ||||
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/Decode.v | 20 | ||||
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v | 22 | ||||
-rw-r--r-- | src/LegacyArithmetic/InterfaceProofs.v | 5 | ||||
-rw-r--r-- | src/LegacyArithmetic/Pow2BaseProofs.v | 37 |
5 files changed, 49 insertions, 38 deletions
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v index b87df814d..f0f0a80d2 100644 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ b/src/LegacyArithmetic/BaseSystemProofs.v @@ -122,7 +122,8 @@ Section BaseSystemProofs. end. rewrite (combine_truncate_r vs bs); apply (f_equal2 Z.add); trivial; []. unfold combine; break_match. - { apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } + { let Heql := match goal with H : _ = nil |- _ => H end in + apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } { cbv -[Z.add Z.mul]; ring_simplify; f_equal. assert (HH: nth_error (z0 :: l) 0 = Some z) by ( diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v index b5b6d6623..1cd5bf06d 100644 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ b/src/LegacyArithmetic/Double/Proofs/Decode.v @@ -145,9 +145,10 @@ Hint Rewrite Hint Rewrite @tuple_decoder_S @tuple_decoder_O @tuple_decoder_m1 using solve [ auto with zarith ] : simpl_tuple_decoder. -Global Instance tuple_decoder_mod {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))) - : tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n). +Global Instance tuple_decoder_mod : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), + tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n). Proof. + intros n W decode k isdecode w. pose proof (snd w). assert (0 <= n) by eauto using decode_exponent_nonnegative. assert (0 <= (S k) * n) by nia. @@ -156,9 +157,10 @@ Proof. reflexivity. Qed. -Global Instance tuple_decoder_div {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))) - : decode (snd w) <~= tuple_decoder w / 2^(S k * n). +Global Instance tuple_decoder_div : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), + decode (snd w) <~= tuple_decoder w / 2^(S k * n). Proof. + intros n W decode k isdecode w. pose proof (snd w). assert (0 <= n) by eauto using decode_exponent_nonnegative. assert (0 <= (S k) * n) by nia. @@ -169,16 +171,18 @@ Proof. reflexivity. Qed. -Global Instance tuple2_decoder_mod {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2) - : decode (fst w) <~= tuple_decoder w mod 2^n. +Global Instance tuple2_decoder_mod : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), + decode (fst w) <~= tuple_decoder w mod 2^n. Proof. + intros n W decode isdecode w. generalize (@tuple_decoder_mod n W decode 0 isdecode w). autorewrite with simpl_tuple_decoder; trivial. Qed. -Global Instance tuple2_decoder_div {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2) - : decode (snd w) <~= tuple_decoder w / 2^n. +Global Instance tuple2_decoder_div : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), + decode (snd w) <~= tuple_decoder w / 2^n. Proof. + intros n W decode isdecode w. generalize (@tuple_decoder_div n W decode 0 isdecode w). autorewrite with simpl_tuple_decoder; trivial. Qed. diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v index e703c2e57..d0514db57 100644 --- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -122,12 +122,13 @@ Section ripple_carry_adc. 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). + Global Instance ripple_carry_is_add_with_carry + : forall {k} + {isdecode : is_decode decode} + {is_adc : is_add_with_carry adc}, + is_add_with_carry (ripple_carry_adc (k := k) adc). Proof using Type. - destruct k as [|k]. + destruct k as [|k]; intros isdecode is_adc. { constructor; simpl; intros; autorewrite with zsimplify; reflexivity. } { induction k as [|k IHk]. { cbv [ripple_carry_adc ripple_carry_tuple to_list]. @@ -166,12 +167,13 @@ Section ripple_carry_subc. 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). + Global Instance ripple_carry_is_sub_with_carry + : forall {k} + {isdecode : is_decode decode} + {is_subc : is_sub_with_carry subc}, + is_sub_with_carry (ripple_carry_subc (k := k) subc). Proof using Type. - destruct k as [|k]. + destruct k as [|k]; intros isdecode is_subc. { constructor; repeat (intros [] || intro); autorewrite with simpl_tuple_decoder zsimplify; reflexivity. } { induction k as [|k IHk]. { cbv [ripple_carry_subc ripple_carry_tuple to_list]. diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v index 9ef97fa55..33917e00d 100644 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ b/src/LegacyArithmetic/InterfaceProofs.v @@ -99,8 +99,9 @@ Global Instance decode_proj n W (dec : W -> Z) : @decode n W {| decode := dec |} =~> dec. Proof. reflexivity. Qed. -Global Instance decode_if_bool n W (decode : decoder n W) (b : bool) x y - : decode (if b then x else y) +Global Instance decode_if_bool n W (decode : decoder n W) + : forall (b : bool) x y, + decode (if b then x else y) =~> if b then decode x else decode y. Proof. destruct b; reflexivity. Qed. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index 35540f39a..b6df85f5c 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -73,7 +73,7 @@ Section Pow2BaseProofs. nth_error base (S i) = Some (two_p w * b). Proof using Type. clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) - induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; + induction limb_widths; intros i b w ? nth_err_w nth_err_b; unfold base_from_limb_widths in *; fold base_from_limb_widths in *; [rewrite (@nil_length0 Z) in *; omega | ]. simpl in *. @@ -97,7 +97,7 @@ Section Pow2BaseProofs. Lemma nth_error_base : forall i, (i < length limb_widths)%nat -> nth_error base i = Some (two_p (sum_firstn limb_widths i)). Proof using Type*. - induction i; intros. + induction i as [|i IHi]; intros H. + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. + assert (i < length limb_widths)%nat as lt_i_length by omega. @@ -165,6 +165,7 @@ Section Pow2BaseProofs. Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i. Proof using Type. clear. + cbv [bounded]; intros lw us i H H0. repeat match goal with | |- _ => progress (cbv [bounded]; intros) | |- _ => break_if @@ -174,6 +175,7 @@ Section Pow2BaseProofs. end. specialize (H0 i). symmetry. + let n := match goal with n : Z |- _ => n end in rewrite <- (Z.mod_pow2_bits_high (nth_default 0 us i) (nth_default 0 lw i) n); [ rewrite Z.mod_small by omega; reflexivity | ]. split; try omega. @@ -183,15 +185,15 @@ Section Pow2BaseProofs. Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). Proof using Type. clear. - split; cbv [bounded]; intros. - + edestruct (In_nth_error_value us u); try assumption. + intros us; split; cbv [bounded]; [ intros H u H0 | intros H i ]. + + edestruct (In_nth_error_value us u) as [x]; try assumption. specialize (H x). replace u with (nth_default 0 us x) by (auto using nth_error_value_eq_nth_default). rewrite nth_default_nil, Z.pow_0_r in H. omega. + rewrite nth_default_nil, Z.pow_0_r. apply nth_default_preserves_properties; try omega. - intros. + intros x H0. apply H in H0. omega. Qed. @@ -206,7 +208,8 @@ Section Pow2BaseProofs. Lemma digit_select : forall us i, bounded limb_widths us -> nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i). Proof using Type*. - intro; revert limb_widths limb_widths_nonneg; induction us; intros. + intro us; revert limb_widths limb_widths_nonneg; induction us as [|a us IHus]; + intros limb_widths limb_widths_nonneg i H. + rewrite nth_default_nil, BaseSystemProofs.decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega). reflexivity. @@ -226,7 +229,7 @@ Section Pow2BaseProofs. rewrite bounded_iff in *. specialize (H 0%nat); rewrite !nth_default_cons in H. rewrite <-Z.lor_shiftl by (auto using in_eq; omega). - apply Z.bits_inj'; intros. + apply Z.bits_inj'; intros n H0. rewrite Z.testbit_pow2_mod by auto using in_eq. break_if. { autorewrite with Ztestbit; break_match; @@ -270,7 +273,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i). Proof using Type*. - intros; induction i; + intros us i H H0 H1; induction i; repeat match goal with | |- _ => rewrite sum_firstn_0, BaseSystemProofs.decode_nil, Z.pow2_mod_0_r; reflexivity | |- _ => progress distr_length @@ -325,7 +328,7 @@ Section Pow2BaseProofs. sum_firstn limb_widths (length us) <= n -> Z.testbit (BaseSystem.decode base us) n = false. Proof using Type*. - intros. + intros us n H H0 H1. erewrite <-(firstn_all _ us) by reflexivity. auto using testbit_decode_firstn_high. Qed. @@ -336,7 +339,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> 0 <= BaseSystem.decode base us. Proof using Type*. - intros. + intros us H H0. unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *. pose 0 as zero. assert (0 <= zero) by reflexivity. @@ -365,7 +368,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> 0 <= BaseSystem.decode base us < upper_bound limb_widths. Proof using Type*. - cbv [upper_bound]; intros. + cbv [upper_bound]; intros us H H0. split. { apply decode_nonneg; auto. } { apply Z.testbit_false_bound; auto; intros. @@ -387,7 +390,7 @@ Section Pow2BaseProofs. Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)). Proof using Type*. - intros; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. + intros us u0 H; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ]. destruct limb_widths; distr_length; reflexivity. Qed. @@ -437,10 +440,10 @@ Section UniformBase. Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). Proof using Type*. - cbv [bounded]; split; intro A; intros. + cbv [bounded]; intros us H; split; intro A; [ intros u H0 | intros i ]. + let G := fresh "G" in match goal with H : In _ us |- _ => - eapply In_nth in H; destruct H as [? G]; destruct G as [? G]; + eapply In_nth in H; destruct H as [x G]; destruct G as [? G]; rewrite <-nth_default_eq in G; rewrite <-G end. specialize (A x). split; try eapply A. @@ -457,7 +460,7 @@ Section UniformBase. Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof using Type*. - intros. + intros w H. replace w with width by (symmetry; auto). assumption. Qed. @@ -502,7 +505,7 @@ Section UniformBase. Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us. Proof using Type. clear. - induction us; intros. + induction us as [|a us IHus]; intros bs. + rewrite !BaseSystemProofs.decode_nil; reflexivity. + distr_length. destruct bs. @@ -517,7 +520,7 @@ Section UniformBase. (n < length xs)%nat -> firstn n xs = firstn n (tl xs). Proof using Type. - intros. + intros A xs n x H H0. erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ]. rewrite ListUtil.tl_repeat. autorewrite with push_firstn. |