Library zoo.program_logic.for_

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo.options.

Implicit Type δ : nat.
Implicit Type 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 ˖δ
        }}
      )
    }}}
      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 ˖δ
        }}
      )
    }}}
      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 ˖δ
        }}
      )
    }}}
      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 ˖δ
        }}
      )
    }}}
      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 ˖δ
        }}
      )
    }}}
      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⌝ ∗
          ▷ Ψ ˖i ˖δ
        }}
      )
    }}}
      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⌝ ∗
          ▷ Ψ ˖i ˖δ
        }}
      )
    }}}
      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⌝ ∗
          ▷ Ψ ˖i ˖δ
        }}
      )
    }}}
      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⌝ ∗
          ▷ Ψ ˖i ˖δ
        }}
      )
    }}}
      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 (𝗳𝘂𝗻 x → body)
    }}}
      𝗳𝗼𝗿 x = #beg 𝘁𝗼 #_end 𝗱𝗼 body 𝗱𝗼𝗻𝗲
    {{{
      RET ();
      True
    }}}.
End zoo۰G.