🍃 Int32.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Module Valid.
Definition t (n : int32) : Prop :=
Int32.min_int ≤ n ≤ Int32.max_int.
#[global] Hint Unfold t : tezos_z.
Definition non_negative (n : int32) : Prop :=
0 ≤ n ≤ Int32.max_int.
Definition positive (n : int32) : Prop :=
0 < n ≤ Int32.max_int.
Definition negative (i : Int32.t) :=
Int32.min_int ≤ i < 0.
#[global] Hint Unfold non_negative positive negative : tezos_z.
End Valid.
Lemma normalize_is_valid (n : Z.t) : Valid.t (Pervasives.normalize_int32 n).
lia.
Qed.
Lemma normalize_identity (n : Z.t) :
Valid.t n → Pervasives.normalize_int32 n = n.
lia.
Qed.
Lemma of_int_is_valid (i : int) :
Valid.t (Int32.of_int i).
lia.
Qed.
Lemma of_int_eq (i : int) :
Valid.t i → Int32.of_int i = i.
lia.
Qed.
Lemma of_int_to_int (i : int32) :
Valid.t i → Int32.of_int (Int32.to_int i) = i.
lia.
Qed.
Lemma to_int_of_int (i : int) :
Valid.t i → Int32.to_int (Int32.of_int i) = i.
lia.
Qed.
Axiom of_string_opt_to_string : ∀ i,
Int32.of_string_opt (Int32.to_string i) = Some i.
Axiom to_string_of_string_opt : ∀ s,
match Int32.of_string_opt s with
| Some i ⇒ Int32.to_string i = s
| None ⇒ True
end.
Lemma pred_neg_pred_neg_inverse (n : Int32.t) :
Int32.Valid.t n →
Int32.pred (Int32.neg (Int32.pred (Int32.neg n ))) = n.
intros H.
autounfold with tezos_z in *; unfold normalize_int32.
unfold two_pow_31, two_pow_32.
lia.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Module Valid.
Definition t (n : int32) : Prop :=
Int32.min_int ≤ n ≤ Int32.max_int.
#[global] Hint Unfold t : tezos_z.
Definition non_negative (n : int32) : Prop :=
0 ≤ n ≤ Int32.max_int.
Definition positive (n : int32) : Prop :=
0 < n ≤ Int32.max_int.
Definition negative (i : Int32.t) :=
Int32.min_int ≤ i < 0.
#[global] Hint Unfold non_negative positive negative : tezos_z.
End Valid.
Lemma normalize_is_valid (n : Z.t) : Valid.t (Pervasives.normalize_int32 n).
lia.
Qed.
Lemma normalize_identity (n : Z.t) :
Valid.t n → Pervasives.normalize_int32 n = n.
lia.
Qed.
Lemma of_int_is_valid (i : int) :
Valid.t (Int32.of_int i).
lia.
Qed.
Lemma of_int_eq (i : int) :
Valid.t i → Int32.of_int i = i.
lia.
Qed.
Lemma of_int_to_int (i : int32) :
Valid.t i → Int32.of_int (Int32.to_int i) = i.
lia.
Qed.
Lemma to_int_of_int (i : int) :
Valid.t i → Int32.to_int (Int32.of_int i) = i.
lia.
Qed.
Axiom of_string_opt_to_string : ∀ i,
Int32.of_string_opt (Int32.to_string i) = Some i.
Axiom to_string_of_string_opt : ∀ s,
match Int32.of_string_opt s with
| Some i ⇒ Int32.to_string i = s
| None ⇒ True
end.
Lemma pred_neg_pred_neg_inverse (n : Int32.t) :
Int32.Valid.t n →
Int32.pred (Int32.neg (Int32.pred (Int32.neg n ))) = n.
intros H.
autounfold with tezos_z in *; unfold normalize_int32.
unfold two_pow_31, two_pow_32.
lia.
Qed.
[non_negative a] implies [t a]