Library zoo_std.clist

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.clist__code.
Require Import zoo_std.clist__types.
Require Import zoo.options.

Implicit Type v t fn : val.

Inductive clist :=
  | Closed
  | Open
  | Cons v (cvs : clist).
Implicit Type cvs : clist.

Fixpoint clist۰to_val cvs :=
  match cvs with
  | Closed ⇒
      §Closed
  | Open ⇒
      §Open
  | Cons v cvs ⇒
      ‘Cons[ v, clist۰to_val cvs ]
  end%V.
Coercion clist۰to_val : clist >-> val.

#[global] Instance clist۰to_valｰinjｰsimilar :
  Inj (=) (≈@{val}) clist۰to_val.
#[global] Instance clist۰to_valｰinj :
  Inj (=) (=) clist۰to_val.

Fixpoint list۰to_clist_open vs :=
  match vs with
  | [] ⇒
      Open
  | v :: vs ⇒
      Cons v (list۰to_clist_open vs)
  end.
Fixpoint list۰to_clist_closed vs :=
  match vs with
  | [] ⇒
      Closed
  | v :: vs ⇒
      Cons v (list۰to_clist_closed vs)
  end.

#[global] Instance list۰to_clist_openｰinj :
  Inj (=) (=) list۰to_clist_open.
#[global] Instance list۰to_clist_closedｰinj :
  Inj (=) (=) list۰to_clist_closed.
Lemma list۰to_clistｰopenｰclosed vs1 vs2 :
  list۰to_clist_open vs1 ≠ list۰to_clist_closed vs2.
Lemma list۰to_clist_openｰnotｰclosed vs :
  list۰to_clist_open vs ≠ Closed.
Lemma list۰to_clist_openｰnotｰclosed' vs :
  Closed ≠ list۰to_clist_open vs.

Fixpoint clist۰app vs1 cvs2 :=
  match vs1 with
  | [] ⇒
      cvs2
  | v :: vs1 ⇒
      Cons v (clist۰app vs1 cvs2)
  end.

Lemma clist۰appｰopen {vs1 cvs2} vs2 :
  cvs2 = list۰to_clist_open vs2 →
  clist۰app vs1 cvs2 = list۰to_clist_open (vs1 ++ vs2).
Lemma clist۰appｰOpen vs :
  clist۰app vs Open = list۰to_clist_open vs.
Lemma clist۰appｰclosed {vs1 cvs2} vs2 :
  cvs2 = list۰to_clist_closed vs2 →
  clist۰app vs1 cvs2 = list۰to_clist_closed (vs1 ++ vs2).
Lemma clist۰appｰClosed vs :
  clist۰app vs Closed = list۰to_clist_closed vs.
Lemma clist۰appｰassoc vs1 vs2 cvs :
  clist۰app (vs1 ++ vs2) cvs = clist۰app vs1 (clist۰app vs2 cvs).

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  Lemma wpｰmatchｰclistｰopen vs e1 x2 e2 Φ :
    WP subst' x2 (list۰to_clist_open vs) e2 {{ Φ }} ⊢
    WP 𝗺𝗮𝘁𝗰𝗵 list۰to_clist_open vs 𝘄𝗶𝘁𝗵 Closed → e1 | ⎽ 𝗮𝘀: x2 → e2 𝗲𝗻𝗱 {{ Φ }}.

  Lemma clist٠appｰspec {t1} vs1 {t2} cvs2 :
    t1 = list۰to_clist_open vs1 →
    t2 = cvs2 →
    {{{
      True
    }}}
      clist٠app t1 t2
    {{{
      RET clist۰app vs1 cvs2;
      True
    }}}.

  Lemma clist٠rev_appｰspec {t1} vs1 {t2} cvs2 :
    t1 = list۰to_clist_open vs1 →
    t2 = cvs2 →
    {{{
      True
    }}}
      clist٠rev_app t1 t2
    {{{
      RET clist۰app (reverse vs1) cvs2;
      True
    }}}.

  #[local] Lemma clist٠iterｰspecｰaux vs_left Ψ vs fn t vs_right :
    vs = vs_left ++ vs_right →
    t = list۰to_clist_open vs_right →
    {{{
      ▷ Ψ vs_left ∗
      ( [∗ list] i ↦ v ∈ vs_right,
        Ψ (vs_left ++ take i vs_right) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (vs_left ++ take i vs_right ++ [v])
        }}
      )
    }}}
      clist٠iter fn t
    {{{
      RET ();
      Ψ vs
    }}}.
  Lemma clist٠iterｰspec Ψ t vs fn :
    t = list۰to_clist_open vs →
    {{{
      ▷ Ψ [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (take i vs ++ [v])
        }}
      )
    }}}
      clist٠iter fn t
    {{{
      RET ();
      Ψ vs
    }}}.
  Lemma clist٠iterｰspecｰdisentangled Ψ t vs fn :
    t = list۰to_clist_open vs →
    {{{
      [∗ list] v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ v
        }}
    }}}
      clist٠iter fn t
    {{{
      RET ();
      [∗ list] v ∈ vs,
        Ψ v
    }}}.
End zoo۰G.

Require zoo_std.clist__opaque.