Skip to main content

🍬 Script_set.v


See code, Gitlab , OCaml

We axiomatize that if we [add] and element to the set, which is alsready in the set, i.e. [mem elem set = true], then set wouldn't change.
Axiom BOXED_set_OPS_add_existing :
    (a : Ty.t) (t : Set)
    (OPS : Script_typed_ir.Boxed_set_OPS (t:=t) (elt:= Ty.to_Set a))
    (boxed : t)
    (v : Ty.to_Set a),
    OPS.(Script_typed_ir.Boxed_set_OPS.mem) v boxed = true
    (OPS.(Script_typed_ir.Boxed_set_OPS.add) v boxed) = boxed.

Updating a valid set returns a valid set.
Lemma update_is_valid {a : Ty.t} (v : Ty.to_Set a)
  (b : bool) (x : Script_typed_ir.set (Ty.to_Set a)) :
  Script_typed_ir.Valid.value a v
  Script_typed_ir.Valid.value (Ty.Set_ a) x
  Script_typed_ir.Valid.value (Ty.Set_ a) (Script_set.update v b x).
  intros Hv Hax.
  unfold Script_set.update.
  step. step.
  destruct b0. simpl.
  { step.
    { rewrite BOXED_set_OPS_add_existing; trivial. }
    { admit. } (* axiom that if we add new element, size increases.  *)
  { step.
    { admit. } (* axiom that if we remove existing element size decreases *)
    { admit. } (* axiom that if we remove non-existing element,
                  size stays the same *)