Skip to main content

🍬 Script_set.v

Proofs

See code, See simulations, Gitlab , OCaml

The simulation [dep_empty] is valid.
Lemma dep_empty_eq {a : Ty.t} (ty : With_family.ty a) :
  Script_typed_ir.With_family.is_Comparable ty
  With_family.to_set (Script_set.dep_empty ty) =
  Script_set.empty (With_family.to_ty ty).
Proof.
  intros.
  unfold With_family.to_set, Script_set.dep_empty, Script_set.empty; simpl.
  repeat f_equal.
  all: try (
    rewrite (Script_comparable.dep_compare_comparable_eq _ ty) by assumption;
    reflexivity
  ).
  apply FunctionalExtensionality.functional_extensionality_dep; intro.
  apply Gas_comparable_input_size.dep_size_of_comparable_value_eq.
Qed.

The simulation [dep_update] is valid.
Lemma dep_update_eq {a : Ty.t} (v : With_family.ty_to_dep_Set a) (b : bool)
  (x : With_family.set a) :
  With_family.to_set (Script_set.dep_update v b x) =
  Script_set.update (With_family.to_value v) b (With_family.to_set x).
Proof.
  unfold With_family.to_set, Script_set.dep_update, Script_set.update; simpl.
  repeat f_equal.
  rewrite Map.mem_from_find.
  pose proof (Map.cardinal_is_valid _ x).
  destruct b.
  { rewrite Map.cardinal_add_find.
    destruct (_.(Map.S.find) _ _); lia.
  }
  { rewrite Map.cardinal_remove_find.
    destruct (_.(Map.S.find) _ _); lia.
  }
Qed.

The simulation [dep_mem] is valid.
The simulation [dep_fold] is valid.
Lemma dep_fold_eq {elt : Ty.t} {acc : Set}
  (dep_f : With_family.ty_to_dep_Set elt acc acc)
  (f : Ty.to_Set elt acc acc) (x : With_family.set elt) (init : acc) :
  Script_family.Ty.is_Comparable elt
  ( k init,
    dep_f k init = f (With_family.to_value k) init
  )
  Script_set.dep_fold dep_f x init =
  Script_set.fold f (With_family.to_set x) init.
Proof.
  intros.
  unfold Script_set.dep_fold, Script_set.fold; simpl.
  f_equal.
  repeat (apply FunctionalExtensionality.functional_extensionality_dep; intro).
  pose proof (Script_typed_ir.With_family.to_value_of_value (ty := elt)).
  hfcrush.
Qed.

The simulation [dep_size_value] is valid.