🍃 Z.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Int32.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.
Lemma compare_is_valid
: Proofs.Compare.Valid.t (fun _ ⇒ True) id Z.compare.
Proof.
exact Compare.z_is_valid.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Int32.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.
Lemma compare_is_valid
: Proofs.Compare.Valid.t (fun _ ⇒ True) id Z.compare.
Proof.
exact Compare.z_is_valid.
Qed.
When in bounds, the conversion to [int] is the identity.
Lemma to_int_eq (z : Z.t) :
Pervasives.Int.Valid.t z →
Z.to_int z = z.
Proof.
intros.
unfold Z.to_int.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
Pervasives.Int.Valid.t z →
Z.to_int z = z.
Proof.
intros.
unfold Z.to_int.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
When in bounds, the conversion to [int32] is the identity.
Lemma to_int32_eq (z : Z.t) :
Int32.Valid.t z →
Z.to_int32 z = z.
Proof.
intros.
unfold Z.to_int32.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
Int32.Valid.t z →
Z.to_int32 z = z.
Proof.
intros.
unfold Z.to_int32.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
When in bounds, the conversion to [int64] is the identity.
Lemma to_int64_eq (z : Z.t) :
Int64.Valid.t z →
Z.to_int64 z = z.
Proof.
intros.
unfold Z.to_int64.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
Axiom to_string_of_string_eq : ∀ s,
to_string (of_string s) = s.
Int64.Valid.t z →
Z.to_int64 z = z.
Proof.
intros.
unfold Z.to_int64.
do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
try reflexivity;
lia.
Qed.
Axiom to_string_of_string_eq : ∀ s,
to_string (of_string s) = s.
[shift_left a b] is positive if [a] is positive
[shift_right a b] is positive if [a] is positive
Lemma shift_right_pos (a b : Z.t) :
0 ≤ a →
0 ≤ shift_right a b.
Proof.
unfold shift_right, Z.shiftr.
apply Z.shiftl_nonneg.
Qed.
0 ≤ a →
0 ≤ shift_right a b.
Proof.
unfold shift_right, Z.shiftr.
apply Z.shiftl_nonneg.
Qed.
[logor a b] is positive if [a] and [b] are positive
[logand a b] is positive if either [a] or [b] is positive
Lemma logand_pos (a b : Z.t) :
0 ≤ a ∨ 0 ≤ b →
0 ≤ logand a b.
Proof.
unfold logand.
now rewrite Z.land_nonneg.
Qed.
0 ≤ a ∨ 0 ≤ b →
0 ≤ logand a b.
Proof.
unfold logand.
now rewrite Z.land_nonneg.
Qed.
[logxor a b] is positive when a is positive iff b is positive
Lemma logxor_pos (a b : Z.t) :
(0 ≤ a ↔ 0 ≤ b) →
0 ≤ logxor a b.
Proof.
unfold logxor.
now rewrite Z.lxor_nonneg.
Qed.
(0 ≤ a ↔ 0 ≤ b) →
0 ≤ logxor a b.
Proof.
unfold logxor.
now rewrite Z.lxor_nonneg.
Qed.
The function [numbits] returns a non-negative [int].
[Z.compare a b <= 0] implies [a <= b]