Skip to main content

🧰 Utils.v

Proofs

Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.

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.