🍃 FallbackArray.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.List.

Properties of fallback arrays made from lists with optional elements.

Module Of_list.

Behavior of [FallbackArray.length].

  Lemma length_eq {a : Set} (l : list a) :
    let array := FallbackArray.of_list None Some l in
    FallbackArray.length array = List.length l.
  Proof.
    apply List.length_map.
  Qed.

Behavior of [FallbackArray.get].

  Lemma get_eq {a : Set} (l : list a) (index : int) :
    let array := FallbackArray.of_list None Some l in
    FallbackArray.get array index = List.nth l index.
  Proof.
    unfold FallbackArray.of_list, FallbackArray.get.
    generalize index; clear index.
    induction l; simpl in *; hauto lq: on.
  Qed.

Behavior of [FallbackArray.fold].

  Lemma fold_eq {a b : Set} (f : b → option a → b) (l : list a) (init : b) :
    let array := FallbackArray.of_list None Some l in
    FallbackArray.fold f array init =
      List.fold_left (fun acc item ⇒ f acc (Some item)) init l.
  Proof.
    unfold FallbackArray.of_list, FallbackArray.fold.
    generalize init; clear init.
    induction l; simpl in *; hauto lq: on.
  Qed.

Two fallback arrays are equal when their list of elements is.

  Lemma of_list_inj {a : Set} (l1 l2 : list a) :
    let array1 := FallbackArray.of_list None Some l1 in
    let array2 := FallbackArray.of_list None Some l2 in
    array1 = array2 → l1 = l2.
  Proof.
    unfold FallbackArray.of_list; simpl; intros H.
    assert (H_Some : List.map Some l1 = List.map Some l2) by hauto lq: on.
    clear H.
    generalize l2 H_Some; clear H_Some l2.
    induction l1; sauto lq: on rew: off.
  Qed.
End Of_list.