6. Programming Language🔗

Definition6.1

Group: Hehner's Chapter 5: the programming notations of "several languages" — control structures, scope, data structures, subprograms — explained as refinement notations or as specifications in the theory of Chapter 4. The while-loop of Section 5.2.0 is formalized in LaPToP.ProgramTheory.WhileLoop the for-loop of Section 5.2.3 in LaPToP.ProgramTheory.ForLoop , and variable declaration and suspension (Section 5.0) in LaPToP.ProgramTheory.Scope , assertions and backtracking (Section 5.4) in LaPToP.ProgramTheory.Assertions . (10)

Group member previews

Preview

Theorem 6.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 5.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Theorem 6.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"The while-loop of several languages has a syntax similar to \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od}. ... We do not define the while-loop as a specification the way we have defined previous programming notations. Instead, if W is an implementable specification, we consider the refinement W \Leftarrow \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od} to be an alternative notation for the refinement W \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ P.\ W\ \mathbf{else}\ \mathit{ok}." Accordingly Spec.WhileRefines W b P is defined as that refinement — a refinement notation, not a specification. By Refinement by Cases it is W \Leftarrow b \land (P.\ W) together with W \Leftarrow \neg b \land \mathit{ok}; the body may be refined in place; and a loop whose condition never holds is \mathit{ok}. The least-fixed-point account of loops and the reference-section law \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od} = t' \ge t \land \mathbf{if}\ b\ \mathbf{then}\ P.\ t := t+1.\ \mathbf{while} \ldots\ \mathbf{else}\ \mathit{ok} belong to Section 6.1.1 and are not formalized here. Uses Definition 5.2 and Theorem 5.12.

Lean code for Definition6.1●5 declarations

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.Spec.WhileRefines.{u} {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) : Prop

def LaPToP.ProgramTheory.Spec.WhileRefines.{u}
  {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) : Prop

`W ⇐ while b do P od`, "an alternative notation for the refinement
`W ⇐ if b then P. W else ok`".

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.whileRefines_iff.{u} {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  W.WhileRefines b P ↔
    W.Refines
      (LaPToP.ProgramTheory.Spec.cond b (P.seq W)
        LaPToP.ProgramTheory.Spec.ok)

theorem LaPToP.ProgramTheory.Spec.whileRefines_iff.{u}
  {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  W.WhileRefines b P ↔
    W.Refines
      (LaPToP.ProgramTheory.Spec.cond b
        (P.seq W)
        LaPToP.ProgramTheory.Spec.ok)

The definition, unfolded.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.whileRefines_iff_cases.{u} {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  W.WhileRefines b P ↔
    W.Refines
        (LaPToP.ProgramTheory.Spec.and (fun s x => b s) (P.seq W)) ∧
      W.Refines
        (LaPToP.ProgramTheory.Spec.and (fun s x => ¬b s)
          LaPToP.ProgramTheory.Spec.ok)

theorem LaPToP.ProgramTheory.Spec.whileRefines_iff_cases.{u}
  {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  W.WhileRefines b P ↔
    W.Refines
        (LaPToP.ProgramTheory.Spec.and
          (fun s x => b s) (P.seq W)) ∧
      W.Refines
        (LaPToP.ProgramTheory.Spec.and
          (fun s x => ¬b s)
          LaPToP.ProgramTheory.Spec.ok)

By Refinement by Cases: `W ⇐ while b do P od` iff `W ⇐ b ∧ (P. W)` and `W ⇐ ¬b ∧ ok`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.WhileRefines.mono.{u} {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (P P' : LaPToP.ProgramTheory.Spec σ) (h : W.WhileRefines b P')
  (hP : P'.Refines P) : W.WhileRefines b P

theorem LaPToP.ProgramTheory.Spec.WhileRefines.mono.{u}
  {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (P P' : LaPToP.ProgramTheory.Spec σ)
  (h : W.WhileRefines b P')
  (hP : P'.Refines P) : W.WhileRefines b P

The body of a while-loop may be refined in place (Refinement by Steps).

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.whileRefines_false.{u} {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) (hb : ∀ (s : σ), ¬b s) :
  W.WhileRefines b P ↔ W.Refines LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.whileRefines_false.{u}
  {σ : Type u}
  (W : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ)
  (hb : ∀ (s : σ), ¬b s) :
  W.WhileRefines b P ↔
    W.Refines LaPToP.ProgramTheory.Spec.ok

A while-loop whose condition never holds is `ok`: `W ⇐ while ⊥ do P od` iff `W ⇐ ok`.

Theorem6.2

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Theorem 5.8

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsprogramsloopshehner-5.2.0

The book's example: "to prove s' = s + \Sigma L[n;..\# L] \land t' = t + \# L - n \Leftarrow \mathbf{while}\ n \neq \# L\ \mathbf{do}\ s := s + L\,n.\ n := n+1.\ t := t+1\ \mathbf{od} prove instead \ldots \Leftarrow \mathbf{if}\ n \neq \# L\ \mathbf{then}\ s := s + L\,n.\ n := n+1.\ t := t+1.\ (s' = s + \Sigma L[n;..\# L] \land t' = t + \# L - n)\ \mathbf{else}\ \mathit{ok}." The state carries the time t, the sum s and the index n, with the bound 0 \le n \le \# L explicit as in Theorem 5.13. Uses Definition 6.1, Definition 5.14 and Theorem 5.8.

Lean code for Theorem6.2●10 declarations

structure(3 fields)defined in LaPToP/ProgramTheory/WhileLoop.lean

complete

structure LaPToP.ProgramTheory.TimedListSummation.TLS : Type

structure LaPToP.ProgramTheory.TimedListSummation.TLS :
  Type

A state with time `t`, the sum `s` and the index `n`.

Fields

t : ℕ∞

The time variable.

s : ℤ

The accumulator `s`.

n : ℤ

The index `n`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.TimedListSummation.assignS
  (e : LaPToP.ProgramTheory.TimedListSummation.TLS → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.TimedListSummation.TLS

def LaPToP.ProgramTheory.TimedListSummation.assignS
  (e :
    LaPToP.ProgramTheory.TimedListSummation.TLS →
      ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.TimedListSummation.TLS

`s:= e`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.TimedListSummation.assignN
  (e : LaPToP.ProgramTheory.TimedListSummation.TLS → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.TimedListSummation.TLS

def LaPToP.ProgramTheory.TimedListSummation.assignN
  (e :
    LaPToP.ProgramTheory.TimedListSummation.TLS →
      ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.TimedListSummation.TLS

`n:= e`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.TimedListSummation.tick :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.TimedListSummation.TLS

def LaPToP.ProgramTheory.TimedListSummation.tick :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.TimedListSummation.TLS

`t:= t+1`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.TimedListSummation.assignS_seq
  (e : LaPToP.ProgramTheory.TimedListSummation.TLS → ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  (LaPToP.ProgramTheory.TimedListSummation.assignS e).seq P =
    fun st st' => P { t := st.t, s := e st, n := st.n } st'

theorem LaPToP.ProgramTheory.TimedListSummation.assignS_seq
  (e :
    LaPToP.ProgramTheory.TimedListSummation.TLS →
      ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  (LaPToP.ProgramTheory.TimedListSummation.assignS
          e).seq
      P =
    fun st st' =>
    P { t := st.t, s := e st, n := st.n }
      st'

Substitution Law for `s:= e`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.TimedListSummation.assignN_seq
  (e : LaPToP.ProgramTheory.TimedListSummation.TLS → ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  (LaPToP.ProgramTheory.TimedListSummation.assignN e).seq P =
    fun st st' => P { t := st.t, s := st.s, n := e st } st'

theorem LaPToP.ProgramTheory.TimedListSummation.assignN_seq
  (e :
    LaPToP.ProgramTheory.TimedListSummation.TLS →
      ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  (LaPToP.ProgramTheory.TimedListSummation.assignN
          e).seq
      P =
    fun st st' =>
    P { t := st.t, s := st.s, n := e st }
      st'

Substitution Law for `n:= e`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.TimedListSummation.tick_seq
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  LaPToP.ProgramTheory.TimedListSummation.tick.seq P = fun st st' =>
    P { t := st.t + 1, s := st.s, n := st.n } st'

theorem LaPToP.ProgramTheory.TimedListSummation.tick_seq
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.TimedListSummation.TLS) :
  LaPToP.ProgramTheory.TimedListSummation.tick.seq
      P =
    fun st st' =>
    P
      { t := st.t + 1, s := st.s,
        n := st.n }
      st'

Substitution Law for `t:= t+1`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.TimedListSummation.Bt
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.TimedListSummation.TLS

def LaPToP.ProgramTheory.TimedListSummation.Bt
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.TimedListSummation.TLS

`s′ = s + Σ L [n;..#L] ∧ t′ = t + #L – n` (with the bound `0 ≤ n ≤ #L`
explicit, as in `ListSummation.B`).

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.TimedListSummation.cast_sub_succ_add_one {m n : ℤ}
  (h : n < m) : ↑(m - (n + 1)).toNat + 1 = ↑(m - n).toNat

theorem LaPToP.ProgramTheory.TimedListSummation.cast_sub_succ_add_one
  {m n : ℤ} (h : n < m) :
  ↑(m - (n + 1)).toNat + 1 =
    ↑(m - n).toNat

`(#L – (n+1)) + 1 = #L – n` for `n < #L`, in `ℕ∞`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.TimedListSummation.whileRefines_Bt
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.TimedListSummation.Bt L).WhileRefines
    (fun st => st.n ≠ LaPToP.ProgramTheory.ListSummation.len L)
    ((LaPToP.ProgramTheory.TimedListSummation.assignS fun st =>
          st.s + L.at st.n.toNat).seq
      ((LaPToP.ProgramTheory.TimedListSummation.assignN fun st =>
            st.n + 1).seq
        LaPToP.ProgramTheory.TimedListSummation.tick))

theorem LaPToP.ProgramTheory.TimedListSummation.whileRefines_Bt
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.TimedListSummation.Bt
        L).WhileRefines
    (fun st =>
      st.n ≠
        LaPToP.ProgramTheory.ListSummation.len
          L)
    ((LaPToP.ProgramTheory.TimedListSummation.assignS
          fun st =>
          st.s + L.at st.n.toNat).seq
      ((LaPToP.ProgramTheory.TimedListSummation.assignN
            fun st => st.n + 1).seq
        LaPToP.ProgramTheory.TimedListSummation.tick))

`s′ = s + Σ L [n;..#L] ∧ t′ = t + #L – n ⇐ while n⧧#L do s:= s + L n. n:= n+1. t:= t+1 od`,
the book's example, proved as `… ⇐ if n⧧#L then s:= s + L n. n:= n+1. t:= t+1. (…) else ok`.

Proof for Theorem 6.2

uses 0

Three applications of the Substitution Law, then \Sigma L[n;..\# L] = L\,n + \Sigma L[n+1;..\# L] and (\# L - (n+1)) + 1 = \# L - n for n < \# L; the exit case is \Sigma L[\# L;..\# L] = 0.

Theorem6.3

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Definition 3.8

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortmediumTagsprogramsloopstimehehner-5.2.0

Exercise 320 (unbounded bound): in natural variables x, y, \mathbf{while}\ \neg(x = y = 0)\ \mathbf{do}\ \mathbf{if}\ y > 0\ \mathbf{then}\ y := y - 1\ \mathbf{else}\ x := x - 1.\ \mathbf{new}\ n : \mathit{nat} \cdot y := n\ \mathbf{od} "decreases y until it is 0; then it decreases x by 1 and assigns an arbitrary natural number to y; ... and so on until both x and y are 0. The problem is to find a time bound." Following the book, the arbitrary values are the values of an arbitrary function f : \mathit{nat} \to \mathit{nat} of x, and with s = \Sigma f[0;..x] the refinement t' = t + x + y + s \Leftarrow \mathbf{if}\ x = y = 0\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ \mathbf{if}\ y > 0\ \mathbf{then}\ y := y-1.\ t := t+1.\ t' = t+x+y+s\ \mathbf{else}\ x := x-1.\ y := f\,x.\ t := t+1.\ t' = t+x+y+s is proved "in three cases", and restated in while-loop notation: "the execution time of the program is x + y + (\text{the sum of } x \text{ arbitrary natural numbers})". Uses Definition 6.1, Definition 5.14, Theorem 5.8 and Definition 3.8.

Lean code for Theorem6.3●13 declarations

structure(3 fields)defined in LaPToP/ProgramTheory/WhileLoop.lean

complete

structure LaPToP.ProgramTheory.UnboundedBound.XY : Type

structure LaPToP.ProgramTheory.UnboundedBound.XY :
  Type

A state with time `t` and natural variables `x`, `y`.

Fields

t : ℕ∞

The time variable.

x : ℕ

The natural variable `x`.

y : ℕ

The natural variable `y`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.assignX
  (e : LaPToP.ProgramTheory.UnboundedBound.XY → ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY

def LaPToP.ProgramTheory.UnboundedBound.assignX
  (e :
    LaPToP.ProgramTheory.UnboundedBound.XY →
      ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.UnboundedBound.XY

`x:= e`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.assignY
  (e : LaPToP.ProgramTheory.UnboundedBound.XY → ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY

def LaPToP.ProgramTheory.UnboundedBound.assignY
  (e :
    LaPToP.ProgramTheory.UnboundedBound.XY →
      ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.UnboundedBound.XY

`y:= e`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.tick :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY

def LaPToP.ProgramTheory.UnboundedBound.tick :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.UnboundedBound.XY

`t:= t+1`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.assignX_seq
  (e : LaPToP.ProgramTheory.UnboundedBound.XY → ℕ)
  (P :
    LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY) :
  (LaPToP.ProgramTheory.UnboundedBound.assignX e).seq P = fun st st' =>
    P { t := st.t, x := e st, y := st.y } st'

theorem LaPToP.ProgramTheory.UnboundedBound.assignX_seq
  (e :
    LaPToP.ProgramTheory.UnboundedBound.XY →
      ℕ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.UnboundedBound.XY) :
  (LaPToP.ProgramTheory.UnboundedBound.assignX
          e).seq
      P =
    fun st st' =>
    P { t := st.t, x := e st, y := st.y }
      st'

Substitution Law for `x:= e`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.assignY_seq
  (e : LaPToP.ProgramTheory.UnboundedBound.XY → ℕ)
  (P :
    LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY) :
  (LaPToP.ProgramTheory.UnboundedBound.assignY e).seq P = fun st st' =>
    P { t := st.t, x := st.x, y := e st } st'

theorem LaPToP.ProgramTheory.UnboundedBound.assignY_seq
  (e :
    LaPToP.ProgramTheory.UnboundedBound.XY →
      ℕ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.UnboundedBound.XY) :
  (LaPToP.ProgramTheory.UnboundedBound.assignY
          e).seq
      P =
    fun st st' =>
    P { t := st.t, x := st.x, y := e st }
      st'

Substitution Law for `y:= e`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.tick_seq
  (P :
    LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY) :
  LaPToP.ProgramTheory.UnboundedBound.tick.seq P = fun st st' =>
    P { t := st.t + 1, x := st.x, y := st.y } st'

theorem LaPToP.ProgramTheory.UnboundedBound.tick_seq
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.UnboundedBound.XY) :
  LaPToP.ProgramTheory.UnboundedBound.tick.seq
      P =
    fun st st' =>
    P
      { t := st.t + 1, x := st.x,
        y := st.y }
      st'

Substitution Law for `t:= t+1`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.sumF (f : ℕ → ℕ) (x : ℕ) : ℕ

def LaPToP.ProgramTheory.UnboundedBound.sumF
  (f : ℕ → ℕ) (x : ℕ) : ℕ

`Σ f [0;..x]`, "the sum of the first `x` values of `f`".

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.sumF_succ (f : ℕ → ℕ) (x : ℕ) :
  LaPToP.ProgramTheory.UnboundedBound.sumF f (x + 1) =
    LaPToP.ProgramTheory.UnboundedBound.sumF f x + f x

theorem LaPToP.ProgramTheory.UnboundedBound.sumF_succ
  (f : ℕ → ℕ) (x : ℕ) :
  LaPToP.ProgramTheory.UnboundedBound.sumF
      f (x + 1) =
    LaPToP.ProgramTheory.UnboundedBound.sumF
        f x +
      f x

`Σ f [0;..x+1] = Σ f [0;..x] + f x`.

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.E (f : ℕ → ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY

def LaPToP.ProgramTheory.UnboundedBound.E
  (f : ℕ → ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.UnboundedBound.XY

`t′ = t + x + y + s` where `s = Σ f [0;..x]`: the execution time is
"`x + y + (the sum of x arbitrary natural numbers)`".

defdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

def LaPToP.ProgramTheory.UnboundedBound.body (f : ℕ → ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.UnboundedBound.XY

def LaPToP.ProgramTheory.UnboundedBound.body
  (f : ℕ → ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.UnboundedBound.XY

The loop body: `if y>0 then y:= y–1. t:= t+1 else x:= x–1. y:= f x. t:= t+1`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.refine_E (f : ℕ → ℕ) :
  (LaPToP.ProgramTheory.UnboundedBound.E f).Refines
    (LaPToP.ProgramTheory.Spec.cond (fun st => st.x = 0 ∧ st.y = 0)
      LaPToP.ProgramTheory.Spec.ok
      (LaPToP.ProgramTheory.Spec.cond (fun st => 0 < st.y)
        ((LaPToP.ProgramTheory.UnboundedBound.assignY fun st =>
              st.y - 1).seq
          (LaPToP.ProgramTheory.UnboundedBound.tick.seq
            (LaPToP.ProgramTheory.UnboundedBound.E f)))
        ((LaPToP.ProgramTheory.UnboundedBound.assignX fun st =>
              st.x - 1).seq
          ((LaPToP.ProgramTheory.UnboundedBound.assignY fun st =>
                f st.x).seq
            (LaPToP.ProgramTheory.UnboundedBound.tick.seq
              (LaPToP.ProgramTheory.UnboundedBound.E f))))))

theorem LaPToP.ProgramTheory.UnboundedBound.refine_E
  (f : ℕ → ℕ) :
  (LaPToP.ProgramTheory.UnboundedBound.E
        f).Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun st => st.x = 0 ∧ st.y = 0)
      LaPToP.ProgramTheory.Spec.ok
      (LaPToP.ProgramTheory.Spec.cond
        (fun st => 0 < st.y)
        ((LaPToP.ProgramTheory.UnboundedBound.assignY
              fun st => st.y - 1).seq
          (LaPToP.ProgramTheory.UnboundedBound.tick.seq
            (LaPToP.ProgramTheory.UnboundedBound.E
              f)))
        ((LaPToP.ProgramTheory.UnboundedBound.assignX
              fun st => st.x - 1).seq
          ((LaPToP.ProgramTheory.UnboundedBound.assignY
                fun st => f st.x).seq
            (LaPToP.ProgramTheory.UnboundedBound.tick.seq
              (LaPToP.ProgramTheory.UnboundedBound.E
                f))))))

The book's refinement, "in three cases":
`t′ = t+x+y+s ⇐ if x=y=0 then ok else if y>0 then y:= y–1. t:= t+1. t′ = t+x+y+s
else x:= x–1. y:= f x. t:= t+1. t′ = t+x+y+s`.

theoremdefined in LaPToP/ProgramTheory/WhileLoop.lean

complete

theorem LaPToP.ProgramTheory.UnboundedBound.whileRefines_E (f : ℕ → ℕ) :
  (LaPToP.ProgramTheory.UnboundedBound.E f).WhileRefines
    (fun st => ¬(st.x = 0 ∧ st.y = 0))
    (LaPToP.ProgramTheory.UnboundedBound.body f)

theorem LaPToP.ProgramTheory.UnboundedBound.whileRefines_E
  (f : ℕ → ℕ) :
  (LaPToP.ProgramTheory.UnboundedBound.E
        f).WhileRefines
    (fun st => ¬(st.x = 0 ∧ st.y = 0))
    (LaPToP.ProgramTheory.UnboundedBound.body
      f)

The same refinement in while-loop notation:
`t′ = t+x+y+s ⇐ while ¬(x=y=0) do if y>0 then y:= y–1. t:= t+1 else x:= x–1. y:= f x. t:= t+1 od`.

Proof for Theorem 6.3

uses 0

Case x = y = 0: \mathit{ok} gives t' = t and s = 0. Case y > 0: the Substitution Law twice, then t + 1 + x + (y-1) + s = t + x + y + s. Case x > 0 \land y = 0: the Substitution Law three times, then t + 1 + (x-1) + f(x-1) + \Sigma f[0;..x-1] = t + x + \Sigma f[0;..x].

Definition6.4

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 5.12

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Theorem 6.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"Let us use the syntax \mathbf{for}\ i := m;..n\ \mathbf{do}\ P\ \mathbf{od} where i is a fresh name called the for-loop index, m and n are integer expressions such that m \le n, and P is a specification ... iteration continues up to but excluding i = n ... i is not a state variable (so it cannot be assigned within P), and the initial values of m and n control the iteration. ... Specification F\,i describes the computation from index i to the end. ... To prove F\,m \Leftarrow \mathbf{for}\ i := m;..n\ \mathbf{do}\ P\ \mathbf{od} prove F\,i \Leftarrow i : m,..n \land (P.\ F(i+1)) and F\,n \Leftarrow \mathit{ok}." As with Definition 6.1, Spec.ForRefines F m n P is defined as these two proof obligations; the index is a parameter of the body and of the indexed specification, and the bounds are natural numbers. The rule has the honest consequence that F\,m is refined by the n - m-fold unrolling P\,m.\ P(m+1).\ \ldots\ P(n-1).\ \mathit{ok}. The invariant special case "A\,m \Rightarrow A'\,n \Leftarrow \mathbf{for}\ i := m;..n\ \mathbf{do}\ i : m,..n \land A\,i \Rightarrow A'(i+1)\ \mathbf{od}", for which "there is nothing to prove", is proved once and for all. Uses Theorem 5.12.

Lean code for Definition6.4●8 declarations

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.Spec.ForRefines.{u} {σ : Type u}
  (F : ℕ → LaPToP.ProgramTheory.Spec σ) (m n : ℕ)
  (P : ℕ → LaPToP.ProgramTheory.Spec σ) : Prop

def LaPToP.ProgramTheory.Spec.ForRefines.{u}
  {σ : Type u}
  (F : ℕ → LaPToP.ProgramTheory.Spec σ)
  (m n : ℕ)
  (P : ℕ → LaPToP.ProgramTheory.Spec σ) :
  Prop

`F m ⇐ for i:= m;..n do P od`: "prove `F i ⇐ i: m,..n ∧ (P. F(i+1))` and
`F n ⇐ ok`".

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.ForRefines.step.{u} {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ} {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h : LaPToP.ProgramTheory.Spec.ForRefines F m n P) {i : ℕ}
  (hm : m ≤ i) (hn : i < n) : (F i).Refines ((P i).seq (F (i + 1)))

theorem LaPToP.ProgramTheory.Spec.ForRefines.step.{u}
  {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ}
  {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h :
    LaPToP.ProgramTheory.Spec.ForRefines F
      m n P)
  {i : ℕ} (hm : m ≤ i) (hn : i < n) :
  (F i).Refines ((P i).seq (F (i + 1)))

The iteration obligation: `F i ⇐ i: m,..n ∧ (P. F(i+1))`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.ForRefines.exit.{u} {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ} {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h : LaPToP.ProgramTheory.Spec.ForRefines F m n P) :
  (F n).Refines LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.ForRefines.exit.{u}
  {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ}
  {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h :
    LaPToP.ProgramTheory.Spec.ForRefines F
      m n P) :
  (F n).Refines
    LaPToP.ProgramTheory.Spec.ok

The exit obligation: `F n ⇐ ok`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.forRefines_self.{u} {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ} {m : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ} :
  LaPToP.ProgramTheory.Spec.ForRefines F m m P ↔
    (F m).Refines LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.forRefines_self.{u}
  {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ}
  {m : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ} :
  LaPToP.ProgramTheory.Spec.ForRefines F m
      m P ↔
    (F m).Refines
      LaPToP.ProgramTheory.Spec.ok

A for-loop with no iterations: `F m ⇐ for i:= m;..m do P od` iff `F m ⇐ ok`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.Spec.iterSeq.{u} {σ : Type u}
  (P : ℕ → LaPToP.ProgramTheory.Spec σ) (m : ℕ) :
  ℕ → LaPToP.ProgramTheory.Spec σ → LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.iterSeq.{u}
  {σ : Type u}
  (P : ℕ → LaPToP.ProgramTheory.Spec σ)
  (m : ℕ) :
  ℕ →
    LaPToP.ProgramTheory.Spec σ →
      LaPToP.ProgramTheory.Spec σ

`P m. P (m+1). … . P (m+k–1). W`: `k` iterations of the body from index `m`,
followed by `W`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.iterSeq_mono.{u} {σ : Type u}
  (P : ℕ → LaPToP.ProgramTheory.Spec σ) (m k : ℕ)
  {W W' : LaPToP.ProgramTheory.Spec σ} (h : W.Refines W') :
  (LaPToP.ProgramTheory.Spec.iterSeq P m k W).Refines
    (LaPToP.ProgramTheory.Spec.iterSeq P m k W')

theorem LaPToP.ProgramTheory.Spec.iterSeq_mono.{u}
  {σ : Type u}
  (P : ℕ → LaPToP.ProgramTheory.Spec σ)
  (m k : ℕ)
  {W W' : LaPToP.ProgramTheory.Spec σ}
  (h : W.Refines W') :
  (LaPToP.ProgramTheory.Spec.iterSeq P m k
        W).Refines
    (LaPToP.ProgramTheory.Spec.iterSeq P m
      k W')

Unrolling is monotonic in the continuation.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.ForRefines.unroll.{u} {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ} {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h : LaPToP.ProgramTheory.Spec.ForRefines F m n P) (hmn : m ≤ n) :
  (F m).Refines
    (LaPToP.ProgramTheory.Spec.iterSeq P m (n - m)
      LaPToP.ProgramTheory.Spec.ok)

theorem LaPToP.ProgramTheory.Spec.ForRefines.unroll.{u}
  {σ : Type u}
  {F : ℕ → LaPToP.ProgramTheory.Spec σ}
  {m n : ℕ}
  {P : ℕ → LaPToP.ProgramTheory.Spec σ}
  (h :
    LaPToP.ProgramTheory.Spec.ForRefines F
      m n P)
  (hmn : m ≤ n) :
  (F m).Refines
    (LaPToP.ProgramTheory.Spec.iterSeq P m
      (n - m)
      LaPToP.ProgramTheory.Spec.ok)

The for-loop rule has the expected consequence: `F m` is refined by the
`n – m`-fold unrolling `P m. P (m+1). … . P (n–1). ok`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.Spec.forRefines_invariant.{u} {σ : Type u}
  (A : ℕ → σ → Prop) (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines (fun i s s' => A i s → A n s') m
    n fun i s s' => m ≤ i ∧ i < n ∧ A i s → A (i + 1) s'

theorem LaPToP.ProgramTheory.Spec.forRefines_invariant.{u}
  {σ : Type u} (A : ℕ → σ → Prop)
  (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (fun i s s' => A i s → A n s') m n
    fun i s s' =>
    m ≤ i ∧ i < n ∧ A i s → A (i + 1) s'

The invariant for-loop rule: "sometimes the indexed specification for the
for-loop has the form `A m ⇒ A′ n`, where `A i` is a binary expression in
unprimed variables called an invariant. ... `A m ⇒ A′ n ⇐ for i:= m;..n do
i: m,..n ∧ A i ⇒ A′(i+1) od`", and "there is nothing to prove".

Theorem6.5

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsprogramsloopshehner-5.2.3

Exercise 179: "let x be a natural variable and n be a natural constant. The binary exponentiation problem can be solved by some initialization and then a for-loop: x' = 2^n \Leftarrow x := 1.\ \mathbf{for}\ i := 0;..n\ \mathbf{do}\ x := 2 \times x\ \mathbf{od}. To prove it, we need to find an indexed specification F\,i such that x' = 2^n \Leftarrow x := 1.\ F\,0, F\,i \Leftarrow i : 0,..n \land (x := 2 \times x.\ F(i+1)), F\,n \Leftarrow \mathit{ok}. The specification we want is F\,i = (x' = x \times 2^{n-i}), which says that the final product is the product so far times the remaining factors. The three proofs are easy." Also the unrolled form. Uses Definition 6.4 and Theorem 5.8.

Lean code for Theorem6.5●7 declarations

structure(1 field)defined in LaPToP/ProgramTheory/ForLoop.lean

complete

structure LaPToP.ProgramTheory.BinaryExponentiation.XS : Type

structure LaPToP.ProgramTheory.BinaryExponentiation.XS :
  Type

A state with one natural variable `x`.

Fields

x : ℕ

The natural variable `x`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.BinaryExponentiation.assignX
  (e : LaPToP.ProgramTheory.BinaryExponentiation.XS → ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.BinaryExponentiation.XS

def LaPToP.ProgramTheory.BinaryExponentiation.assignX
  (e :
    LaPToP.ProgramTheory.BinaryExponentiation.XS →
      ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.BinaryExponentiation.XS

`x:= e`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.BinaryExponentiation.assignX_seq
  (e : LaPToP.ProgramTheory.BinaryExponentiation.XS → ℕ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.BinaryExponentiation.XS) :
  (LaPToP.ProgramTheory.BinaryExponentiation.assignX e).seq P =
    fun st st' => P { x := e st } st'

theorem LaPToP.ProgramTheory.BinaryExponentiation.assignX_seq
  (e :
    LaPToP.ProgramTheory.BinaryExponentiation.XS →
      ℕ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.BinaryExponentiation.XS) :
  (LaPToP.ProgramTheory.BinaryExponentiation.assignX
          e).seq
      P =
    fun st st' => P { x := e st } st'

Substitution Law for `x:= e`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.BinaryExponentiation.F (n i : ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.BinaryExponentiation.XS

def LaPToP.ProgramTheory.BinaryExponentiation.F
  (n i : ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.BinaryExponentiation.XS

`F i = (x′ = x × 2^(n–i))`: "the final product is the product so far times
the remaining factors".

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.BinaryExponentiation.forRefines_F (n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.BinaryExponentiation.F n) 0 n fun x =>
    LaPToP.ProgramTheory.BinaryExponentiation.assignX fun st => 2 * st.x

theorem LaPToP.ProgramTheory.BinaryExponentiation.forRefines_F
  (n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.BinaryExponentiation.F
      n)
    0 n fun x =>
    LaPToP.ProgramTheory.BinaryExponentiation.assignX
      fun st => 2 * st.x

`F i ⇐ i: 0,..n ∧ (x:= 2×x. F(i+1))` and `F n ⇐ ok`:
`F 0 ⇐ for i:= 0;..n do x:= 2×x od`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.BinaryExponentiation.refine_pow (n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines (fun x st' => st'.x = 2 ^ n)
    ((LaPToP.ProgramTheory.BinaryExponentiation.assignX fun x => 1).seq
      (LaPToP.ProgramTheory.BinaryExponentiation.F n 0))

theorem LaPToP.ProgramTheory.BinaryExponentiation.refine_pow
  (n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines
    (fun x st' => st'.x = 2 ^ n)
    ((LaPToP.ProgramTheory.BinaryExponentiation.assignX
          fun x => 1).seq
      (LaPToP.ProgramTheory.BinaryExponentiation.F
        n 0))

`x′ = 2^n ⇐ x:= 1. F 0`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.BinaryExponentiation.refine_pow_unrolled (n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines (fun x st' => st'.x = 2 ^ n)
    ((LaPToP.ProgramTheory.BinaryExponentiation.assignX fun x => 1).seq
      (LaPToP.ProgramTheory.Spec.iterSeq
        (fun x =>
          LaPToP.ProgramTheory.BinaryExponentiation.assignX fun st =>
            2 * st.x)
        0 n LaPToP.ProgramTheory.Spec.ok))

theorem LaPToP.ProgramTheory.BinaryExponentiation.refine_pow_unrolled
  (n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines
    (fun x st' => st'.x = 2 ^ n)
    ((LaPToP.ProgramTheory.BinaryExponentiation.assignX
          fun x => 1).seq
      (LaPToP.ProgramTheory.Spec.iterSeq
        (fun x =>
          LaPToP.ProgramTheory.BinaryExponentiation.assignX
            fun st => 2 * st.x)
        0 n LaPToP.ProgramTheory.Spec.ok))

`x′ = 2^n ⇐ x:= 1. for i:= 0;..n do x:= 2×x od`, with the loop unrolled.

Theorem6.6

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 3.8

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsprogramsloopstimehehner-5.2.3

"The time taken by the body of a for-loop may be a function f of the iteration i. To prove t' = t + \Sigma i : m,..n \cdot f\,i \Leftarrow \mathbf{for}\ i := m;..n\ \mathbf{do}\ t' = t + f\,i\ \mathbf{od} define F\,i = (t' = t + \Sigma j : i,..n \cdot f\,j) and prove t' = t + \Sigma i : m,..n \cdot f\,i \Leftarrow F\,m, F\,i \Leftarrow i : m,..n \land (t' = t + f\,i.\ F(i+1)), F\,n \Leftarrow \mathit{ok}, all of which are easy. When the body takes constant time c, this simplifies to t' = t + (n-m) \times c \Leftarrow \mathbf{for}\ i := m;..n\ \mathbf{do}\ t' = t + c\ \mathbf{od}." Uses Definition 6.4, Definition 5.14 and Definition 3.8.

Lean code for Theorem6.6●7 declarations

structure(1 field)defined in LaPToP/ProgramTheory/ForLoop.lean

complete

structure LaPToP.ProgramTheory.ForLoopTiming.TS : Type

structure LaPToP.ProgramTheory.ForLoopTiming.TS :
  Type

A state with only a time variable.

Fields

t : ℕ∞

The time variable.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.ForLoopTiming.addT (c : ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ForLoopTiming.TS

def LaPToP.ProgramTheory.ForLoopTiming.addT
  (c : ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ForLoopTiming.TS

`t:= t + c`, a body taking time `c`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.ForLoopTiming.addT_seq (c : ℕ)
  (P :
    LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ForLoopTiming.TS) :
  (LaPToP.ProgramTheory.ForLoopTiming.addT c).seq P = fun st st' =>
    P { t := st.t + ↑c } st'

theorem LaPToP.ProgramTheory.ForLoopTiming.addT_seq
  (c : ℕ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.ForLoopTiming.TS) :
  (LaPToP.ProgramTheory.ForLoopTiming.addT
          c).seq
      P =
    fun st st' => P { t := st.t + ↑c } st'

Substitution Law for `t:= t + c`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.ForLoopTiming.F (f : ℕ → ℕ) (n i : ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ForLoopTiming.TS

def LaPToP.ProgramTheory.ForLoopTiming.F
  (f : ℕ → ℕ) (n i : ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ForLoopTiming.TS

`F i = (t′ = t + Σj: i,..n· f j)`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.ForLoopTiming.forRefines_F (f : ℕ → ℕ) (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.ForLoopTiming.F f n) m n fun i =>
    LaPToP.ProgramTheory.ForLoopTiming.addT (f i)

theorem LaPToP.ProgramTheory.ForLoopTiming.forRefines_F
  (f : ℕ → ℕ) (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.ForLoopTiming.F
      f n)
    m n fun i =>
    LaPToP.ProgramTheory.ForLoopTiming.addT
      (f i)

`t′ = t + Σi: m,..n· f i ⇐ for i:= m;..n do t′ = t + f i od`: the obligations
`F i ⇐ i: m,..n ∧ (t′ = t + f i. F(i+1))` and `F n ⇐ ok`, "all of which are easy".

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.ForLoopTiming.refine_time (f : ℕ → ℕ) (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines
    (fun st st' => st'.t = st.t + ↑(∑ i ∈ Finset.Ico m n, f i))
    (LaPToP.ProgramTheory.ForLoopTiming.F f n m)

theorem LaPToP.ProgramTheory.ForLoopTiming.refine_time
  (f : ℕ → ℕ) (m n : ℕ) :
  LaPToP.ProgramTheory.Spec.Refines
    (fun st st' =>
      st'.t =
        st.t +
          ↑(∑ i ∈ Finset.Ico m n, f i))
    (LaPToP.ProgramTheory.ForLoopTiming.F
      f n m)

`t′ = t + Σi: m,..n· f i ⇐ F m` (they are equal).

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.ForLoopTiming.forRefines_const (m n c : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (fun i st st' => st'.t = st.t + ↑((n - i) * c)) m n fun x =>
    LaPToP.ProgramTheory.ForLoopTiming.addT c

theorem LaPToP.ProgramTheory.ForLoopTiming.forRefines_const
  (m n c : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (fun i st st' =>
      st'.t = st.t + ↑((n - i) * c))
    m n fun x =>
    LaPToP.ProgramTheory.ForLoopTiming.addT
      c

"When the body takes constant time `c`, this simplifies to
`t′ = t + (n–m)×c ⇐ for i:= m;..n do t′ = t+c od`."

Theorem6.7

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 4.9

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortmediumTagsprogramsloopslistshehner-5.2.3

Exercise 326: "add 1 to each item in a list. The specification S is defined as S = (\# L' = \# L \land \forall n : \square L \cdot L'\,n = L\,n + 1). Now we need a specification F\,i that describes the iterations from i to the end: adding 1 to each item from index i to (not including) \# L: F\,i = (\# L' = \# L \land (\forall n : 0,..i \cdot L'\,n = L\,n) \land (\forall n : i,..\# L \cdot L'\,n = L\,n + 1)). Then S = F\,0. To prove F\,0 \Leftarrow \mathbf{for}\ i := 0;..\# L\ \mathbf{do}\ L := i \to L\,i + 1 \mid L\ \mathbf{od} we must prove two theorems: F\,i \Leftarrow i : 0,..\# L \land (L := i \to L\,i + 1 \mid L.\ F(i+1)) and F(\# L) \Leftarrow \mathit{ok}." The loop bound is the length of the list in the initial state; since the body preserves the length, the specifications carry the antecedent \# L = N for a constant N. The body is the list modification of Definition 4.9. Uses Definition 6.4 and Theorem 5.8.

Lean code for Theorem6.7●10 declarations

structure(1 field)defined in LaPToP/ProgramTheory/ForLoop.lean

complete

structure LaPToP.ProgramTheory.AddOneToEach.LS : Type

structure LaPToP.ProgramTheory.AddOneToEach.LS :
  Type

A state with one list variable `L`.

Fields

L : LaPToP.DataStructures.HList ℤ

The list variable.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.AddOneToEach.assignL
  (e :
    LaPToP.ProgramTheory.AddOneToEach.LS →
      LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.AddOneToEach.LS

def LaPToP.ProgramTheory.AddOneToEach.assignL
  (e :
    LaPToP.ProgramTheory.AddOneToEach.LS →
      LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.AddOneToEach.LS

`L:= e`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.AddOneToEach.assignL_seq
  (e :
    LaPToP.ProgramTheory.AddOneToEach.LS →
      LaPToP.DataStructures.HList ℤ)
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.AddOneToEach.LS) :
  (LaPToP.ProgramTheory.AddOneToEach.assignL e).seq P = fun st st' =>
    P { L := e st } st'

theorem LaPToP.ProgramTheory.AddOneToEach.assignL_seq
  (e :
    LaPToP.ProgramTheory.AddOneToEach.LS →
      LaPToP.DataStructures.HList ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.AddOneToEach.LS) :
  (LaPToP.ProgramTheory.AddOneToEach.assignL
          e).seq
      P =
    fun st st' => P { L := e st } st'

Substitution Law for `L:= e`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.AddOneToEach.S (N : ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.AddOneToEach.LS

def LaPToP.ProgramTheory.AddOneToEach.S
  (N : ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.AddOneToEach.LS

`S = (#L′ = #L ∧ ∀n: ☐L· L′ n = L n + 1)`, for a list of length `N`.

defdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

def LaPToP.ProgramTheory.AddOneToEach.F (N i : ℕ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.AddOneToEach.LS

def LaPToP.ProgramTheory.AddOneToEach.F
  (N i : ℕ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.AddOneToEach.LS

`F i = (#L′ = #L ∧ (∀n: 0,..i· L′ n = L n) ∧ (∀n: i,..#L· L′ n = L n + 1))`:
"adding 1 to each item from index `i` to (not including) `#L`".

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.AddOneToEach.refine_S (N : ℕ) :
  (LaPToP.ProgramTheory.AddOneToEach.S N).Refines
    (LaPToP.ProgramTheory.AddOneToEach.F N 0)

theorem LaPToP.ProgramTheory.AddOneToEach.refine_S
  (N : ℕ) :
  (LaPToP.ProgramTheory.AddOneToEach.S
        N).Refines
    (LaPToP.ProgramTheory.AddOneToEach.F N
      0)

`S = F 0`: `S ⇐ F 0`.

theoremdefined in LaPToP/ProgramTheory/ForLoop.lean

complete

theorem LaPToP.ProgramTheory.AddOneToEach.forRefines_F (N : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.AddOneToEach.F N) 0 N fun i =>
    LaPToP.ProgramTheory.AddOneToEach.assignL fun st =>
      LaPToP.DataStructures.HList.modify i (st.L.at i + 1) st.L

theorem LaPToP.ProgramTheory.AddOneToEach.forRefines_F
  (N : ℕ) :
  LaPToP.ProgramTheory.Spec.ForRefines
    (LaPToP.ProgramTheory.AddOneToEach.F
      N)
    0 N fun i =>
    LaPToP.ProgramTheory.AddOneToEach.assignL
      fun st =>
      LaPToP.DataStructures.HList.modify i
        (st.L.at i + 1) st.L

`F i ⇐ i: 0,..#L ∧ (L:= i→L i+1 | L. F(i+1))` and `F(#L) ⇐ ok`:
`F 0 ⇐ for i:= 0;..#L do L:= i→L i+1 | L od`.

theoremdefined in LaPToP/DataStructures/Lists.lean

complete

theorem LaPToP.DataStructures.HList.length_contents_modify.{u} {α : Type u}
  (L : LaPToP.DataStructures.HList α) (n : ℕ) (i : α) :
  List.length (LaPToP.DataStructures.HList.modify n i L).contents =
    List.length L.contents

theorem LaPToP.DataStructures.HList.length_contents_modify.{u}
  {α : Type u}
  (L : LaPToP.DataStructures.HList α)
  (n : ℕ) (i : α) :
  List.length
      (LaPToP.DataStructures.HList.modify
          n i L).contents =
    List.length L.contents

`#(n→i | L) = #L`: modification preserves length.

theoremdefined in LaPToP/DataStructures/Lists.lean

complete

theorem LaPToP.DataStructures.HList.at_modify_self.{u} {α : Type u}
  [Inhabited α] (L : LaPToP.DataStructures.HList α) {n : ℕ} (i : α)
  (h : n < List.length L.contents) :
  (LaPToP.DataStructures.HList.modify n i L).at n = i

theorem LaPToP.DataStructures.HList.at_modify_self.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α)
  {n : ℕ} (i : α)
  (h : n < List.length L.contents) :
  (LaPToP.DataStructures.HList.modify n i
          L).at
      n =
    i

`(n→i | L) n = i` for `n` an index of `L`.

theoremdefined in LaPToP/DataStructures/Lists.lean

complete

theorem LaPToP.DataStructures.HList.at_modify_ne.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) {n m : ℕ} (i : α) (h : m ≠ n) :
  (LaPToP.DataStructures.HList.modify n i L).at m = L.at m

theorem LaPToP.DataStructures.HList.at_modify_ne.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α)
  {n m : ℕ} (i : α) (h : m ≠ n) :
  (LaPToP.DataStructures.HList.modify n i
          L).at
      m =
    L.at m

`(n→i | L) m = L m` for `m ≠ n`.

Proof for Theorem 6.7

uses 0

The book's calculation: after the Substitution Law, \#(i \to L\,i + 1 \mid L) = \# L; divide the domain 0,..i+1 into 0,..i and i; for n : 0,..i and for n : i+1,..\# L the modified list agrees with L, and at i it is L\,i + 1.

Definition6.8

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 3.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

"We can express a variable declaration together with the specification to which it applies as a binary expression in the initial and final state: \mathbf{new}\ x : T \cdot P = \exists x, x' : T \cdot P. Specification P is an expression in the initial and final values of all nonlocal (already declared) variables plus the newly declared local variable. Specification \mathbf{new}\ x : T \cdot P is an expression in the nonlocal variables only. For a variable declaration to be implementable, its type must be nonempty." In Lean the state inside the scope is the product \sigma \times T of the nonlocal state and the local variable, and Spec.newVar P is literally \exists x, x' : T \cdot P; a nonlocal specification is lifted into the scope leaving the local variable unchanged, and assignments inside the scope are to the local or to a nonlocal variable. Proved: implementability for nonempty T (and unimplementability for empty T), that declaring an unused variable changes nothing, the initializing declaration \mathbf{new}\ x : T := e \cdot P = \exists x : e \cdot \exists x' : T \cdot P as a declaration followed by a local assignment, nesting \mathbf{new}\ x, y : T \cdot P = \exists x, x', y, y' : T \cdot P, monotonicity, and the book's examples in nonlocal integer variables y, z: \mathbf{new}\ x : \mathit{int} \cdot x := 2.\ y := x + z = (y' = 2 + z \land z' = z), \mathbf{new}\ x : \mathit{int} \cdot y := x = (z' = z) ("the initial value of the local variable is an arbitrary value of its type"), and \mathbf{new}\ x : \mathit{int} \cdot y := x - x = (y' = 0 \land z' = z). Uses Definition 5.2, Definition 3.5 and Theorem 5.8.

Lean code for Definition6.8●18 declarations

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.newVar.{u, v} {σ : Type u} {T : Type v}
  (P : LaPToP.ProgramTheory.Spec (σ × T)) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.newVar.{u, v}
  {σ : Type u} {T : Type v}
  (P :
    LaPToP.ProgramTheory.Spec (σ × T)) :
  LaPToP.ProgramTheory.Spec σ

`new x: T· P = ∃x, x′: T· P`: the specification `P` in the nonlocal state
`σ` together with a local variable `x : T`, with the local variable's initial
and final values existentially quantified.

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.newVarInit.{u, v} {σ : Type u} {T : Type v}
  (e : σ → T) (P : LaPToP.ProgramTheory.Spec (σ × T)) :
  LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.newVarInit.{u,
    v}
  {σ : Type u} {T : Type v} (e : σ → T)
  (P :
    LaPToP.ProgramTheory.Spec (σ × T)) :
  LaPToP.ProgramTheory.Spec σ

`new x: T := e· P = ∃x: e· ∃x′: T· P`, an initializing declaration.

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.assignLocal.{u, v} {σ : Type u} {T : Type v}
  (e : σ × T → T) : LaPToP.ProgramTheory.Spec (σ × T)

def LaPToP.ProgramTheory.Spec.assignLocal.{u,
    v}
  {σ : Type u} {T : Type v}
  (e : σ × T → T) :
  LaPToP.ProgramTheory.Spec (σ × T)

`x:= e` for the local variable `x`, `e` an expression of the whole initial state.

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.liftNonlocal.{u, v} {σ : Type u} {T : Type v}
  (Q : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec (σ × T)

def LaPToP.ProgramTheory.Spec.liftNonlocal.{u,
    v}
  {σ : Type u} {T : Type v}
  (Q : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec (σ × T)

A nonlocal specification `Q` inside the scope of a local variable: `Q`
holds of the nonlocal state and the local variable is unchanged.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.assignLocal_seq.{u, v} {σ : Type u}
  {T : Type v} (e : σ × T → T) (P : LaPToP.ProgramTheory.Spec (σ × T)) :
  (LaPToP.ProgramTheory.Spec.assignLocal e).seq P = fun st st' =>
    P (st.1, e st) st'

theorem LaPToP.ProgramTheory.Spec.assignLocal_seq.{u,
    v}
  {σ : Type u} {T : Type v}
  (e : σ × T → T)
  (P :
    LaPToP.ProgramTheory.Spec (σ × T)) :
  (LaPToP.ProgramTheory.Spec.assignLocal
          e).seq
      P =
    fun st st' => P (st.1, e st) st'

Substitution Law for the local assignment.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_newVar.{u, v} {σ : Type u}
  {T : Type v} [Nonempty T] {P : LaPToP.ProgramTheory.Spec (σ × T)}
  (hP : P.Implementable) : P.newVar.Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_newVar.{u,
    v}
  {σ : Type u} {T : Type v} [Nonempty T]
  {P : LaPToP.ProgramTheory.Spec (σ × T)}
  (hP : P.Implementable) :
  P.newVar.Implementable

"For a variable declaration to be implementable, its type must be
nonempty": `new x: T· P` is implementable when `P` is and `T` is nonempty.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.not_implementable_newVar.{u, v} {σ : Type u}
  {T : Type v} [IsEmpty T] [Nonempty σ]
  (P : LaPToP.ProgramTheory.Spec (σ × T)) : ¬P.newVar.Implementable

theorem LaPToP.ProgramTheory.Spec.not_implementable_newVar.{u,
    v}
  {σ : Type u} {T : Type v} [IsEmpty T]
  [Nonempty σ]
  (P :
    LaPToP.ProgramTheory.Spec (σ × T)) :
  ¬P.newVar.Implementable

With an empty type, no declaration is implementable.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.newVar_liftNonlocal.{u, v} {σ : Type u}
  {T : Type v} [Nonempty T] (Q : LaPToP.ProgramTheory.Spec σ) :
  Q.liftNonlocal.newVar = Q

theorem LaPToP.ProgramTheory.Spec.newVar_liftNonlocal.{u,
    v}
  {σ : Type u} {T : Type v} [Nonempty T]
  (Q : LaPToP.ProgramTheory.Spec σ) :
  Q.liftNonlocal.newVar = Q

Declaring a variable that a specification does not use changes nothing:
`new x: T· Q = Q` for nonlocal `Q` (and nonempty `T`).

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.newVarInit_eq.{u, v} {σ : Type u} {T : Type v}
  [Nonempty T] (e : σ → T) (P : LaPToP.ProgramTheory.Spec (σ × T)) :
  LaPToP.ProgramTheory.Spec.newVarInit e P =
    ((LaPToP.ProgramTheory.Spec.assignLocal fun st => e st.1).seq
        P).newVar

theorem LaPToP.ProgramTheory.Spec.newVarInit_eq.{u,
    v}
  {σ : Type u} {T : Type v} [Nonempty T]
  (e : σ → T)
  (P :
    LaPToP.ProgramTheory.Spec (σ × T)) :
  LaPToP.ProgramTheory.Spec.newVarInit e
      P =
    ((LaPToP.ProgramTheory.Spec.assignLocal
            fun st => e st.1).seq
        P).newVar

An initializing declaration is a declaration followed by a local
assignment: `new x: T := e· P = new x: T· x:= e. P`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.newVar_newVar.{u, v, w} {σ : Type u}
  {T : Type v} {T' : Type w}
  (P : LaPToP.ProgramTheory.Spec ((σ × T) × T')) :
  P.newVar.newVar = fun s s' =>
    ∃ x x' y y', P ((s, x), y) ((s', x'), y')

theorem LaPToP.ProgramTheory.Spec.newVar_newVar.{u,
    v, w}
  {σ : Type u} {T : Type v} {T' : Type w}
  (P :
    LaPToP.ProgramTheory.Spec
      ((σ × T) × T')) :
  P.newVar.newVar = fun s s' =>
    ∃ x x' y y',
      P ((s, x), y) ((s', x'), y')

Declarations nest: `new x, y: T· P = new x: T· new y: T′· P`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.newVar_mono.{u, v} {σ : Type u} {T : Type v}
  {P Q : LaPToP.ProgramTheory.Spec (σ × T)} (h : P.Refines Q) :
  P.newVar.Refines Q.newVar

theorem LaPToP.ProgramTheory.Spec.newVar_mono.{u,
    v}
  {σ : Type u} {T : Type v}
  {P Q :
    LaPToP.ProgramTheory.Spec (σ × T)}
  (h : P.Refines Q) :
  P.newVar.Refines Q.newVar

Declaration is monotonic with respect to refinement.

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.assignNonlocal.{u, v, w} {Var : Type u}
  {Val : Type v} {T : Type w} [DecidableEq Var] (y : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val × T → Val) :
  LaPToP.ProgramTheory.Spec
    (LaPToP.ProgramTheory.Spec.State Var Val × T)

def LaPToP.ProgramTheory.Spec.assignNonlocal.{u,
    v, w}
  {Var : Type u} {Val : Type v}
  {T : Type w} [DecidableEq Var] (y : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
          Val ×
        T →
      Val) :
  LaPToP.ProgramTheory.Spec
    (LaPToP.ProgramTheory.Spec.State Var
        Val ×
      T)

`y:= e` for a nonlocal variable `y` inside the scope of a local variable,
`e` an expression of the whole initial state.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.assignNonlocal_seq.{u, v, w} {Var : Type u}
  {Val : Type v} {T : Type w} [DecidableEq Var] (y : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val × T → Val)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val × T)) :
  (LaPToP.ProgramTheory.Spec.assignNonlocal y e).seq P = fun st st' =>
    P (Function.update st.1 y (e st), st.2) st'

theorem LaPToP.ProgramTheory.Spec.assignNonlocal_seq.{u,
    v, w}
  {Var : Type u} {Val : Type v}
  {T : Type w} [DecidableEq Var] (y : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
          Val ×
        T →
      Val)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
          Val ×
        T)) :
  (LaPToP.ProgramTheory.Spec.assignNonlocal
          y e).seq
      P =
    fun st st' =>
    P
      (Function.update st.1 y (e st),
        st.2)
      st'

Substitution Law for the nonlocal assignment.

inductive(2 constructors)defined in LaPToP/ProgramTheory/Scope.lean

complete

inductive LaPToP.ProgramTheory.ScopeExamples.YZ : Type

inductive LaPToP.ProgramTheory.ScopeExamples.YZ :
  Type

The nonlocal integer variables `y` and `z`.

Constructors

LaPToP.ProgramTheory.ScopeExamples.YZ.y :
  LaPToP.ProgramTheory.ScopeExamples.YZ

The variable `y`.

LaPToP.ProgramTheory.ScopeExamples.YZ.z :
  LaPToP.ProgramTheory.ScopeExamples.YZ

The variable `z`.

abbrevdefined in LaPToP/ProgramTheory/Scope.lean

complete

abbrev LaPToP.ProgramTheory.ScopeExamples.St : Type

abbrev LaPToP.ProgramTheory.ScopeExamples.St :
  Type

Nonlocal states.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.ScopeExamples.example₁ :
  ((LaPToP.ProgramTheory.Spec.assignLocal fun x => 2).seq
        (LaPToP.ProgramTheory.Spec.assignNonlocal
          LaPToP.ProgramTheory.ScopeExamples.YZ.y fun st =>
          st.2 + st.1 LaPToP.ProgramTheory.ScopeExamples.YZ.z)).newVar =
    fun s s' =>
    s' LaPToP.ProgramTheory.ScopeExamples.YZ.y =
        2 + s LaPToP.ProgramTheory.ScopeExamples.YZ.z ∧
      s' LaPToP.ProgramTheory.ScopeExamples.YZ.z =
        s LaPToP.ProgramTheory.ScopeExamples.YZ.z

theorem LaPToP.ProgramTheory.ScopeExamples.example₁ :
  ((LaPToP.ProgramTheory.Spec.assignLocal
            fun x => 2).seq
        (LaPToP.ProgramTheory.Spec.assignNonlocal
          LaPToP.ProgramTheory.ScopeExamples.YZ.y
          fun st =>
          st.2 +
            st.1
              LaPToP.ProgramTheory.ScopeExamples.YZ.z)).newVar =
    fun s s' =>
    s'
          LaPToP.ProgramTheory.ScopeExamples.YZ.y =
        2 +
          s
            LaPToP.ProgramTheory.ScopeExamples.YZ.z ∧
      s'
          LaPToP.ProgramTheory.ScopeExamples.YZ.z =
        s
          LaPToP.ProgramTheory.ScopeExamples.YZ.z

`new x: int· x:= 2. y:= x+z = y′ = 2+z ∧ z′=z`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.ScopeExamples.example₂ :
  (LaPToP.ProgramTheory.Spec.assignNonlocal
        LaPToP.ProgramTheory.ScopeExamples.YZ.y fun st => st.2).newVar =
    fun s s' =>
    s' LaPToP.ProgramTheory.ScopeExamples.YZ.z =
      s LaPToP.ProgramTheory.ScopeExamples.YZ.z

theorem LaPToP.ProgramTheory.ScopeExamples.example₂ :
  (LaPToP.ProgramTheory.Spec.assignNonlocal
        LaPToP.ProgramTheory.ScopeExamples.YZ.y
        fun st => st.2).newVar =
    fun s s' =>
    s'
        LaPToP.ProgramTheory.ScopeExamples.YZ.z =
      s
        LaPToP.ProgramTheory.ScopeExamples.YZ.z

`new x: int· y:= x = z′=z`: "the initial value of the local variable is an
arbitrary value of its type", so nothing is known about `y′`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.ScopeExamples.example₃ :
  (LaPToP.ProgramTheory.Spec.assignNonlocal
        LaPToP.ProgramTheory.ScopeExamples.YZ.y fun st =>
        st.2 - st.2).newVar =
    fun s s' =>
    s' LaPToP.ProgramTheory.ScopeExamples.YZ.y = 0 ∧
      s' LaPToP.ProgramTheory.ScopeExamples.YZ.z =
        s LaPToP.ProgramTheory.ScopeExamples.YZ.z

theorem LaPToP.ProgramTheory.ScopeExamples.example₃ :
  (LaPToP.ProgramTheory.Spec.assignNonlocal
        LaPToP.ProgramTheory.ScopeExamples.YZ.y
        fun st => st.2 - st.2).newVar =
    fun s s' =>
    s'
          LaPToP.ProgramTheory.ScopeExamples.YZ.y =
        0 ∧
      s'
          LaPToP.ProgramTheory.ScopeExamples.YZ.z =
        s
          LaPToP.ProgramTheory.ScopeExamples.YZ.z

`new x: int· y:= x–x = y′=0 ∧ z′=z`.

Definition6.9

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Definition 1.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

"We may wish, temporarily, to narrow our focus to a part of the state space. ... The frame notation is the formal way of saying “and all other variables (even the ones we cannot say because they are covered by local declarations) are unchanged”. If the state variables not included in the frame are w and z, then \mathbf{frame}\ x, y \cdot P = P \land w' = w \land z' = z." On states of Definition 1.7, Spec.frame xs P conjoins P with v' = v for every variable v outside the frame. The book's remark that "if we had defined \mathbf{frame} first, we could have defined \mathit{ok} and assignment formally at the high level" — \mathit{ok} = \mathbf{frame} \cdot \top, x := e = \mathbf{frame}\ x \cdot x' = e — is proved, together with: the full frame is no restriction, \mathbf{frame}\ xs \cdot \mathit{ok} = \mathit{ok}, nested frames intersect, a frame strengthens and is monotonic, a frame distributes over \mathbf{if}, a sequence of framed specifications refines the framed sequence, and a framed variable may be assigned freely. The book's example s := \Sigma L = \mathbf{frame}\ s \cdot \mathbf{new}\ n : \mathit{nat} \cdot s' = \Sigma L ("first we reduce the state space to s; ... next we introduce local variable n") is checked on the state of Theorem 5.13. Uses Definition 6.8 and Definition 5.3.

Lean code for Definition6.9●12 declarations

defdefined in LaPToP/ProgramTheory/Scope.lean

complete

def LaPToP.ProgramTheory.Spec.frame.{u, v} {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)) :
  LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val)

def LaPToP.ProgramTheory.Spec.frame.{u, v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)) :
  LaPToP.ProgramTheory.Spec
    (LaPToP.ProgramTheory.Spec.State Var
      Val)

`frame x, y· P = P ∧ w′=w ∧ z′=z`: `P` holds, and every state variable not
in the frame is unchanged.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_empty_top.{u, v} {Var : Type u}
  {Val : Type v} :
  LaPToP.ProgramTheory.Spec.frame ∅ LaPToP.ProgramTheory.Spec.top =
    LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.frame_empty_top.{u,
    v}
  {Var : Type u} {Val : Type v} :
  LaPToP.ProgramTheory.Spec.frame ∅
      LaPToP.ProgramTheory.Spec.top =
    LaPToP.ProgramTheory.Spec.ok

`ok = frame· ⊤`: the empty frame of the trivial specification.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_singleton_eq.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  (LaPToP.ProgramTheory.Spec.frame {x} fun s s' => s' x = e s) =
    LaPToP.ProgramTheory.Spec.assign x e

theorem LaPToP.ProgramTheory.Spec.frame_singleton_eq.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  (LaPToP.ProgramTheory.Spec.frame {x}
      fun s s' => s' x = e s) =
    LaPToP.ProgramTheory.Spec.assign x e

`x:= e = frame x· x′=e`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_univ.{u, v} {Var : Type u}
  {Val : Type v}
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)) :
  LaPToP.ProgramTheory.Spec.frame Set.univ P = P

theorem LaPToP.ProgramTheory.Spec.frame_univ.{u,
    v}
  {Var : Type u} {Val : Type v}
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)) :
  LaPToP.ProgramTheory.Spec.frame Set.univ
      P =
    P

`frame (all variables)· P = P`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_ok.{u, v} {Var : Type u} {Val : Type v}
  (xs : Set Var) :
  LaPToP.ProgramTheory.Spec.frame xs LaPToP.ProgramTheory.Spec.ok =
    LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.frame_ok.{u, v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var) :
  LaPToP.ProgramTheory.Spec.frame xs
      LaPToP.ProgramTheory.Spec.ok =
    LaPToP.ProgramTheory.Spec.ok

`frame xs· ok = ok`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_frame.{u, v} {Var : Type u}
  {Val : Type v} (xs ys : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.frame ys P) =
    LaPToP.ProgramTheory.Spec.frame (xs ∩ ys) P

theorem LaPToP.ProgramTheory.Spec.frame_frame.{u,
    v}
  {Var : Type u} {Val : Type v}
  (xs ys : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.frame ys
        P) =
    LaPToP.ProgramTheory.Spec.frame
      (xs ∩ ys) P

Nested frames intersect: `frame xs· frame ys· P = frame (xs ‘ ys)· P`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_frame.{u, v} {Var : Type u}
  {Val : Type v} (xs : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)) :
  P.Refines (LaPToP.ProgramTheory.Spec.frame xs P)

theorem LaPToP.ProgramTheory.Spec.refines_frame.{u,
    v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)) :
  P.Refines
    (LaPToP.ProgramTheory.Spec.frame xs P)

A frame strengthens: `P ⇐ frame xs· P`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_mono.{u, v} {Var : Type u}
  {Val : Type v} (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val))
  (h : P.Refines Q) :
  (LaPToP.ProgramTheory.Spec.frame xs P).Refines
    (LaPToP.ProgramTheory.Spec.frame xs Q)

theorem LaPToP.ProgramTheory.Spec.frame_mono.{u,
    v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val))
  (h : P.Refines Q) :
  (LaPToP.ProgramTheory.Spec.frame xs
        P).Refines
    (LaPToP.ProgramTheory.Spec.frame xs Q)

Frames are monotonic with respect to refinement.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_cond.{u, v} {Var : Type u}
  {Val : Type v} (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val))
  (b : LaPToP.ProgramTheory.Spec.State Var Val → Prop) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.cond b P Q) =
    LaPToP.ProgramTheory.Spec.cond b
      (LaPToP.ProgramTheory.Spec.frame xs P)
      (LaPToP.ProgramTheory.Spec.frame xs Q)

theorem LaPToP.ProgramTheory.Spec.frame_cond.{u,
    v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val))
  (b :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Prop) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.cond b P
        Q) =
    LaPToP.ProgramTheory.Spec.cond b
      (LaPToP.ProgramTheory.Spec.frame xs
        P)
      (LaPToP.ProgramTheory.Spec.frame xs
        Q)

A frame distributes over `if`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_seq.{u, v} {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)) :
  (LaPToP.ProgramTheory.Spec.frame xs (P.seq Q)).Refines
    ((LaPToP.ProgramTheory.Spec.frame xs P).seq
      (LaPToP.ProgramTheory.Spec.frame xs Q))

theorem LaPToP.ProgramTheory.Spec.frame_seq.{u, v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var)
  (P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)) :
  (LaPToP.ProgramTheory.Spec.frame xs
        (P.seq Q)).Refines
    ((LaPToP.ProgramTheory.Spec.frame xs
          P).seq
      (LaPToP.ProgramTheory.Spec.frame xs
        Q))

A sequence of framed specifications is a framed sequence:
`frame xs· (P. Q) ⇐ (frame xs· P). (frame xs· Q)`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.Spec.frame_assign.{u, v} {Var : Type u}
  {Val : Type v} (xs : Set Var) [DecidableEq Var] (x : Var)
  (hx : x ∈ xs) (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.assign x e) =
    LaPToP.ProgramTheory.Spec.assign x e

theorem LaPToP.ProgramTheory.Spec.frame_assign.{u,
    v}
  {Var : Type u} {Val : Type v}
  (xs : Set Var) [DecidableEq Var]
  (x : Var) (hx : x ∈ xs)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  LaPToP.ProgramTheory.Spec.frame xs
      (LaPToP.ProgramTheory.Spec.assign x
        e) =
    LaPToP.ProgramTheory.Spec.assign x e

Assignment to a framed variable is unaffected: `frame xs· x:= e = x:= e` for `x` in `xs`.

theoremdefined in LaPToP/ProgramTheory/Scope.lean

complete

theorem LaPToP.ProgramTheory.ScopeExamples.assign_sum_eq_frame_newVar
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.Spec.assign
      LaPToP.ProgramTheory.ListSummation.SV.s fun x =>
      List.sum L.contents) =
    LaPToP.ProgramTheory.Spec.frame
      {LaPToP.ProgramTheory.ListSummation.SV.s}
      (LaPToP.ProgramTheory.Spec.newVar fun x st' =>
        st'.1 LaPToP.ProgramTheory.ListSummation.SV.s =
          List.sum L.contents)

theorem LaPToP.ProgramTheory.ScopeExamples.assign_sum_eq_frame_newVar
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.Spec.assign
      LaPToP.ProgramTheory.ListSummation.SV.s
      fun x => List.sum L.contents) =
    LaPToP.ProgramTheory.Spec.frame
      {LaPToP.ProgramTheory.ListSummation.SV.s}
      (LaPToP.ProgramTheory.Spec.newVar
        fun x st' =>
        st'.1
            LaPToP.ProgramTheory.ListSummation.SV.s =
          List.sum L.contents)

`s:= ΣL = frame s· new n: nat· s′ = ΣL`: "first we reduce the state space to
`s`; ... next we introduce local variable `n`", on the state variables `s`, `n`
of the list summation.

Definition6.10

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 5.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 6.11

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"As a safety check, some programming languages include the notation \mathbf{assert}\ b where b is binary, to mean “b is true”. ... It is executed by checking that b is true; if it is, execution continues normally, but if not, an error message is printed and execution is suspended. ... \mathbf{assert}\ b = \mathbf{if}\ b\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ \mathbf{screen}!\ \text{“error”}.\ \mathbf{wait\ until}\ \infty. If b is true, \mathbf{assert}\ b is the same as \mathit{ok}. If b is false, an error message is printed, and execution cannot proceed in finite time to any following actions." Output (\mathbf{screen}!) is a Chapter 9 notation with no counterpart here, and \mathbf{wait\ until}\ \infty is t := \infty; so the else-branch is formalized as what the theory of Chapter 4 observes — the final time is \infty — on a state with a time variable, and the printed message is not modelled. Proved: \mathbf{assert}\ b = \mathit{ok} when b holds and t' = \infty otherwise, \mathbf{assert}\ \top = \mathit{ok} ("all assertions are redundant" in a correct program), implementability with nondecreasing time, and that a false assertion followed by P starts P at time \infty. Uses Definition 5.2 and Definition 5.14.

Lean code for Definition6.10●13 declarations

structure(3 fields)defined in LaPToP/ProgramTheory/Assertions.lean

complete

structure LaPToP.ProgramTheory.Assertions.AT : Type

structure LaPToP.ProgramTheory.Assertions.AT : Type

A state with a time variable `t` and two integer variables `x`, `y`.

Fields

t : ℕ∞

The time variable.

x : ℤ

The variable `x`.

y : ℤ

The variable `y`.

defdefined in LaPToP/ProgramTheory/Assertions.lean

complete

def LaPToP.ProgramTheory.Assertions.assignX
  (e : LaPToP.ProgramTheory.Assertions.AT → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT

def LaPToP.ProgramTheory.Assertions.assignX
  (e :
    LaPToP.ProgramTheory.Assertions.AT →
      ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Assertions.AT

`x:= e`.

defdefined in LaPToP/ProgramTheory/Assertions.lean

complete

def LaPToP.ProgramTheory.Assertions.assignY
  (e : LaPToP.ProgramTheory.Assertions.AT → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT

def LaPToP.ProgramTheory.Assertions.assignY
  (e :
    LaPToP.ProgramTheory.Assertions.AT →
      ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Assertions.AT

`y:= e`.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assignX_seq
  (e : LaPToP.ProgramTheory.Assertions.AT → ℤ)
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assignX e).seq P = fun s s' =>
    P { t := s.t, x := e s, y := s.y } s'

theorem LaPToP.ProgramTheory.Assertions.assignX_seq
  (e :
    LaPToP.ProgramTheory.Assertions.AT →
      ℤ)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assignX
          e).seq
      P =
    fun s s' =>
    P { t := s.t, x := e s, y := s.y } s'

Substitution Law for `x:= e`.

defdefined in LaPToP/ProgramTheory/Assertions.lean

complete

def LaPToP.ProgramTheory.Assertions.assert
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT

def LaPToP.ProgramTheory.Assertions.assert
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Assertions.AT

`assert b = if b then ok else screen! “error”. wait until ∞`: if `b` holds,
`ok`; otherwise "execution cannot proceed in finite time to any following
actions", i.e. `t′ = ∞` (the printed message is not modelled).

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_of_holds
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop)
  {s : LaPToP.ProgramTheory.Assertions.AT} (hb : b s)
  (s' : LaPToP.ProgramTheory.Assertions.AT) :
  LaPToP.ProgramTheory.Assertions.assert b s s' ↔
    LaPToP.ProgramTheory.Spec.ok s s'

theorem LaPToP.ProgramTheory.Assertions.assert_of_holds
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop)
  {s : LaPToP.ProgramTheory.Assertions.AT}
  (hb : b s)
  (s' :
    LaPToP.ProgramTheory.Assertions.AT) :
  LaPToP.ProgramTheory.Assertions.assert b
      s s' ↔
    LaPToP.ProgramTheory.Spec.ok s s'

"If `b` is true, `assert b` is the same as `ok`."

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_of_not
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop)
  {s : LaPToP.ProgramTheory.Assertions.AT} (hb : ¬b s)
  (s' : LaPToP.ProgramTheory.Assertions.AT) :
  LaPToP.ProgramTheory.Assertions.assert b s s' ↔ s'.t = ⊤

theorem LaPToP.ProgramTheory.Assertions.assert_of_not
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop)
  {s : LaPToP.ProgramTheory.Assertions.AT}
  (hb : ¬b s)
  (s' :
    LaPToP.ProgramTheory.Assertions.AT) :
  LaPToP.ProgramTheory.Assertions.assert b
      s s' ↔
    s'.t = ⊤

If `b` is false, `assert b` ends at time `∞`.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_true :
  (LaPToP.ProgramTheory.Assertions.assert fun x => True) =
    LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Assertions.assert_true :
  (LaPToP.ProgramTheory.Assertions.assert
      fun x => True) =
    LaPToP.ProgramTheory.Spec.ok

`assert ⊤ = ok`: "in a correct program, the asserted expressions will
always be true, and so all assertions are redundant".

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_refines_ensure
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop) :
  (LaPToP.ProgramTheory.Assertions.assert b).Refines
    (LaPToP.ProgramTheory.Spec.ensure b)

theorem LaPToP.ProgramTheory.Assertions.assert_refines_ensure
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop) :
  (LaPToP.ProgramTheory.Assertions.assert
        b).Refines
    (LaPToP.ProgramTheory.Spec.ensure b)

`ensure b` refines `assert b`: both are `ok` when `b` holds.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.implementable_assert
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop)
  (s : LaPToP.ProgramTheory.Assertions.AT) :
  ∃ s', LaPToP.ProgramTheory.Assertions.assert b s s' ∧ s.t ≤ s'.t

theorem LaPToP.ProgramTheory.Assertions.implementable_assert
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop)
  (s :
    LaPToP.ProgramTheory.Assertions.AT) :
  ∃ s',
    LaPToP.ProgramTheory.Assertions.assert
        b s s' ∧
      s.t ≤ s'.t

An assertion is implementable with time not decreasing: a false assertion
is satisfied by waiting forever.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.implementable_assert'
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop) :
  (LaPToP.ProgramTheory.Assertions.assert b).Implementable

theorem LaPToP.ProgramTheory.Assertions.implementable_assert'
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop) :
  (LaPToP.ProgramTheory.Assertions.assert
      b).Implementable

Hence `assert b` is implementable.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_seq_of_not
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop)
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT)
  {s : LaPToP.ProgramTheory.Assertions.AT} (hb : ¬b s)
  (s' : LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assert b).seq P s s' ↔
    ∃ s'', s''.t = ⊤ ∧ P s'' s'

theorem LaPToP.ProgramTheory.Assertions.assert_seq_of_not
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Assertions.AT)
  {s : LaPToP.ProgramTheory.Assertions.AT}
  (hb : ¬b s)
  (s' :
    LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assert
          b).seq
      P s s' ↔
    ∃ s'', s''.t = ⊤ ∧ P s'' s'

A false assertion followed by anything: "execution cannot proceed in finite
time to any following actions" — the following specification starts at time `∞`.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.assert_seq_of_holds
  (b : LaPToP.ProgramTheory.Assertions.AT → Prop)
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT)
  {s : LaPToP.ProgramTheory.Assertions.AT} (hb : b s)
  (s' : LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assert b).seq P s s' ↔ P s s'

theorem LaPToP.ProgramTheory.Assertions.assert_seq_of_holds
  (b :
    LaPToP.ProgramTheory.Assertions.AT →
      Prop)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Assertions.AT)
  {s : LaPToP.ProgramTheory.Assertions.AT}
  (hb : b s)
  (s' :
    LaPToP.ProgramTheory.Assertions.AT) :
  (LaPToP.ProgramTheory.Assertions.assert
          b).seq
      P s s' ↔
    P s s'

A true assertion followed by `P` is `P`.

Theorem6.11

Group member previews

Preview

Definition 6.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Theorem 5.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsprogramsbacktrackinghehner-5.4.0

"If P and Q are implementable specifications, so is P \lor Q. ... We could save this programming step by making disjunction a programming connective, perhaps using the notation \mathbf{or}. ... We introduce the notation \mathbf{ensure}\ b where b is binary, to mean “make b true without changing anything”: \mathbf{ensure}\ b = \mathbf{if}\ b\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ b \land \mathit{ok} = b \land \mathit{ok}. ... When b is false ... this is unimplementable (unless b is identically \top). However, in combination with other constructs, the whole may be implementable": x := 0\ \mathbf{or}\ x := 1.\ \mathbf{ensure}\ x = 1 = (x' = 1 \land y' = y) = x := 1. Proved: both forms of \mathbf{ensure}, \mathbf{ensure}\ \top = \mathit{ok}, \mathbf{ensure}\ b is implementable iff b holds in every state, \mathbf{ensure} refines \mathbf{assert}, P.\ \mathbf{ensure}\ b filters the results of P by b, (P\ \mathbf{or}\ Q).\ \mathbf{ensure}\ b = (P.\ \mathbf{ensure}\ b)\ \mathbf{or}\ (Q.\ \mathbf{ensure}\ b) (the choice is made to satisfy the later \mathbf{ensure}), P \lor Q \Leftarrow P, P \lor Q \Leftarrow Q, and the book's example. Uses Definition 6.10, Theorem 5.4 and Theorem 5.8.

Lean code for Theorem6.11●12 declarations

defdefined in LaPToP/ProgramTheory/Assertions.lean

complete

def LaPToP.ProgramTheory.Spec.ensure.{u} {σ : Type u} (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.ensure.{u}
  {σ : Type u} (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec σ

`ensure b = b ∧ ok`: "make `b` true without changing anything".

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.ensure_eq_cond.{u} {σ : Type u}
  (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.ensure b =
    LaPToP.ProgramTheory.Spec.cond b LaPToP.ProgramTheory.Spec.ok
      (LaPToP.ProgramTheory.Spec.and (fun s x => b s)
        LaPToP.ProgramTheory.Spec.ok)

theorem LaPToP.ProgramTheory.Spec.ensure_eq_cond.{u}
  {σ : Type u} (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.ensure b =
    LaPToP.ProgramTheory.Spec.cond b
      LaPToP.ProgramTheory.Spec.ok
      (LaPToP.ProgramTheory.Spec.and
        (fun s x => b s)
        LaPToP.ProgramTheory.Spec.ok)

`ensure b = if b then ok else b ∧ ok`, the book's first form.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.ensure_of_holds.{u} {σ : Type u}
  (b : σ → Prop) {s : σ} (hb : b s) (s' : σ) :
  LaPToP.ProgramTheory.Spec.ensure b s s' ↔
    LaPToP.ProgramTheory.Spec.ok s s'

theorem LaPToP.ProgramTheory.Spec.ensure_of_holds.{u}
  {σ : Type u} (b : σ → Prop) {s : σ}
  (hb : b s) (s' : σ) :
  LaPToP.ProgramTheory.Spec.ensure b s
      s' ↔
    LaPToP.ProgramTheory.Spec.ok s s'

"Like `assert b`, `ensure b` is equal to `ok` if `b` is true."

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.ensure_true.{u} {σ : Type u} :
  (LaPToP.ProgramTheory.Spec.ensure fun x => True) =
    LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.ensure_true.{u}
  {σ : Type u} :
  (LaPToP.ProgramTheory.Spec.ensure
      fun x => True) =
    LaPToP.ProgramTheory.Spec.ok

`ensure ⊤ = ok`.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_ensure_iff.{u} {σ : Type u}
  (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.ensure b).Implementable ↔ ∀ (s : σ), b s

theorem LaPToP.ProgramTheory.Spec.implementable_ensure_iff.{u}
  {σ : Type u} (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.ensure
        b).Implementable ↔
    ∀ (s : σ), b s

"When `b` is false, ... this is unimplementable (unless `b` is identically
`⊤`)": `ensure b` is implementable iff `b` holds in every state.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.seq_ensure.{u} {σ : Type u} (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  P.seq (LaPToP.ProgramTheory.Spec.ensure b) = fun s s' => P s s' ∧ b s'

theorem LaPToP.ProgramTheory.Spec.seq_ensure.{u}
  {σ : Type u} (b : σ → Prop)
  (P : LaPToP.ProgramTheory.Spec σ) :
  P.seq
      (LaPToP.ProgramTheory.Spec.ensure
        b) =
    fun s s' => P s s' ∧ b s'

`P. ensure b` keeps the results of `P` that satisfy `b`: `ensure` filters
the poststate.

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.or_seq_ensure.{u} {σ : Type u} (b : σ → Prop)
  (P Q : LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).seq (LaPToP.ProgramTheory.Spec.ensure b) =
    (P.seq (LaPToP.ProgramTheory.Spec.ensure b)).or
      (Q.seq (LaPToP.ProgramTheory.Spec.ensure b))

theorem LaPToP.ProgramTheory.Spec.or_seq_ensure.{u}
  {σ : Type u} (b : σ → Prop)
  (P Q : LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).seq
      (LaPToP.ProgramTheory.Spec.ensure
        b) =
    (P.seq
          (LaPToP.ProgramTheory.Spec.ensure
            b)).or
      (Q.seq
        (LaPToP.ProgramTheory.Spec.ensure
          b))

`(P or Q). ensure b = (P. ensure b) or (Q. ensure b)`: the choice is made
so as to satisfy the later `ensure` (backtracking).

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.or_refines_left.{u} {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) : (P.or Q).Refines P

theorem LaPToP.ProgramTheory.Spec.or_refines_left.{u}
  {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).Refines P

`P ∨ Q ⇐ P`: "normally this choice is made as a refinement".

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Spec.or_refines_right.{u} {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) : (P.or Q).Refines Q

theorem LaPToP.ProgramTheory.Spec.or_refines_right.{u}
  {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).Refines Q

`P ∨ Q ⇐ Q`.

defdefined in LaPToP/ProgramTheory/Assertions.lean

complete

def LaPToP.ProgramTheory.Assertions.choice :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Assertions.AT

def LaPToP.ProgramTheory.Assertions.choice :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Assertions.AT

`x:= 0 or x:= 1`: "a program whose execution assigns either 0 or 1 to `x`".

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.choice_ensure :
  LaPToP.ProgramTheory.Assertions.choice.seq
      (LaPToP.ProgramTheory.Spec.ensure fun s => s.x = 1) =
    LaPToP.ProgramTheory.Assertions.assignX fun x => 1

theorem LaPToP.ProgramTheory.Assertions.choice_ensure :
  LaPToP.ProgramTheory.Assertions.choice.seq
      (LaPToP.ProgramTheory.Spec.ensure
        fun s => s.x = 1) =
    LaPToP.ProgramTheory.Assertions.assignX
      fun x => 1

`x:= 0 or x:= 1. ensure x=1 = x:= 1`: "although an implementation is given a
choice between `x:= 0` and `x:= 1`, it must choose the right one to satisfy a
later binary expression".

theoremdefined in LaPToP/ProgramTheory/Assertions.lean

complete

theorem LaPToP.ProgramTheory.Assertions.implementable_choice :
  LaPToP.ProgramTheory.Assertions.choice.Implementable

theorem LaPToP.ProgramTheory.Assertions.implementable_choice :
  LaPToP.ProgramTheory.Assertions.choice.Implementable

`x:= 0 or x:= 1` is implementable, and so is the whole example.

Proof for Theorem 6.11

uses 0

The example: P.\ \mathbf{ensure}\ b is P \land b'; the disjunct x := 0 is excluded by x' = 1, leaving x := 1.