🍬 Script_list.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Module Valid.
The validity predicate for the type [Script_list.t] .
Definition t {a : Set} (l : Script_list.t a) : Prop :=
List.length l.(Script_list.t.elements) =
l.(Script_list.t.length).
End Valid.
List.length l.(Script_list.t.elements) =
l.(Script_list.t.length).
End Valid.
The [empty] definition from [Script_list] is valid.
The function [cons_value] is valid.
Lemma cons_value_is_valid {a} {v : Ty.to_Set a} {l}
: Pervasives.Int.Valid.non_negative
(l.(Script_list.t.length))%Z →
1 + l.(Script_list.t.length) ≤ Pervasives.max_int →
Script_typed_ir.Valid.value a v →
Script_typed_ir.Valid.value (Ty.List a) l →
Script_typed_ir.Valid.value (Ty.List a) (Script_list.cons_value v l).
Proof.
intros.
unfold Script_list.cons_value, "+i".
rewrite Pervasives.normalize_identity.
sauto lq: on.
hfcrush.
Qed.
: Pervasives.Int.Valid.non_negative
(l.(Script_list.t.length))%Z →
1 + l.(Script_list.t.length) ≤ Pervasives.max_int →
Script_typed_ir.Valid.value a v →
Script_typed_ir.Valid.value (Ty.List a) l →
Script_typed_ir.Valid.value (Ty.List a) (Script_list.cons_value v l).
Proof.
intros.
unfold Script_list.cons_value, "+i".
rewrite Pervasives.normalize_identity.
sauto lq: on.
hfcrush.
Qed.