Library zoo_std.glist

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  glist__types
  glist__code.
From zoo Require Import
  options.

Implicit Types v : val.
Implicit Types vs : list val.

Fixpoint glist_to_val vs :=
  match vs with
  | [] ⇒
      §Gnil%V
  | v :: vs ⇒
      ‘Gcons[ v, glist_to_val vs ]%V
  end.
#[global] Arguments glist_to_val !_ / : assert.

#[global] Instance glist_to_val_inj_similar :
  Inj (=) (≈@{val}) glist_to_val.
#[global] Instance glist_to_val_inj :
  Inj (=) (=) glist_to_val.

Lemma glist_to_val_nil :
  glist_to_val [] = §Gnil%V.
Lemma glist_to_val_cons v vs :
  glist_to_val (v :: vs) = ‘Gcons[ v, glist_to_val vs ]%V.
Lemma glist_to_val_singleton v :
  glist_to_val [v] = ‘Gcons[ v, §Gnil ]%V.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Definition glist_model' t vs :=
    t = glist_to_val vs.
  Definition glist_model t vs : iProp Σ :=
    ⌜glist_model' t vs⌝.

  Lemma glist٠rev_app𑁒spec {t1} vs1 {t2} vs2 :
    glist_model' t1 vs1 →
    glist_model' t2 vs2 →
    {{{
      True
    }}}
      glist٠rev_app t1 t2
    {{{
      RET glist_to_val (reverse vs1 ++ vs2);
      True
    }}}.

  Lemma glist٠rev𑁒spec {t} vs :
    glist_model' t vs →
    {{{
      True
    }}}
      glist٠rev t
    {{{
      RET glist_to_val (reverse vs);
      True
    }}}.
End zoo_G.

From zoo_std Require
  glist__opaque.