Library zoo_std.list

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.list__code.
Require Import zoo_std.list__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type i j : nat.
Implicit Type v w t fn acc pred : val.
Implicit Type 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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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⌝ -∗
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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⌝ -∗
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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,
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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⌝ -∗
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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,
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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.

Require zoo_std.list__opaque.