diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-04 07:43:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-04 07:43:59 +0000 |
| commit | 4ef212cf00231a59581abbf60528a3a4a235e5ef (patch) | |
| tree | 6ec497c5ef6b8812b66dcea2c5323115ab681268 | |
| parent | 42f62fbf8bc3d14d66ecf0a5db6fa2db16b82db5 (diff) | |
| download | vericert-kvx-4ef212cf00231a59581abbf60528a3a4a235e5ef.tar.gz vericert-kvx-4ef212cf00231a59581abbf60528a3a4a235e5ef.zip | |
Continue to prove signed_neg
| -rw-r--r-- | src/common/IntegerExtra.v | 45 |
1 files changed, 44 insertions, 1 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index f1cc0e4..ac69483 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -400,9 +400,52 @@ Module IntExtra. unfold signed. simpl. rewrite Z_mod_modulus_eq. + replace modulus with 4294967296; auto. + replace half_modulus with 2147483648; auto. simpl. repeat match goal with | |- context[if ?x then _ else _] => destruct x end. - Admitted. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e. auto. + + pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296). + assert (4294967296 <> 0). lia. + apply H in H0. + rewrite H0 in l. + pose proof (Z.mod_small (unsigned x) 4294967296). + assert (0 <= unsigned x < 4294967296). + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + apply H1 in H2. rewrite H2 in l. lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz. + rewrite Z.opp_sub_distr. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e in *. rewrite Z.opp_0 in *. rewrite Zmod_0_l in g. lia. + + rewrite Z.mod_opp_l_nz. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + lia. + rewrite Z.mod_small. + assumption. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in *; auto. lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz in g. + rewrite Z.mod_small in g. + assert (- unsigned x >= - 2147483648) by lia. + Lemma neg_divs_distr_l : forall x y, |