🪙 Tez_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require Import TezosOfOCaml.Environment.V8.Proofs.Utils.
Module Repr.
Module Valid.
Definition t (tz : Tez_repr.repr) :=
0 ≤ tz ≤ Int64.max_int.
#[global] Hint Unfold t : tezos_z.
Definition positive (tz : Tez_repr.repr) :=
0 < tz ≤ Int64.max_int.
#[global] Hint Unfold positive : tezos_z.
End Valid.
End Repr.
Module Valid.
Definition t (tz : Tez_repr.t) :=
let 'Tez_repr.Tez_tag repr := tz in
Repr.Valid.t repr.
#[global] Hint Unfold t : tezos_z.
Definition positive (tz : Tez_repr.t) :=
let 'Tez_repr.Tez_tag repr := tz in
Repr.Valid.positive repr.
#[global] Hint Unfold positive : tezos_z.
End Valid.
#[global] Hint Unfold
Tez_repr.op_minusquestion
Tez_repr.op_plusquestion
Tez_repr.op_starquestion
Tez_repr.op_divquestion
Tez_repr.sub_opt
Tez_repr.of_mutez
Tez_repr.to_mutez
Tez_repr.op_lteq
Tez_repr.op_lt
Tez_repr.op_eq
Tez_repr.op_gt
Tez_repr.of_string
: tezos_z.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require Import TezosOfOCaml.Environment.V8.Proofs.Utils.
Module Repr.
Module Valid.
Definition t (tz : Tez_repr.repr) :=
0 ≤ tz ≤ Int64.max_int.
#[global] Hint Unfold t : tezos_z.
Definition positive (tz : Tez_repr.repr) :=
0 < tz ≤ Int64.max_int.
#[global] Hint Unfold positive : tezos_z.
End Valid.
End Repr.
Module Valid.
Definition t (tz : Tez_repr.t) :=
let 'Tez_repr.Tez_tag repr := tz in
Repr.Valid.t repr.
#[global] Hint Unfold t : tezos_z.
Definition positive (tz : Tez_repr.t) :=
let 'Tez_repr.Tez_tag repr := tz in
Repr.Valid.positive repr.
#[global] Hint Unfold positive : tezos_z.
End Valid.
#[global] Hint Unfold
Tez_repr.op_minusquestion
Tez_repr.op_plusquestion
Tez_repr.op_starquestion
Tez_repr.op_divquestion
Tez_repr.sub_opt
Tez_repr.of_mutez
Tez_repr.to_mutez
Tez_repr.op_lteq
Tez_repr.op_lt
Tez_repr.op_eq
Tez_repr.op_gt
Tez_repr.of_string
: tezos_z.
[Tez_repr.op_minusquestion] is valid
Lemma op_minusquestion_is_valid : ∀ {t1 t2 : Tez_repr.t},
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.op_minusquestion t1 t2 with
| Pervasives.Ok t ⇒
let 'Tez_repr.Tez_tag t' := t in
t1' ≥ t2' ∧ Valid.t t ∧ t' = t1' - t2'
| Pervasives.Error _ ⇒ t1' < t2'
end.
Proof.
intros; unfold Tez_repr.op_minusquestion.
destruct_all Tez_repr.t.
destruct (_ ≤i64 _) eqn:?; simpl; lia.
Qed.
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.op_minusquestion t1 t2 with
| Pervasives.Ok t ⇒
let 'Tez_repr.Tez_tag t' := t in
t1' ≥ t2' ∧ Valid.t t ∧ t' = t1' - t2'
| Pervasives.Error _ ⇒ t1' < t2'
end.
Proof.
intros; unfold Tez_repr.op_minusquestion.
destruct_all Tez_repr.t.
destruct (_ ≤i64 _) eqn:?; simpl; lia.
Qed.
[Tez_repr.op_minusquestion] equals to subtraction in Z
Lemma op_minusquestion_eq : ∀ t1 t2,
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
match
Tez_repr.op_minusquestion (Tez_repr.Tez_tag t1) (Tez_repr.Tez_tag t2)
with
| Pervasives.Ok (Tez_repr.Tez_tag t) ⇒ t = t1 - t2
| Pervasives.Error _ ⇒ True
end.
Proof.
intros.
unfold Tez_repr.op_minusquestion.
destruct (_ ≤i64 _) eqn:?; simpl; trivial.
lia.
Qed.
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
match
Tez_repr.op_minusquestion (Tez_repr.Tez_tag t1) (Tez_repr.Tez_tag t2)
with
| Pervasives.Ok (Tez_repr.Tez_tag t) ⇒ t = t1 - t2
| Pervasives.Error _ ⇒ True
end.
Proof.
intros.
unfold Tez_repr.op_minusquestion.
destruct (_ ≤i64 _) eqn:?; simpl; trivial.
lia.
Qed.
[Tez_repr.sub_opt] is valid
Lemma sub_opt_is_valid : ∀ {t1 t2 : Tez_repr.t},
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.sub_opt t1 t2 with
| Some t ⇒
let 'Tez_repr.Tez_tag t' := t in
t1' ≥ t2' ∧ Valid.t t ∧ t' = t1' - t2'
| None ⇒ t1' < t2'
end.
Proof.
intros; unfold Tez_repr.sub_opt.
destruct_all Tez_repr.t.
destruct (_ ≤i64 _) eqn:?; simpl; lia.
Qed.
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.sub_opt t1 t2 with
| Some t ⇒
let 'Tez_repr.Tez_tag t' := t in
t1' ≥ t2' ∧ Valid.t t ∧ t' = t1' - t2'
| None ⇒ t1' < t2'
end.
Proof.
intros; unfold Tez_repr.sub_opt.
destruct_all Tez_repr.t.
destruct (_ ≤i64 _) eqn:?; simpl; lia.
Qed.
[Tez_repr.sub_opt] computes subtraction in Z
Lemma sub_opt_eq : ∀ t t1 t2,
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
Tez_repr.sub_opt
(Tez_repr.Tez_tag t1)
(Tez_repr.Tez_tag t2) = Some (Tez_repr.Tez_tag t) →
t = t1 - t2.
Proof.
simpl.
intros.
destruct (_ <=? _) eqn:?; [| discriminate].
unfold "-i64" in *; rewrite Int64.normalize_identity in × by lia.
congruence.
Qed.
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
Tez_repr.sub_opt
(Tez_repr.Tez_tag t1)
(Tez_repr.Tez_tag t2) = Some (Tez_repr.Tez_tag t) →
t = t1 - t2.
Proof.
simpl.
intros.
destruct (_ <=? _) eqn:?; [| discriminate].
unfold "-i64" in *; rewrite Int64.normalize_identity in × by lia.
congruence.
Qed.
The function [op_plusquestion] is valid
Lemma op_plusquestion_is_valid x1 x2 :
Tez_repr.Valid.t x1 →
letP? x3 := Tez_repr.op_plusquestion x1 x2 in
Tez_repr.Valid.t x3.
Proof.
intros.
unfold Tez_repr.op_plusquestion.
destruct x1, x2; cbn.
step; cbn; [easy|].
lia.
Qed.
Tez_repr.Valid.t x1 →
letP? x3 := Tez_repr.op_plusquestion x1 x2 in
Tez_repr.Valid.t x3.
Proof.
intros.
unfold Tez_repr.op_plusquestion.
destruct x1, x2; cbn.
step; cbn; [easy|].
lia.
Qed.
@Q is this lemma useful? When the first parameter is positive, [op_plus_question]
outputs a positive integer.
Lemma op_plusquestion_is_valid_positive x1 x2 :
Tez_repr.Valid.positive x1 →
letP? x3 := Tez_repr.op_plusquestion x1 x2 in
Tez_repr.Valid.positive x3.
Proof.
intros.
unfold Tez_repr.op_plusquestion.
destruct x1, x2; cbn.
step; cbn; [easy|].
split ; lia.
Qed.
Tez_repr.Valid.positive x1 →
letP? x3 := Tez_repr.op_plusquestion x1 x2 in
Tez_repr.Valid.positive x3.
Proof.
intros.
unfold Tez_repr.op_plusquestion.
destruct x1, x2; cbn.
step; cbn; [easy|].
split ; lia.
Qed.
[Tez_repr.op_plusquestion] computes addition in Z
Lemma op_plusquestion_eq : ∀ t t1 t2,
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
Tez_repr.op_plusquestion
(Tez_repr.Tez_tag t1)
(Tez_repr.Tez_tag t2) = return? (Tez_repr.Tez_tag t) →
t = t1 +Z t2.
Proof.
simpl; intros.
destruct (_ <? _) eqn:?; [discriminate | ].
unfold "+i64" in *; rewrite Int64.normalize_identity in × by lia.
sauto q: on.
Qed.
Valid.t (Tez_repr.Tez_tag t1) →
Valid.t (Tez_repr.Tez_tag t2) →
Tez_repr.op_plusquestion
(Tez_repr.Tez_tag t1)
(Tez_repr.Tez_tag t2) = return? (Tez_repr.Tez_tag t) →
t = t1 +Z t2.
Proof.
simpl; intros.
destruct (_ <? _) eqn:?; [discriminate | ].
unfold "+i64" in *; rewrite Int64.normalize_identity in × by lia.
sauto q: on.
Qed.
[Tez_repr.mul_pos] is valid
Lemma mul_pos_is_valid : ∀ {t1 t2 : Z.t},
Int64.Valid.non_negative t1 →
Int64.Valid.positive t2 →
t1 ≤ Int64.max_int / t2 → Int64.Valid.t (t1 × t2)%Z.
intros t1 t2 [Ht11 Ht12] [Ht21 Ht22] H__t1t3;
unfold Int64.Valid.t, min_int; split; [lia | ];
replace (t1 × t2)%Z with (t2 × t1)%Z by lia;
replace max_int with (max_int × 1)%Z by lia;
replace 1 with (t2 / t2) by (apply Z_div_same; lia).
assert(t2 × t1 ≤ t2 × (max_int / t2))
by (apply Zmult_le_compat_l; [assumption | lia]).
assert(t2 × (max_int / t2) ≤ max_int × (t2 / t2))
by (
replace (max_int × (t2 / t2))%Z
with (max_int × t2 / t2)%Z
by (rewrite Z_div_mult, Z_div_same; lia);
replace (max_int × t2)%Z
with (t2 × max_int)%Z by lia;
apply Zdiv_mult_le; lia
); lia.
Qed.
Int64.Valid.non_negative t1 →
Int64.Valid.positive t2 →
t1 ≤ Int64.max_int / t2 → Int64.Valid.t (t1 × t2)%Z.
intros t1 t2 [Ht11 Ht12] [Ht21 Ht22] H__t1t3;
unfold Int64.Valid.t, min_int; split; [lia | ];
replace (t1 × t2)%Z with (t2 × t1)%Z by lia;
replace max_int with (max_int × 1)%Z by lia;
replace 1 with (t2 / t2) by (apply Z_div_same; lia).
assert(t2 × t1 ≤ t2 × (max_int / t2))
by (apply Zmult_le_compat_l; [assumption | lia]).
assert(t2 × (max_int / t2) ≤ max_int × (t2 / t2))
by (
replace (max_int × (t2 / t2))%Z
with (max_int × t2 / t2)%Z
by (rewrite Z_div_mult, Z_div_same; lia);
replace (max_int × t2)%Z
with (t2 × max_int)%Z by lia;
apply Zdiv_mult_le; lia
); lia.
Qed.
[Tez_repr.op_starquestion] is valid
Lemma op_starquestion_is_valid (t1 : Tez_repr.t) (t2 : int64) :
Valid.t t1 →
Int64.Valid.t t2 →
letP? t := Tez_repr.op_starquestion t1 t2 in
Valid.t t.
Proof.
intros.
unfold Tez_repr.op_starquestion.
destruct t1.
destruct (_ <i64 _) eqn:?; simpl; [easy | ].
destruct (_ =? _) eqn:?; simpl; [lia | ].
destruct (_ >? _) eqn:H_div64; simpl; [easy | ].
assert (Int64.Valid.t (max_int ÷ t2)) as H_div by nia.
unfold "/i64" in H_div64.
rewrite (Int64.normalize_identity _ H_div) in H_div64.
nia.
Qed.
Valid.t t1 →
Int64.Valid.t t2 →
letP? t := Tez_repr.op_starquestion t1 t2 in
Valid.t t.
Proof.
intros.
unfold Tez_repr.op_starquestion.
destruct t1.
destruct (_ <i64 _) eqn:?; simpl; [easy | ].
destruct (_ =? _) eqn:?; simpl; [lia | ].
destruct (_ >? _) eqn:H_div64; simpl; [easy | ].
assert (Int64.Valid.t (max_int ÷ t2)) as H_div by nia.
unfold "/i64" in H_div64.
rewrite (Int64.normalize_identity _ H_div) in H_div64.
nia.
Qed.
[Tez_repr.op_starquestion] auxiliary function
Lemma op_starquestion_eq_helper : ∀ t t1 i,
Repr.Valid.t t1 →
Int64.Valid.positive i →
t1 ≤ (max_int /i64 i) →
t1 ×i64 i = t →
t = t1 ×Z i.
Proof.
intros.
unfold "/i64" in ×.
rewrite Int64.normalize_identity in × by nia.
nia.
Qed.
Repr.Valid.t t1 →
Int64.Valid.positive i →
t1 ≤ (max_int /i64 i) →
t1 ×i64 i = t →
t = t1 ×Z i.
Proof.
intros.
unfold "/i64" in ×.
rewrite Int64.normalize_identity in × by nia.
nia.
Qed.
[Tez_repr.op_starquestion] computes multiplication in Z
Lemma op_starquestion_eq : ∀ {t t1 i : int64},
Int64.Valid.non_negative i →
Valid.t (Tez_repr.Tez_tag t1) →
Tez_repr.op_starquestion (Tez_repr.Tez_tag t1) i = return? (Tez_repr.Tez_tag t) →
t = t1 ×Z i.
Proof.
unfold Tez_repr.op_starquestion.
intros t t1 i Hi H1.
repeat match goal with
| |- context [if ?e then _ else _] ⇒ destruct e eqn:?
end; [sauto q: on | hauto l: on | sauto q: on | ].
simpl in *;
unfold "return?"; intros H; injection H.
apply op_starquestion_eq_helper; lia.
Qed.
Int64.Valid.non_negative i →
Valid.t (Tez_repr.Tez_tag t1) →
Tez_repr.op_starquestion (Tez_repr.Tez_tag t1) i = return? (Tez_repr.Tez_tag t) →
t = t1 ×Z i.
Proof.
unfold Tez_repr.op_starquestion.
intros t t1 i Hi H1.
repeat match goal with
| |- context [if ?e then _ else _] ⇒ destruct e eqn:?
end; [sauto q: on | hauto l: on | sauto q: on | ].
simpl in *;
unfold "return?"; intros H; injection H.
apply op_starquestion_eq_helper; lia.
Qed.
[Tez_repr.op_divquestion] is valid
Lemma op_divquestion_is_valid : ∀ {t1 t2 : Tez_repr.t},
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.op_divquestion t1 t2' with
| Pervasives.Ok t ⇒ t2' ≠ 0 ∧ Valid.t t
| Pervasives.Error _ ⇒ t2' = 0
end.
intros [t1] [t2].
unfold Tez_repr.op_divquestion.
destruct (_ ≤i64 _) eqn:?; simpl; [lia | ].
split; [lia | ].
assert (0 ≤ t1 ÷ t2 ≤ t1) by nia.
lia.
Qed.
Valid.t t1 →
Valid.t t2 →
let 'Tez_repr.Tez_tag t1' := t1 in
let 'Tez_repr.Tez_tag t2' := t2 in
match Tez_repr.op_divquestion t1 t2' with
| Pervasives.Ok t ⇒ t2' ≠ 0 ∧ Valid.t t
| Pervasives.Error _ ⇒ t2' = 0
end.
intros [t1] [t2].
unfold Tez_repr.op_divquestion.
destruct (_ ≤i64 _) eqn:?; simpl; [lia | ].
split; [lia | ].
assert (0 ≤ t1 ÷ t2 ≤ t1) by nia.
lia.
Qed.
The function [op_divquestion] is valid (alternative version)
Lemma op_divquestion_is_valid' a b :
Tez_repr.Valid.t a →
Int64.Valid.t b →
letP? x := Tez_repr.op_divquestion a b in
Tez_repr.Valid.t x.
Proof.
intros H_a H_b.
unfold Tez_repr.op_divquestion.
destruct a.
step; [easy|]. simpl.
assert (b > 0) by lia.
unfold "/i64".
rewrite Int64.normalize_identity by nia.
nia.
Qed.
Tez_repr.Valid.t a →
Int64.Valid.t b →
letP? x := Tez_repr.op_divquestion a b in
Tez_repr.Valid.t x.
Proof.
intros H_a H_b.
unfold Tez_repr.op_divquestion.
destruct a.
step; [easy|]. simpl.
assert (b > 0) by lia.
unfold "/i64".
rewrite Int64.normalize_identity by nia.
nia.
Qed.
[Tez_repr.op_divquestion] auxiliary function
Lemma op_divquestion_eq_helper : ∀ r i t,
Valid.t (Tez_repr.Tez_tag r) →
Int64.Valid.positive i →
r /i64 i = t →
t = r ÷ i.
Proof.
autounfold with tezos_z.
intros.
rewrite Int64.normalize_identity in *; nia.
Qed.
Valid.t (Tez_repr.Tez_tag r) →
Int64.Valid.positive i →
r /i64 i = t →
t = r ÷ i.
Proof.
autounfold with tezos_z.
intros.
rewrite Int64.normalize_identity in *; nia.
Qed.
[Tez_repr.op_divquestion] computes division in Z
Lemma op_divquestion_eq : ∀ {t i : int64} {t1 : Tez_repr.t},
Int64.Valid.t i→
Valid.t t1 →
Tez_repr.op_divquestion t1 i = return? (Tez_repr.Tez_tag t) →
let 'Tez_repr.Tez_tag t1' := t1 in
t = t1' ÷ i.
Proof.
unfold Tez_repr.op_divquestion. simpl.
intros t i t1 Hi H.
destruct (_ <=? 0) eqn:?; [sauto q: on | ].
destruct t1. unfold "return?".
intros Hok. injection Hok.
apply op_divquestion_eq_helper; lia.
Qed.
Int64.Valid.t i→
Valid.t t1 →
Tez_repr.op_divquestion t1 i = return? (Tez_repr.Tez_tag t) →
let 'Tez_repr.Tez_tag t1' := t1 in
t = t1' ÷ i.
Proof.
unfold Tez_repr.op_divquestion. simpl.
intros t i t1 Hi H.
destruct (_ <=? 0) eqn:?; [sauto q: on | ].
destruct t1. unfold "return?".
intros Hok. injection Hok.
apply op_divquestion_eq_helper; lia.
Qed.
Tez_repr.op_mutez is valid
Lemma of_mutez_is_valid : ∀ {t1 : Tez_repr.t},
Valid.t t1 →
let 'Tez_repr.Tez_tag t1' := t1 in
Tez_repr.of_mutez t1' = Some t1.
autounfold with tezos_z; intros t1 H1; destruct t1 as [t1]; simpl.
destruct (Z.ltb_spec t1 0); auto; lia.
Qed.
Valid.t t1 →
let 'Tez_repr.Tez_tag t1' := t1 in
Tez_repr.of_mutez t1' = Some t1.
autounfold with tezos_z; intros t1 H1; destruct t1 as [t1]; simpl.
destruct (Z.ltb_spec t1 0); auto; lia.
Qed.
[Tez_repr.of_mutez] wraps the identity on positive integers
Lemma of_mutez_eq : ∀ {i : int64},
Int64.Valid.non_negative i →
Tez_repr.of_mutez i = Some (Tez_repr.Tez_tag i).
Proof.
intros.
unfold Tez_repr.of_mutez.
destruct (_ <i64 _) eqn:?; lia.
Qed.
Int64.Valid.non_negative i →
Tez_repr.of_mutez i = Some (Tez_repr.Tez_tag i).
Proof.
intros.
unfold Tez_repr.of_mutez.
destruct (_ <i64 _) eqn:?; lia.
Qed.
[Tez_repr.of_string] is valid
Lemma of_string_is_valid : ∀ (s_value : string),
match Tez_repr.of_string s_value with
| Some (Tez_repr.Tez_tag t) ⇒ Int64.Valid.t t
| None ⇒ True
end.
intros.
unfold Tez_repr.of_string.
destruct (String.split_on_char _ _); [easy |].
repeat match goal with
| l : list string |- context[match l with _ ⇒ _ end] ⇒ destruct l
| |- context[if ?e then _ else _] ⇒ destruct e
| |- match Option.map _ ?e with _ ⇒ _ end ⇒
destruct e eqn:Hoptmatch; simpl; [ | easy];
apply Int64.of_string_eq_some_implies_valid in Hoptmatch;
easy
| |- match ?t with Tez_repr.Tez_tag t' ⇒ Int64.Valid.t t' end ⇒ destruct t
end; trivial.
Qed.
match Tez_repr.of_string s_value with
| Some (Tez_repr.Tez_tag t) ⇒ Int64.Valid.t t
| None ⇒ True
end.
intros.
unfold Tez_repr.of_string.
destruct (String.split_on_char _ _); [easy |].
repeat match goal with
| l : list string |- context[match l with _ ⇒ _ end] ⇒ destruct l
| |- context[if ?e then _ else _] ⇒ destruct e
| |- match Option.map _ ?e with _ ⇒ _ end ⇒
destruct e eqn:Hoptmatch; simpl; [ | easy];
apply Int64.of_string_eq_some_implies_valid in Hoptmatch;
easy
| |- match ?t with Tez_repr.Tez_tag t' ⇒ Int64.Valid.t t' end ⇒ destruct t
end; trivial.
Qed.
[Tez_repr.encoding] is valid
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Tez_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros.
destruct_all Tez_repr.t; simpl.
unfold Z.of_int64.
unfold Json.wrap_error.
rewrite Z.to_int64_eq by lia.
split; [lia | reflexivity].
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros.
destruct_all Tez_repr.t; simpl.
unfold Z.of_int64.
unfold Json.wrap_error.
rewrite Z.to_int64_eq by lia.
split; [lia | reflexivity].
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[Tez_repr.compare] is valid
Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Tez_repr.compare.
Proof.
apply (Compare.equality (
let proj '(Tez_repr.Tez_tag t) := t in
Compare.projection proj Compare.Int64.(Compare.S.compare)
)); [sauto lq: on | ].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.int64_is_valid.
}
{ trivial. }
{ sauto q: on. }
Qed.
Proof.
apply (Compare.equality (
let proj '(Tez_repr.Tez_tag t) := t in
Compare.projection proj Compare.Int64.(Compare.S.compare)
)); [sauto lq: on | ].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.int64_is_valid.
}
{ trivial. }
{ sauto q: on. }
Qed.
[op_minusquestion] with [Tez_repr.zero] forms an identity
Lemma op_minusquestion_zero_id
(t : Tez_repr.t) :
Tez_repr.Valid.t t →
Tez_repr.op_minusquestion t Tez_repr.zero = Pervasives.Ok t.
Proof.
intros. unfold Tez_repr.zero. destruct t.
unfold Tez_repr.Valid.t, Tez_repr.Repr.Valid.t in H.
unfold Tez_repr.op_minusquestion. simpl.
replace (BinInt.Z.leb BinNums.Z0 r) with true by lia.
unfold "-i64".
rewrite Int64.normalize_identity; [| lia].
now replace (r - 0) with r by lia.
Qed.
(t : Tez_repr.t) :
Tez_repr.Valid.t t →
Tez_repr.op_minusquestion t Tez_repr.zero = Pervasives.Ok t.
Proof.
intros. unfold Tez_repr.zero. destruct t.
unfold Tez_repr.Valid.t, Tez_repr.Repr.Valid.t in H.
unfold Tez_repr.op_minusquestion. simpl.
replace (BinInt.Z.leb BinNums.Z0 r) with true by lia.
unfold "-i64".
rewrite Int64.normalize_identity; [| lia].
now replace (r - 0) with r by lia.
Qed.