diff options
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs')
| -rw-r--r-- | src/LegacyArithmetic/Double/Proofs/Decode.v | 20 | ||||
| -rw-r--r-- | src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v | 22 |
2 files changed, 24 insertions, 18 deletions
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]. |