🍃 Utils.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Ltac tezos_z_autounfold :=
autounfold with tezos_z;
unfold
Pervasives.normalize_int,
Pervasives.normalize_int32,
Pervasives.normalize_int64;
unfold
Pervasives.two_pow_31,
Pervasives.two_pow_32,
Pervasives.two_pow_62,
Pervasives.two_pow_63,
Pervasives.two_pow_64.
Ltac tezos_z_auto :=
tezos_z_autounfold; intros; lia.
Ltac tezos_z_easy :=
repeat (autounfold with tezos_z in *;
autorewrite with tezos_z in *); lia.
Lemma BinInt_Z_min_eq :∀ a b, a = b ∨ a < b → BinInt.Z.min a b = a.
unfold Z.min, BinInt.Z.min. intros.
destruct H.
rewrite H. now rewrite Z.compare_refl.
inversion H. now rewrite H1.
Qed.
Lemma BinInt_Z_max_eq : ∀ a b, a > b ∨ a = b → Z.max a b = a.
unfold Z.max, BinInt.Z.max. intros.
destruct H.
inversion H. now rewrite H1.
rewrite H.
now rewrite Z.compare_refl.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Ltac tezos_z_autounfold :=
autounfold with tezos_z;
unfold
Pervasives.normalize_int,
Pervasives.normalize_int32,
Pervasives.normalize_int64;
unfold
Pervasives.two_pow_31,
Pervasives.two_pow_32,
Pervasives.two_pow_62,
Pervasives.two_pow_63,
Pervasives.two_pow_64.
Ltac tezos_z_auto :=
tezos_z_autounfold; intros; lia.
Ltac tezos_z_easy :=
repeat (autounfold with tezos_z in *;
autorewrite with tezos_z in *); lia.
Lemma BinInt_Z_min_eq :∀ a b, a = b ∨ a < b → BinInt.Z.min a b = a.
unfold Z.min, BinInt.Z.min. intros.
destruct H.
rewrite H. now rewrite Z.compare_refl.
inversion H. now rewrite H1.
Qed.
Lemma BinInt_Z_max_eq : ∀ a b, a > b ∨ a = b → Z.max a b = a.
unfold Z.max, BinInt.Z.max. intros.
destruct H.
inversion H. now rewrite H1.
rewrite H.
now rewrite Z.compare_refl.
Qed.