🍃 Int64.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.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 i ⇒ Int64.to_string i = s
| None ⇒ True
end.
Axiom of_string_opt_is_valid : ∀ s,
match Int64.of_string_opt s with
| Some i ⇒ Valid.t i
| None ⇒ True
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.
∃ 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 i ⇒ Int64.to_string i = s
| None ⇒ True
end.
Axiom of_string_opt_is_valid : ∀ s,
match Int64.of_string_opt s with
| Some i ⇒ Valid.t i
| None ⇒ True
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
Subtraction identity in Z
Division identity in Z
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.
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.