Library examples.pool_quicksort

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Export examples.pool_quicksort__code.
Require Import examples.pool_quicksort__types.
Require Import zoo.options.

Section pool ۰ G.
  Context `{pool ۰ G : PoolG}.

  #[local] Lemma pool_quicksort ٠ partition ｰ spec arr i i_ xs sz :
    (0 ≤ i)%Z →
    i_ = ₊i →
    (1 < sz)%Z →
    length xs = ₊sz →
    {{{
      array ۰ slice arr i_ (DfracOwn 1) (#*@{Z } xs)
    }}}
      pool_quicksort ٠ partition arr #i #sz
    {{{
      xs1 p pivot xs2
    , RET #p ;
      ⌜p = (i_ + length xs1)%nat⌝ ∗
      ⌜xs ≡ₚ xs1 ++ pivot :: xs2 ⌝ ∗
      ⌜Forall ((≥)%Z pivot) xs1 ⌝ ∗
      ⌜Forall ((≤)%Z pivot) xs2 ⌝ ∗
      array ۰ slice arr i_ (DfracOwn 1) (#*@{Z } xs1 ++ #@{Z } pivot :: #*@{Z } xs2)
    }}}.
  #[local] Lemma pool_quicksort ٠ main₂ ｰ spec pool ctx scope arr i i_ xs sz :
    (0 ≤ i)%Z →
    i_ = ₊i →
    length xs = ₊sz →
    {{{
      pool ۰ context pool ctx scope ∗
      array ۰ slice arr i_ (DfracOwn 1) (#*@{Z } xs)
    }}}
      pool_quicksort ٠ main₂ ctx arr #i #sz
    {{{
      RET ();
      pool ۰ context pool ctx scope ∗
      pool ۰ consumer pool (
        ∃ xs',
        ⌜xs ≡ₚ xs'⌝ ∗
        ⌜StronglySorted (≤)%Z xs'⌝ ∗
        array ۰ slice arr i_ (DfracOwn 1) (#*@{Z } xs')
      )
    }}}.
  #[local] Lemma pool_quicksort ٠ main₁ ｰ spec pool ctx scope arr xs :
    {{{
      pool ۰ context pool ctx scope ∗
      array ۰ model arr (DfracOwn 1) (#*@{Z } xs)
    }}}
      pool_quicksort ٠ main₁ ctx arr
    {{{
      RET ();
      pool ۰ context pool ctx scope ∗
      pool ۰ consumer pool (
        ∃ xs',
        ⌜xs ≡ₚ xs'⌝ ∗
        ⌜StronglySorted (≤)%Z xs'⌝ ∗
        array ۰ model arr (DfracOwn 1) (#*@{Z } xs')
      )
    }}}.

  Lemma pool_quicksort ٠ main ｰ spec (num_dom : nat) arr xs :
    {{{
      array ۰ model arr (DfracOwn 1) (#*@{Z } xs)
    }}}
      pool_quicksort ٠ main #num_dom arr
    {{{
      xs'
    , RET ();
      ⌜xs ≡ₚ xs'⌝ ∗
      ⌜StronglySorted (≤)%Z xs'⌝ ∗
      array ۰ model arr (DfracOwn 1) (#*@{Z } xs')
    }}}.
End pool ۰ G.

Require examples.pool_quicksort__opaque.