Library zoo_std.for_

From zoo Require Import
  prelude.
From zoo.iris.bi Require Import
  big_op.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base.
From zoo Require Import
  options.

Implicit Types δ : nat.
Implicit Types body : expr.

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

  #[local] Lemma for𑁒spec_stronger beg i δ Ψ _end body :
    i = (beg + δ)%Z →
    {{{
      ▷ Ψ i δ ∗
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%Z⌝ -∗
        ⌜i < _end⌝%Z -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (i + 1)%Z (S δ)
        }}
      )
    }}}
      For #i #_end body
    {{{
      RET ();
      Ψ (i `max` _end)%Z (δ + ₊(_end - i))
    }}}.
  Lemma for𑁒spec_strong Ψ beg _end body :
    {{{
      ▷ Ψ beg 0 ∗
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%Z⌝ -∗
        ⌜i < _end⌝%Z -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (i + 1)%Z (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ (beg `max` _end)%Z ₊(_end - beg)
    }}}.
  Lemma for𑁒spec Ψ beg _end body :
    (beg ≤ _end)%Z →
    {{{
      ▷ Ψ beg 0 ∗
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%Z⌝ -∗
        ⌜i < _end⌝%Z -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (i + 1)%Z (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ _end ₊(_end - beg)
    }}}.
  Lemma for𑁒spec_strong' Ψ beg _end body :
    {{{
      ▷ Ψ beg 0 ∗
      ( [∗ list] δ ∈ seq 0 ₊(_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%Z⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (i + 1)%Z (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ (beg `max` _end)%Z ₊(_end - beg)
    }}}.
  Lemma for𑁒spec' Ψ beg _end body :
    (beg ≤ _end)%Z →
    {{{
      ▷ Ψ beg 0 ∗
      ( [∗ list] δ ∈ seq 0 ₊(_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%Z⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (i + 1)%Z (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ _end ₊(_end - beg)
    }}}.
  Lemma for𑁒spec_disentangled Ψ beg _end body :
    {{{
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%Z⌝ -∗
        ⌜i < _end⌝%Z -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i δ
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      ( [∗ list] δ ∈ seq 0 ₊(_end - beg),
        Ψ (beg + δ)%Z δ
      )
    }}}.
  Lemma for𑁒spec_disentangled' Ψ beg _end body :
    {{{
      ( [∗ list] δ ∈ seq 0 ₊(_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%Z⌝ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i δ
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      ( [∗ list] δ ∈ seq 0 ₊(_end - beg),
        Ψ (beg + δ)%Z δ
      )
    }}}.

  Lemma for𑁒spec_nat_strong Ψ beg _end body :
    {{{
      ▷ Ψ beg 0 ∗
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%nat⌝ -∗
        ⌜i < _end⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ (beg `max` _end) (_end - beg)
    }}}.
  Lemma for𑁒spec_nat Ψ beg _end body :
    beg ≤ _end →
    {{{
      ▷ Ψ beg 0 ∗
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%nat⌝ -∗
        ⌜i < _end⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ _end (_end - beg)
    }}}.
  Lemma for𑁒spec_nat_strong' Ψ beg _end body :
    {{{
      ▷ Ψ beg 0 ∗
      ( [∗ list] δ ∈ seq 0 (_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%nat⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ (beg `max` _end) (_end - beg)
    }}}.
  Lemma for𑁒spec_nat' Ψ beg _end body :
    beg ≤ _end →
    {{{
      ▷ Ψ beg 0 ∗
      ( [∗ list] δ ∈ seq 0 (_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%nat⌝ -∗
        Ψ i δ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (S δ)
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      Ψ _end (_end - beg)
    }}}.
  Lemma for𑁒spec_disentangled_nat Ψ beg _end body :
    {{{
      □ (
        ∀ i δ,
        ⌜i = (beg + δ)%nat⌝ -∗
        ⌜i < _end⌝ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i δ
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      ( [∗ list] δ ∈ seq 0 (_end - beg),
        Ψ (beg + δ) δ
      )
    }}}.
  Lemma for𑁒spec_disentangled_nat' Ψ beg _end body :
    {{{
      ( [∗ list] δ ∈ seq 0 (_end - beg),
        ∀ i,
        ⌜i = (beg + δ)%nat⌝ -∗
        WP body #i {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i δ
        }}
      )
    }}}
      For #beg #_end body
    {{{
      RET ();
      ( [∗ list] δ ∈ seq 0 (_end - beg),
        Ψ (beg + δ) δ
      )
    }}}.

  Lemma for𑁒type τ `{!iType (iProp Σ) τ} x beg _end body :
    {{{
      (itype_int_range beg _end --> itype_unit)%T (fun: x ⇒ body)
    }}}
      for: x := #beg to #_end begin body end
    {{{
      RET ();
      True
    }}}.
End zoo_G.