Library zoo_std.list

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

Implicit Types b : bool.
Implicit Types i j : nat.
Implicit Types v w t fn acc pred : val.
Implicit Types vs vs_left vs_right ws : list val.

Fixpoint plist_to_val nil vs :=
  match vs with
  | [] ⇒
      nil
  | v :: vs ⇒
      (v :: plist_to_val nil vs)%V
  end.
#[global] Arguments plist_to_val _ !_ : assert.

Lemma plist_to_val_nil nil :
  plist_to_val nil [] = nil.
Lemma plist_to_val_cons nil v vs :
  plist_to_val nil (v :: vs) = (v :: plist_to_val nil vs)%V.
Lemma plist_to_val_singleton nil v :
  plist_to_val nil [v] = (v :: nil)%V.
Lemma plist_to_val_app vs1 nil vs2 :
  plist_to_val (plist_to_val nil vs2) vs1 = plist_to_val nil (vs1 ++ vs2).

Fixpoint list_to_val vs :=
  match vs with
  | [] ⇒
      []%V
  | v :: vs ⇒
      (v :: list_to_val vs)%V
  end.
#[global] Arguments list_to_val !_ : assert.

Lemma list_to_val_plist_to_val vs :
  list_to_val vs = plist_to_val [] vs.

#[global] Instance list_to_val_inj :
  Inj (=) (=) list_to_val.

Lemma list_to_val_nil :
  list_to_val [] = []%V.
Lemma list_to_val_cons v vs :
  list_to_val (v :: vs) = (v :: list_to_val vs)%V.
Lemma list_to_val_singleton v :
  list_to_val [v] = (v :: [])%V.
Lemma list_to_val_app vs1 vs2 :
  plist_to_val (list_to_val vs2) vs1 = list_to_val (vs1 ++ vs2).

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

  Definition plist_model' t nil vs :=
    t = plist_to_val nil vs.
  Definition plist_model t nil vs : iProp Σ :=
    ⌜plist_model' t nil vs⌝.

  Definition list_model' t vs :=
    t = list_to_val vs.
  Definition list_model t vs : iProp Σ :=
    ⌜list_model' t vs⌝.

  Lemma list_model'_plist_model' t vs :
    list_model' t vs ↔
    plist_model' t [] vs.

  Lemma list٠singleton𑁒spec v :
    {{{
      True
    }}}
      list٠singleton v
    {{{
      t
    , RET t;
      list_model t [v]
    }}}.

  Lemma list٠head𑁒spec {t vs} v vs' :
    vs = v :: vs' →
    list_model' t vs →
    {{{
      True
    }}}
      list٠head t
    {{{
      RET v;
      True
    }}}.

  Lemma list٠tail𑁒spec {t vs} v vs' :
    vs = v :: vs' →
    list_model' t vs →
    {{{
      True
    }}}
      list٠tail t
    {{{
      t'
    , RET t';
      list_model t' vs'
    }}}.

  Lemma list٠is_empty𑁒spec t vs :
    list_model' t vs →
    {{{
      True
    }}}
      list٠is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      True
    }}}.

  Lemma list٠get𑁒spec v t (i : Z) vs :
    vs !! ₊i = Some v →
    list_model' t vs →
    {{{
      True
    }}}
      list٠get t #i
    {{{
      RET v;
      True
    }}}.

  #[local] Lemma list٠initi₀𑁒spec vs_left Ψ sz fn i :
    i ≤ ₊sz →
    i = length vs_left →
    {{{
      ▷ Ψ i vs_left ∗
      □ (
        ∀ i vs,
        ⌜i < ₊sz ∧ i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn #i {{ v,
          ▷ Ψ (S i) (vs ++ [v])
        }}
      )
    }}}
      list٠initi₀ #sz fn #i
    {{{
      t vs_right
    , RET t;
      ⌜(length vs_left + length vs_right)%nat = ₊sz⌝ ∗
      list_model t vs_right ∗
      Ψ ₊sz (vs_left ++ vs_right)
    }}}.
  Lemma list٠initi𑁒spec Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      □ (
        ∀ i vs,
        ⌜i < ₊sz ∧ i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn #i {{ v,
          ▷ Ψ (S i) (vs ++ [v])
        }}
      )
    }}}
      list٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma list٠initi𑁒spec' Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ vs,
        ⌜i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn #i {{ v,
          ▷ Ψ (S i) (vs ++ [v])
        }}
      )
    }}}
      list٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma list٠initi𑁒spec_disentangled Ψ sz fn :
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      list٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma list٠initi𑁒spec_disentangled' Ψ sz fn :
    {{{
      [∗ list] i ∈ seq 0 ₊sz,
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
    }}}
      list٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma list٠init𑁒spec Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      □ (
        ∀ i vs,
        ⌜i < ₊sz ∧ i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn () {{ v,
          ▷ Ψ (S i) (vs ++ [v])
        }}
      )
    }}}
      list٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma list٠init𑁒spec' Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ vs,
        ⌜i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn () {{ v,
          ▷ Ψ (S i) (vs ++ [v])
        }}
      )
    }}}
      list٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma list٠init𑁒spec_disentangled Ψ sz fn :
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn () {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      list٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma list٠init𑁒spec_disentangled' Ψ sz fn :
    {{{
      [∗ list] i ∈ seq 0 ₊sz,
        WP fn () {{ v,
          ▷ Ψ i v
        }}
    }}}
      list٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      list_model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  #[local] Lemma list٠foldli₀𑁒spec vs_left Ψ vs fn i acc t vs_right :
    vs = vs_left ++ vs_right →
    i = length vs_left →
    list_model' t vs_right →
    {{{
      ▷ Ψ i vs_left acc ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) acc -∗
        WP fn #i acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      list٠foldli₀ fn #i acc t
    {{{
      acc
    , RET acc;
      Ψ (length vs) vs acc
    }}}.
  Lemma list٠foldli𑁒spec Ψ fn acc t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] acc ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) acc -∗
        WP fn #i acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      list٠foldli fn acc t
    {{{
      acc
    , RET acc;
      Ψ (length vs) vs acc
    }}}.
  Lemma list٠foldli𑁒spec' Ψ fn acc t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] acc ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ i (take i vs) acc -∗
        WP fn #i acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      list٠foldli fn acc t
    {{{
      acc
    , RET acc;
      Ψ (length vs) vs acc
    }}}.

  Lemma list٠foldl𑁒spec Ψ fn acc t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] acc ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) acc -∗
        WP fn acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      list٠foldl fn acc t
    {{{
      acc
    , RET acc;
      Ψ (length vs) vs acc
    }}}.
  Lemma list٠foldl𑁒spec' Ψ fn acc t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] acc ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ i (take i vs) acc -∗
        WP fn acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      list٠foldl fn acc t
    {{{
      acc
    , RET acc;
      Ψ (length vs) vs acc
    }}}.

  #[local] Lemma list٠foldri₀𑁒spec vs_left Ψ vs fn i t vs_right acc :
    vs = vs_left ++ vs_right →
    i = length vs_left →
    list_model' t vs_right →
    {{{
      ▷ Ψ (length vs) acc [] ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      list٠foldri₀ fn #i t acc
    {{{
      acc
    , RET acc;
      Ψ i acc vs_right
    }}}.
  Lemma list٠foldri𑁒spec Ψ fn t vs acc :
    list_model' t vs →
    {{{
      ▷ Ψ (length vs) acc [] ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      list٠foldri fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs
    }}}.
  Lemma list٠foldri𑁒spec' Ψ fn t vs acc :
    list_model' t vs →
    {{{
      ▷ Ψ (length vs) acc [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      list٠foldri fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs
    }}}.

  Lemma list٠foldr𑁒spec Ψ fn t vs acc :
    list_model' t vs →
    {{{
      ▷ Ψ (length vs) acc [] ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      list٠foldr fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs
    }}}.
  Lemma list٠foldr𑁒spec' Ψ fn t vs acc :
    list_model' t vs →
    {{{
      ▷ Ψ (length vs) acc [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      list٠foldr fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs
    }}}.

  Lemma list٠size𑁒spec t vs :
    list_model' t vs →
    {{{
      True
    }}}
      list٠size t
    {{{
      RET #(length vs);
      True
    }}}.

  Lemma list٠rev_app𑁒spec t1 vs1 t2 vs2 :
    list_model' t1 vs1 →
    list_model' t2 vs2 →
    {{{
      True
    }}}
      list٠rev_app t1 t2
    {{{
      t
    , RET t;
      list_model t (reverse vs1 ++ vs2)
    }}}.

  Lemma list٠rev𑁒spec t vs :
    list_model' t vs →
    {{{
      True
    }}}
      list٠rev t
    {{{
      t'
    , RET t';
      list_model t' (reverse vs)
    }}}.

  Lemma list٠app𑁒spec t1 vs1 t2 vs2 :
    list_model' t1 vs1 →
    list_model' t2 vs2 →
    {{{
      True
    }}}
      list٠app t1 t2
    {{{
      t
    , RET t;
      list_model t (vs1 ++ vs2)
    }}}.

  Lemma list٠snoc𑁒spec t vs v :
    list_model' t vs →
    {{{
      True
    }}}
      list٠snoc t v
    {{{
      t'
    , RET t';
      list_model t' (vs ++ [v])
    }}}.

  Lemma list٠iteri𑁒spec Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      list٠iteri fn t
    {{{
      RET ();
      Ψ (length vs) vs
    }}}.
  Lemma list٠iteri𑁒spec' Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      list٠iteri fn t
    {{{
      RET ();
      Ψ (length vs) vs
    }}}.
  Lemma list٠iteri𑁒spec_disentangled Ψ fn t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      list٠iteri fn t
    {{{
      RET ();
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma list٠iteri𑁒spec_disentangled' Ψ fn t vs :
    list_model' t vs →
    {{{
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      list٠iteri fn t
    {{{
      RET ();
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma list٠iter𑁒spec Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      list٠iter fn t
    {{{
      RET ();
      Ψ (length vs) vs
    }}}.
  Lemma list٠iter𑁒spec' Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      list٠iter fn t
    {{{
      RET ();
      Ψ (length vs) vs
    }}}.
  Lemma list٠iter𑁒spec_disentangled Ψ fn t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      list٠iter fn t
    {{{
      RET ();
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma list٠iter𑁒spec_disentangled' Ψ fn t vs :
    list_model' t vs →
    {{{
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      list٠iter fn t
    {{{
      RET ();
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  #[local] Lemma list٠mapi₀𑁒spec vs_left ws_left Ψ vs fn i t vs_right :
    vs = vs_left ++ vs_right →
    i = length vs_left →
    i = length ws_left →
    list_model' t vs_right →
    {{{
      ▷ Ψ i vs_left ws_left ∗
      □ (
        ∀ i v ws,
        ⌜vs !! i = Some v ∧ i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      list٠mapi₀ fn #i t
    {{{
      t' ws_right
    , RET t';
      ⌜length vs = (length ws_left + length ws_right)%nat⌝ ∗
      list_model t' ws_right ∗
      Ψ (length vs) vs (ws_left ++ ws_right)
    }}}.
  Lemma list٠mapi𑁒spec Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] [] ∗
      □ (
        ∀ i v ws,
        ⌜vs !! i = Some v ∧ i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      list٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma list٠mapi𑁒spec' Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      list٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma list٠mapi𑁒spec_disentangled Ψ fn t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      list٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.
  Lemma list٠mapi𑁒spec_disentangled' Ψ fn t vs :
    list_model' t vs →
    {{{
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      list٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.

  Lemma list٠map𑁒spec Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] [] ∗
      □ (
        ∀ i v ws,
        ⌜vs !! i = Some v ∧ i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      list٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma list٠map𑁒spec' Ψ fn t vs :
    list_model' t vs →
    {{{
      ▷ Ψ 0 [] [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      list٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma list٠map𑁒spec_disentangled Ψ fn t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      list٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.
  Lemma list٠map𑁒spec_disentangled' Ψ fn t vs :
    list_model' t vs →
    {{{
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      list٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length vs = length ws⌝ ∗
      list_model t' ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.

  Lemma list٠∀𑁒spec Ψ pred t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP pred v {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          Ψ i v b
        }}
      )
    }}}
      list٠∀ pred t
    {{{
      b
    , RET #b;
      if b then
        [∗ list] i ↦ v ∈ vs, Ψ i v true
      else
        ∃ i v,
        ⌜vs !! i = Some v⌝ ∗
        Ψ i v false
    }}}.

  Lemma list٠∃𑁒spec Ψ pred t vs :
    list_model' t vs →
    {{{
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP pred v {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          Ψ i v b
        }}
      )
    }}}
      list٠∃ pred t
    {{{
      b
    , RET #b;
      if b then
        ∃ i v,
        ⌜vs !! i = Some v⌝ ∗
        Ψ i v true
      else
        [∗ list] i ↦ v ∈ vs, Ψ i v false
    }}}.
End zoo_G.

From zoo_std Require
  list__opaque.