🍬 Michelson_v1_primitives.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Definition prim_encoding_eq (prim1 prim2 : Michelson_v1_primitives.prim)
  : bool :=
  String.eqb
    (Michelson_v1_primitives.string_of_prim prim1)
    (Michelson_v1_primitives.string_of_prim prim2).

Lemma prim_encoding_eq_implies_eq prim1 prim2
  : prim_encoding_eq prim1 prim2 = true →
    prim1 = prim2.
  destruct prim1, prim2; cbv; congruence.
Qed.

We use the decidable equality on [prim] in order to have a proof which is fast to build.

Lemma prim_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True) Michelson_v1_primitives.prim_encoding.
  eapply Data_encoding.Valid.implies.
  unfold Michelson_v1_primitives.prim_encoding.
  apply Data_encoding.Valid.def.
  apply Data_encoding.Valid.string_enum_dec;
    try apply prim_encoding_eq_implies_eq;
    try reflexivity.
  intros x H; cbv beta; simpl List.map.
  destruct x; reflexivity.
Qed.
#[global] Hint Resolve prim_encoding_is_valid : Data_encoding_db.