🍃 Utils.v

Proofs

Gitlab

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.