Library zoo_std.glist

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.glist__code.
Require Import zoo_std.glist__types.
Require Import zoo.options.

Implicit Type v : val.
Implicit Type vs : list val.

Fixpoint glist۰to_val vs :=
  match vs with
  | [] ⇒
      §Nil%V
  | v :: vs ⇒
      ‘Cons[ 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 [] = §Nil%V.
Lemma glist۰to_valｰcons v vs :
  glist۰to_val (v :: vs) = ‘Cons[ v, glist۰to_val vs ]%V.
Lemma glist۰to_valｰsingleton v :
  glist۰to_val [v] = ‘Cons[ v, §Nil ]%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.

Require zoo_std.glist__opaque.