diff options
Diffstat (limited to 'src/common')
-rw-r--r-- | src/common/Coquplib.v | 3 | ||||
-rw-r--r-- | src/common/IntegerExtra.v | 50 |
2 files changed, 53 insertions, 0 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index b4ca906..b8a02d2 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -117,6 +117,9 @@ Ltac simplify := unfold_constants; simpl in *; Global Opaque Nat.div. Global Opaque Z.mul. +Infix "==nat" := eq_nat_dec (no associativity, at level 50). +Infix "==Z" := Z.eq_dec (no associativity, at level 50). + (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 2f9aae6..5f06e26 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -51,6 +51,23 @@ Module PtrofsExtra. Ltac ptrofs_mod_tac m := repeat (ptrofs_mod_match m); lia. + Lemma signed_mod_unsigned_mod : + forall x m, + 0 < m -> + Ptrofs.modulus mod m = 0 -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.unsigned x mod m = 0. + Proof. + intros. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + Lemma of_int_mod : forall x m, Int.signed x mod m = 0 -> @@ -121,6 +138,25 @@ Module PtrofsExtra. congruence. Qed. + Lemma divs_unsigned : + forall x y, + 0 <= Ptrofs.signed x -> + 0 < Ptrofs.signed y -> + Ptrofs.unsigned (Ptrofs.divs x y) = Ptrofs.signed x / Ptrofs.signed y. + Proof. + intros. + unfold Ptrofs.divs. + rewrite Ptrofs.unsigned_repr. + apply Z.quot_div_nonneg; lia. + split. + apply Z.quot_pos; lia. + apply Zquot.Zquot_le_upper_bound; try lia. + eapply Z.le_trans. + 2: { apply ZBinary.Z.le_mul_diag_r; simplify; try lia. } + pose proof (Ptrofs.signed_range x). + simplify; lia. + Qed. + Lemma mul_unsigned : forall x y, Ptrofs.mul x y = @@ -130,6 +166,20 @@ Module PtrofsExtra. apply Ptrofs.eqm_samerepr. apply Ptrofs.eqm_mult; exists 0; lia. Qed. + + Lemma pos_signed_unsigned : + forall x, + 0 <= Ptrofs.signed x -> + Ptrofs.signed x = Ptrofs.unsigned x. + Proof. + intros. + rewrite Ptrofs.unsigned_signed. + destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ. + unfold Ptrofs.lt in EQ. + destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate. + replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity. lia. + reflexivity. + Qed. End PtrofsExtra. Module IntExtra. |