🍃 Int32.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.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]

Lemma non_negative_impl_t a :
  Int32.Valid.non_negative a →
  Int32.Valid.t a.
Proof.
  lia.
Qed.