Skip to main content

🍬 Script_list.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Proofs.Utils.

Module Valid.
  Definition t {a : Set} (l : Script_typed_ir.boxed_list a) : Prop :=
    List.length l.(Script_typed_ir.boxed_list.elements) =
    l.(Script_typed_ir.boxed_list.length).
End Valid.

Lemma empty_is_valid {a : Set} : Valid.t (Script_list.empty (a := a)).
  reflexivity.
Qed.

Lemma cons_is_valid {a : Set} {v : a} {l}
  : Valid.t l Valid.t (Script_list.cons_value v l).
  unfold Valid.t; intro H; cbn - ["+i"].
  Utils.tezos_z_auto.
Qed.