Skip to main content

🍃 Int64.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V7.Proofs.Utils.

Module Valid.
  Definition t (n : int64) : Prop :=
    Int64.min_int n Int64.max_int.
  #[global] Hint Unfold t : tezos_z.

  Definition positive (n : int64) : Prop :=
    0 < n Int64.max_int.
  #[global] Hint Unfold positive : tezos_z.

  Definition non_negative (n : int64) : Prop :=
    0 n Int64.max_int.
  #[global] Hint Unfold non_negative : tezos_z.
End Valid.

Lemma normalize_is_valid (n : Z.t) : Valid.t (Pervasives.normalize_int64 n).
Proof.
  lia.
Qed.

Lemma normalize_identity (n : Z.t) :
  Valid.t n Pervasives.normalize_int64 n = n.
  lia.
Qed.

Lemma int64_add_is_valid a b : Valid.t (a +i64 b). lia. Qed.
Lemma int64_mul_is_valid a b : Valid.t (a ×i64 b). lia. Qed.
Lemma int64_div_is_valid a b : Valid.t (a /i64 b). lia. Qed.
Lemma int64_sub_is_valid a b : Valid.t (a -i64 b). lia. Qed.

Lemma int64_add_assoc a b c : a +i64 b +i64 c = a +i64 (b +i64 c).
Proof.
  lia.
Qed.

Lemma normalize_int64_0_r a : (a + Pervasives.normalize_int64 0)%Z = a.
Proof.
  lia.
Qed.

Lemma normalize_int64_0_l a : (Pervasives.normalize_int64 0 + a)%Z = a.
Proof.
  lia.
Qed.

Lemma normalize_int64_lte_max_int a :
  Pervasives.normalize_int64 a Int64.max_int.
Proof.
  lia.
Qed.

normalize is not distrubutive
Lemma normalize_add_not_distr :
   a b, Valid.t a Valid.t b
  Pervasives.normalize_int64 (a + b)%Z (Pervasives.normalize_int64 a + Pervasives.normalize_int64 b)%Z.
Proof.
   1, max_int.
  lia.
Qed.

Lemma normalize_mul_not_distr :
   a b, Valid.t a Valid.t b
  Pervasives.normalize_int64 (a × b)%Z (Pervasives.normalize_int64 a × Pervasives.normalize_int64 b)%Z.
Proof.
   2, max_int.
  lia.
Qed.

Lemma normalize_div_mul_false : i p,
    Int64.Valid.t i
    Int64.Valid.t p
    p 0
    (i ×i64 p) /i64 p i.
Proof.
   Int64.max_int, 2.
  unfold "<>".
  lia.
Qed.

Axiom of_string_opt_to_string : i,
  Int64.of_string_opt (Int64.to_string i) = Some i.

Axiom to_string_of_string_opt : s,
  match Int64.of_string_opt s with
  | Some iInt64.to_string i = s
  | NoneTrue
  end.

Axiom of_string_opt_is_valid : s,
  match Int64.of_string_opt s with
  | Some iValid.t i
  | NoneTrue
  end.

Axiom of_string_eq_some_implies_valid : s i,
  of_string_opt s = Some i Int64.Valid.t i.

Lemma of_int_is_valid : i,
  Pervasives.Int.Valid.t i
  Valid.t (Int64.of_int i).
Proof.
  lia.
Qed.

Addtion identity in Z
Lemma add_eq : a b,
  Valid.t (a +Z b) a +i64 b = a +Z b.
Proof.
  lia.
Qed.

Subtraction identity in Z
Lemma sub_eq : a b,
  Valid.t (a -Z b) a -i64 b = a -Z b.
Proof.
  lia.
Qed.

Division identity in Z
Lemma div_eq : a b,
  Valid.t (a ÷ b) a /i64 b = a ÷ b.
Proof.
  lia.
Qed.

Multiplication identity in Z
Lemma mul_eq : a b,
  Valid.t (a ×Z b) a ×i64 b = a ×Z b.
Proof.
  lia.
Qed.

Lemma add_sub_identity : (x y : Int64.t),
    Int64.Valid.t x
    Int64.Valid.t y
    x +i64 y -i64 x = y.
Proof.
  intros. lia.
Qed.

Lemma of_int_to_int : (i : int64),
  Pervasives.Int.Valid.t i Int64.of_int (Int64.to_int i) = i.
Proof.
  lia.
Qed.

Lemma to_int_of_int : (i : int64),
  Pervasives.Int.Valid.t i Int64.to_int (Int64.of_int i) = i.
Proof.
  lia.
Qed.