5. Program Theory🔗

Definition5.1

Group: Programs as predicates on pre- and post-states; refinement as implication; sequential composition, conditionals, and assignment in Hehner's theory. Sections 4.0–4.2 of the book are formalized in the Lean modules LaPToP.ProgramTheory.Specifications , LaPToP.ProgramTheory.Programs and LaPToP.ProgramTheory.Time . (15)

Group member previews

Preview

Definition 5.2

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 1.1

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Definition 5.2

Loading preview

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

✓L∃∀N

A program (or specification) is a Boolean expression relating initial and final states. Implementing a specification S by a program P means proving P \Rightarrow S (refinement).

"A specification is a binary expression whose variables represent quantities of interest": the prestate \sigma and the poststate \sigma'. In Lean a specification over a state space \sigma is a relation Spec σ := σ → σ → Prop between prestate and poststate — a proposition rather than a Binary, since \forall\sigma\cdot\exists\sigma'\cdot S over an infinite state space is not a computable binary value. Equality of specifications is Lean equality of relations, which by extensionality is the book's \forall\sigma, \sigma'\cdot P = Q. The book's four counting definitions — S is unsatisfiable for prestate \sigma when {\rm c\llap{/}}(\S\sigma'\cdot S) < 1, satisfiable when \ge 1 (equivalently \exists\sigma'\cdot S), deterministic when \le 1, nondeterministic when > 1 — and implementable, \forall\sigma\cdot\exists\sigma'\cdot S, are defined and shown equivalent to their counting forms via Theorem 2.6 and Definition 3.6. Specifications take values in Definition 1.1; the state variables are those of Definition 1.7.

Lean code for Definition5.1●13 declarations

abbrevdefined in LaPToP/ProgramTheory/Specifications.lean

complete

abbrev LaPToP.ProgramTheory.Spec.{u} (σ : Type u) : Type u

abbrev LaPToP.ProgramTheory.Spec.{u}
  (σ : Type u) : Type u

A *specification* over a state space `σ` (aPToP §4.0): a binary expression
in the prestate and the poststate, modelled as a relation.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.ext.{u} {σ : Type u}
  {P Q : LaPToP.ProgramTheory.Spec σ}
  (h : ∀ (s s' : σ), P s s' ↔ Q s s') : P = Q

theorem LaPToP.ProgramTheory.Spec.ext.{u}
  {σ : Type u}
  {P Q : LaPToP.ProgramTheory.Spec σ}
  (h : ∀ (s s' : σ), P s s' ↔ Q s s') :
  P = Q

Two specifications are equal iff they agree on all prestates and
poststates: `∀σ, σ′· P = Q`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.outputs.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) :
  LaPToP.BasicTheories.Bunch σ

def LaPToP.ProgramTheory.Spec.outputs.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) : LaPToP.BasicTheories.Bunch σ

`§σ′· S`, the bunch of satisfactory poststates for prestate `s`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Satisfiable.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) : Prop

def LaPToP.ProgramTheory.Spec.Satisfiable.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) : Prop

`S` is *satisfiable* for prestate `s`: `∃σ′· S`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Unsatisfiable.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) : Prop

def LaPToP.ProgramTheory.Spec.Unsatisfiable.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) : Prop

`S` is *unsatisfiable* for prestate `s`: `¢(§σ′· S) < 1`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Deterministic.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) : Prop

def LaPToP.ProgramTheory.Spec.Deterministic.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) : Prop

`S` is *deterministic* for prestate `s`: `¢(§σ′· S) ≤ 1`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Nondeterministic.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) : Prop

def LaPToP.ProgramTheory.Spec.Nondeterministic.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) : Prop

`S` is *nondeterministic* for prestate `s`: `¢(§σ′· S) > 1`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Implementable.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) : Prop

def LaPToP.ProgramTheory.Spec.Implementable.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) : Prop

`S` is *implementable*: `∀σ· ∃σ′· S` — "there must be at least one
satisfactory output state for each input state".

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.satisfiable_iff.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) :
  S.Satisfiable s ↔ 1 ≤ (S.outputs s).size

theorem LaPToP.ProgramTheory.Spec.satisfiable_iff.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) :
  S.Satisfiable s ↔ 1 ≤ (S.outputs s).size

`¢(§σ′· S) ≥ 1` is `∃σ′· S` (the book's rewriting of satisfiable).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.unsatisfiable_iff.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) :
  S.Unsatisfiable s ↔ (S.outputs s).size < 1

theorem LaPToP.ProgramTheory.Spec.unsatisfiable_iff.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) :
  S.Unsatisfiable s ↔
    (S.outputs s).size < 1

Unsatisfiable: `¢(§σ′· S) < 1`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.deterministic_iff.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) :
  S.Deterministic s ↔ (S.outputs s).size ≤ 1

theorem LaPToP.ProgramTheory.Spec.deterministic_iff.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) :
  S.Deterministic s ↔
    (S.outputs s).size ≤ 1

Deterministic: `¢(§σ′· S) ≤ 1`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.nondeterministic_iff.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) (s : σ) :
  S.Nondeterministic s ↔ 1 < (S.outputs s).size

theorem LaPToP.ProgramTheory.Spec.nondeterministic_iff.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ)
  (s : σ) :
  S.Nondeterministic s ↔
    1 < (S.outputs s).size

Nondeterministic: `¢(§σ′· S) > 1`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_iff.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  S.Implementable ↔ ∀ (s : σ), S.Satisfiable s

theorem LaPToP.ProgramTheory.Spec.implementable_iff.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  S.Implementable ↔
    ∀ (s : σ), S.Satisfiable s

Implementable means satisfiable for every prestate.

Definition5.2

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 4.9

Loading preview

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

Used by 10

Reverse dependency previews

Preview

Definition 5.3

Loading preview

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

✓L∃∀N

The specification notations of Section 4.0.0: \top and \bot; \mathit{ok} = (\sigma' = \sigma) = (x' = x \land y' = y \land \ldots), satisfied by doing nothing; S \land R, S \lor R, \neg S; \mathbf{if}\ b\ \mathbf{then}\ S\ \mathbf{else}\ R for b a binary expression of the initial state; sequential composition S.\ R = \exists\sigma''\cdot \langle\sigma'\cdot S\rangle\,\sigma'' \land \langle\sigma\cdot R\rangle\,\sigma'' ("first behaves according to S, then according to R, with the final state from S serving as initial state for R"); and refinement P \Leftarrow S, \forall\sigma, \sigma'\cdot P \Leftarrow S. A state is an assignment of values to state variables, State Var Val := Var → Val, and the assignment x := e = (\sigma' = \sigma \triangleleft \mathit{address}\ \text{“x”} \triangleright e) = (x' = e \land y' = y \land \ldots) is the poststate obtained by updating the prestate at x — literally the book's list-modification reading, cf. Definition 4.9. Extends Definition 5.1.

Lean code for Definition5.2●12 declarations

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.top.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.top.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

`⊤`, "the easiest specification to implement, because all computer behavior satisfies it".

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.bot.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.bot.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

`⊥`, "impossible to implement because it is not satisfied by any computer behavior".

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.ok.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.ok.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec σ

`ok = σ′ = σ`: "the final values of all variables equal the corresponding
initial values. A computer can satisfy this specification by doing nothing."

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.and.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.and.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec σ

`S ∧ R`, satisfied by computations satisfying both.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.or.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.or.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec σ

`S ∨ R`, satisfied by computations satisfying either.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.not.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.not.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec σ

`¬S`, satisfied by computations not satisfying `S`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

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

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

`if b then S else R`, for `b` a binary expression of the initial state:
`b∧S ∨ ¬b∧R`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.seq.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.seq.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec σ

`S. R = ∃σ′′· ⟨σ′· S⟩ σ′′ ∧ ⟨σ· R⟩ σ′′`, sequential composition: "a computer
that first behaves according to `S`, then behaves according to `R`, with the
final state from `S` serving as initial state for `R`".

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.Refines.{u} {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ) : Prop

def LaPToP.ProgramTheory.Spec.Refines.{u}
  {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ) :
  Prop

`P ⇐ S`, "`P` is refined by `S`": `∀σ, σ′· P ⇐ S`. "We call `P` the
“problem” and `S` the “solution”."

abbrevdefined in LaPToP/ProgramTheory/Specifications.lean

complete

abbrev LaPToP.ProgramTheory.Spec.State.{u, v} (Var : Type u) (Val : Type v) :
  Type (max u v)

abbrev LaPToP.ProgramTheory.Spec.State.{u, v}
  (Var : Type u) (Val : Type v) :
  Type (max u v)

A state as an assignment of values to state variables (aPToP §4): a
function from variable names to values.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.assign.{u, v} {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val)

def LaPToP.ProgramTheory.Spec.assign.{u, v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  LaPToP.ProgramTheory.Spec
    (LaPToP.ProgramTheory.Spec.State Var
      Val)

`x:= e`, "`x` is assigned `e`": `σ′ = σ⊲address “x”⊳e`, the poststate is
the prestate with `x` replaced by the value of `e` in the prestate; `e` is any
expression of the initial values.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.assign_iff.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val)
  (s s' : LaPToP.ProgramTheory.Spec.State Var Val) :
  LaPToP.ProgramTheory.Spec.assign x e s s' ↔
    s' x = e s ∧ ∀ (y : Var), y ≠ x → s' y = s y

theorem LaPToP.ProgramTheory.Spec.assign_iff.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val)
  (s s' :
    LaPToP.ProgramTheory.Spec.State Var
      Val) :
  LaPToP.ProgramTheory.Spec.assign x e s
      s' ↔
    s' x = e s ∧
      ∀ (y : Var), y ≠ x → s' y = s y

`x:= e = x′=e ∧ y′=y ∧ ...`: the assigned variable gets `e`, every other
variable is unchanged.

Definition5.3

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 5.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Definition 5.6

Loading preview

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

✓L∃∀N

The assignment x := e relates pre-state and post-state by setting x to the value of e in the pre-state and leaving other variables unchanged. This is the atomic building block for Definition 5.1; in Lean it is Spec.assign x e, with assign_iff giving the x' = e \land y' = y \land \ldots form. Defined in Definition 5.2.

Lean code for Definition5.3●3 declarations

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.assign.{u, v} {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val)

def LaPToP.ProgramTheory.Spec.assign.{u, v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  LaPToP.ProgramTheory.Spec
    (LaPToP.ProgramTheory.Spec.State Var
      Val)

`x:= e`, "`x` is assigned `e`": `σ′ = σ⊲address “x”⊳e`, the poststate is
the prestate with `x` replaced by the value of `e` in the prestate; `e` is any
expression of the initial values.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.assign_iff.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val)
  (s s' : LaPToP.ProgramTheory.Spec.State Var Val) :
  LaPToP.ProgramTheory.Spec.assign x e s s' ↔
    s' x = e s ∧ ∀ (y : Var), y ≠ x → s' y = s y

theorem LaPToP.ProgramTheory.Spec.assign_iff.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val)
  (s s' :
    LaPToP.ProgramTheory.Spec.State Var
      Val) :
  LaPToP.ProgramTheory.Spec.assign x e s
      s' ↔
    s' x = e s ∧
      ∀ (y : Var), y ≠ x → s' y = s y

`x:= e = x′=e ∧ y′=y ∧ ...`: the assigned variable gets `e`, every other
variable is unchanged.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_assign.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  (LaPToP.ProgramTheory.Spec.assign x e).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_assign.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  (LaPToP.ProgramTheory.Spec.assign x
      e).Implementable

`x:= e` is implementable.

Theorem5.4

Group member previews

Preview

Definition 5.1

Loading preview

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

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 5.10

Loading preview

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

✓L∃∀N

EffortsmallTagsprogramshehner-4.0

\mathit{ok}, \top and x := e are implementable; \bot is not (on a nonempty state space). "The \lor and \mathbf{if}\ \mathbf{then}\ \mathbf{else} operators have the nice property that if their operands are implementable, so is the result; the operators \land and \neg do not have that property" — \lor, \mathbf{if} and S.\ R preserve implementability, and \mathit{ok} \land \neg\mathit{ok} is a counterexample for \land, \neg. Uses Definition 5.2.

Lean code for Theorem5.4●8 theorems

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_ok.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec.ok.Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_ok.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec.ok.Implementable

`ok` is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_top.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_top.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Implementable

`⊤` is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.not_implementable_bot.{u} {σ : Type u}
  [Nonempty σ] : ¬LaPToP.ProgramTheory.Spec.bot.Implementable

theorem LaPToP.ProgramTheory.Spec.not_implementable_bot.{u}
  {σ : Type u} [Nonempty σ] :
  ¬LaPToP.ProgramTheory.Spec.bot.Implementable

`⊥` is not implementable (on a nonempty state space).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_assign.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  (LaPToP.ProgramTheory.Spec.assign x e).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_assign.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (e :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  (LaPToP.ProgramTheory.Spec.assign x
      e).Implementable

`x:= e` is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_or.{u} {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ} (hS : S.Implementable) :
  (S.or R).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_or.{u}
  {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ}
  (hS : S.Implementable) :
  (S.or R).Implementable

"The `∨` and `if then else` operators have the nice property that if their
operands are implementable, so is the result": `∨`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_cond.{u} {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop)
  (hS : S.Implementable) (hR : R.Implementable) :
  (LaPToP.ProgramTheory.Spec.cond b S R).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_cond.{u}
  {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop) (hS : S.Implementable)
  (hR : R.Implementable) :
  (LaPToP.ProgramTheory.Spec.cond b S
      R).Implementable

`if b then S else R` is implementable when `S` and `R` are.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_seq.{u} {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ} (hS : S.Implementable)
  (hR : R.Implementable) : (S.seq R).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_seq.{u}
  {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ}
  (hS : S.Implementable)
  (hR : R.Implementable) :
  (S.seq R).Implementable

`S. R` is implementable when `S` and `R` are.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.not_implementable_and_not.{u} {σ : Type u}
  [Nonempty σ] :
  ¬(LaPToP.ProgramTheory.Spec.ok.and
        LaPToP.ProgramTheory.Spec.ok.not).Implementable

theorem LaPToP.ProgramTheory.Spec.not_implementable_and_not.{u}
  {σ : Type u} [Nonempty σ] :
  ¬(LaPToP.ProgramTheory.Spec.ok.and
        LaPToP.ProgramTheory.Spec.ok.not).Implementable

"The operators `∧` and `¬` do not have that property": `ok ∧ ¬ok` is not
implementable although `ok` is.

Theorem5.5

Group member previews

Preview

Definition 5.1

Loading preview

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

uses 1used by 1✓L∃∀N

EffortsmallPriorityhighTagsprogramsrefinement

The trivial program that leaves the state unchanged (ok / skip) implements the always-true specification. In propositional form this is the reflexivity seed for refinement of Definition 5.1.

Lean code for Theorem5.5●1 theorem

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.top_refines_ok.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Refines LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.top_refines_ok.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Refines
    LaPToP.ProgramTheory.Spec.ok

`⊤ ⇐ ok`: doing nothing implements the always-true specification.

Proof for Theorem 5.5

uses 0

Immediate: the identity relation implies \top.

Lean code for Theorem5.5

open LaPToP.ProgramTheory in
theorem skip_refines_true {σ : Type} :
    Spec.Refines (Spec.top : Spec σ) Spec.ok :=
  Spec.top_refines _

Definition5.6

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 5.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 5.7

Loading preview

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

✓L∃∀N

Sequential composition P ; Q exists when there is an intermediate state accepted as final by P and initial by Q. It builds programs from Definition 5.3 and larger blocks while preserving Definition 5.1. Hehner writes it P.\ Q ("dot"); in Lean it is Spec.seq P Q, defined in Definition 5.2.

Lean code for Definition5.6●2 declarations

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Spec.seq.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) : LaPToP.ProgramTheory.Spec σ

def LaPToP.ProgramTheory.Spec.seq.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec σ

`S. R = ∃σ′′· ⟨σ′· S⟩ σ′′ ∧ ⟨σ· R⟩ σ′′`, sequential composition: "a computer
that first behaves according to `S`, then behaves according to `R`, with the
final state from `S` serving as initial state for `R`".

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_seq.{u} {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ} (hS : S.Implementable)
  (hR : R.Implementable) : (S.seq R).Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_seq.{u}
  {σ : Type u}
  {S R : LaPToP.ProgramTheory.Spec σ}
  (hS : S.Implementable)
  (hR : R.Implementable) :
  (S.seq R).Implementable

`S. R` is implementable when `S` and `R` are.

Theorem5.7

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 1.6

Loading preview

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

used by 1✓L∃∀N

EffortsmallTagsprogramslawshehner-4.0.1

The Specification Laws of Section 4.0.1, for specifications P, Q, R, S and binary b of the prestate: \mathit{ok}.\ P = P = P.\ \mathit{ok} (Identity), P.\ (Q.\ R) = (P.\ Q).\ R (Associative), \mathbf{if}\ b\ \mathbf{then}\ P\ \mathbf{else}\ P = P (Idempotent), \mathbf{if}\ b\ \mathbf{then}\ P\ \mathbf{else}\ Q = \mathbf{if}\ \neg b\ \mathbf{then}\ Q\ \mathbf{else}\ P (Case Reversal), P = \mathbf{if}\ b\ \mathbf{then}\ b \Rightarrow P\ \mathbf{else}\ \neg b \Rightarrow P (Case Creation), \mathbf{if}\ b\ \mathbf{then}\ S\ \mathbf{else}\ R = b \land S \lor \neg b \land R = (b \Rightarrow S) \land (\neg b \Rightarrow R) (Case Analysis), P \lor Q.\ R \lor S = (P.\ R) \lor (P.\ S) \lor (Q.\ R) \lor (Q.\ S) (Distributive), \mathbf{if}\ b\ \mathbf{then}\ P\ \mathbf{else}\ Q \land R = \mathbf{if}\ b\ \mathbf{then}\ P \land R\ \mathbf{else}\ Q \land R (Distributive — "we can replace \land with any other binary operator", stated once for an arbitrary operator), \mathbf{if}\ b\ \mathbf{then}\ P\ \mathbf{else}\ Q.\ R = \mathbf{if}\ b\ \mathbf{then}\ P.\ R\ \mathbf{else}\ Q.\ R (Distributive, b unprimed), and x := \mathbf{if}\ b\ \mathbf{then}\ e\ \mathbf{else}\ f = \mathbf{if}\ b\ \mathbf{then}\ x := e\ \mathbf{else}\ x := f (Functional-Imperative). Uses Definition 5.2, Definition 5.6 and Theorem 1.6.

Lean code for Theorem5.7●15 theorems

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.ok_seq.{u} {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec.ok.seq P = P

theorem LaPToP.ProgramTheory.Spec.ok_seq.{u}
  {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec.ok.seq P = P

`ok. P = P` (Identity Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.seq_ok.{u} {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) :
  P.seq LaPToP.ProgramTheory.Spec.ok = P

theorem LaPToP.ProgramTheory.Spec.seq_ok.{u}
  {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) :
  P.seq LaPToP.ProgramTheory.Spec.ok = P

`P. ok = P` (Identity Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.seq_assoc.{u} {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ) :
  P.seq (Q.seq R) = (P.seq Q).seq R

theorem LaPToP.ProgramTheory.Spec.seq_assoc.{u}
  {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ) :
  P.seq (Q.seq R) = (P.seq Q).seq R

`P. (Q. R) = (P. Q). R` (Associative Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_self.{u} {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b P P = P

theorem LaPToP.ProgramTheory.Spec.cond_self.{u}
  {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b P P = P

`if b then P else P = P` (Idempotent Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_not.{u} {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b P Q =
    LaPToP.ProgramTheory.Spec.cond (fun s => ¬b s) Q P

theorem LaPToP.ProgramTheory.Spec.cond_not.{u}
  {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b P Q =
    LaPToP.ProgramTheory.Spec.cond
      (fun s => ¬b s) Q P

`if b then P else Q = if ¬b then Q else P` (Case Reversal Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.case_creation.{u} {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  P =
    LaPToP.ProgramTheory.Spec.cond b (fun s s' => b s → P s s')
      fun s s' => ¬b s → P s s'

theorem LaPToP.ProgramTheory.Spec.case_creation.{u}
  {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  P =
    LaPToP.ProgramTheory.Spec.cond b
      (fun s s' => b s → P s s')
      fun s s' => ¬b s → P s s'

`P = if b then b ⇒ P else ¬b ⇒ P` (Case Creation Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_eq_or.{u} {σ : Type u}
  (R S : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b S R =
    (LaPToP.ProgramTheory.Spec.and (fun s x => b s) S).or
      (LaPToP.ProgramTheory.Spec.and (fun s x => ¬b s) R)

theorem LaPToP.ProgramTheory.Spec.cond_eq_or.{u}
  {σ : Type u}
  (R S : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b S R =
    (LaPToP.ProgramTheory.Spec.and
          (fun s x => b s) S).or
      (LaPToP.ProgramTheory.Spec.and
        (fun s x => ¬b s) R)

`if b then S else R = b∧S ∨ ¬b∧R` (Case Analysis Law), the definition.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_eq_and.{u} {σ : Type u}
  (R S : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b S R = fun s s' =>
    (b s → S s s') ∧ (¬b s → R s s')

theorem LaPToP.ProgramTheory.Spec.cond_eq_and.{u}
  {σ : Type u}
  (R S : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  LaPToP.ProgramTheory.Spec.cond b S R =
    fun s s' =>
    (b s → S s s') ∧ (¬b s → R s s')

`if b then S else R = (b⇒S) ∧ (¬b⇒R)` (Case Analysis Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_pos.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) {s : σ} (hb : b s)
  (s' : σ) : LaPToP.ProgramTheory.Spec.cond b S R s s' = S s s'

theorem LaPToP.ProgramTheory.Spec.cond_pos.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) {s : σ} (hb : b s)
  (s' : σ) :
  LaPToP.ProgramTheory.Spec.cond b S R s
      s' =
    S s s'

`if b then S else R` for a prestate satisfying `b` is `S`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_neg.{u} {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) {s : σ} (hb : ¬b s)
  (s' : σ) : LaPToP.ProgramTheory.Spec.cond b S R s s' = R s s'

theorem LaPToP.ProgramTheory.Spec.cond_neg.{u}
  {σ : Type u}
  (S R : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) {s : σ} (hb : ¬b s)
  (s' : σ) :
  LaPToP.ProgramTheory.Spec.cond b S R s
      s' =
    R s s'

`if b then S else R` for a prestate not satisfying `b` is `R`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.or_seq_or.{u} {σ : Type u}
  (P Q R S : LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).seq (R.or S) =
    ((P.seq R).or (P.seq S)).or ((Q.seq R).or (Q.seq S))

theorem LaPToP.ProgramTheory.Spec.or_seq_or.{u}
  {σ : Type u}
  (P Q R S :
    LaPToP.ProgramTheory.Spec σ) :
  (P.or Q).seq (R.or S) =
    ((P.seq R).or (P.seq S)).or
      ((Q.seq R).or (Q.seq S))

`P∨Q. R∨S = (P. R) ∨ (P. S) ∨ (Q. R) ∨ (Q. S)` (Distributive Law).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_op.{u} {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop)
  (op : Prop → Prop → Prop) :
  (fun s s' =>
      op (LaPToP.ProgramTheory.Spec.cond b P Q s s') (R s s')) =
    LaPToP.ProgramTheory.Spec.cond b (fun s s' => op (P s s') (R s s'))
      fun s s' => op (Q s s') (R s s')

theorem LaPToP.ProgramTheory.Spec.cond_op.{u}
  {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop)
  (op : Prop → Prop → Prop) :
  (fun s s' =>
      op
        (LaPToP.ProgramTheory.Spec.cond b
          P Q s s')
        (R s s')) =
    LaPToP.ProgramTheory.Spec.cond b
      (fun s s' => op (P s s') (R s s'))
      fun s s' => op (Q s s') (R s s')

`if b then P else Q ∧ R = if b then P∧R else Q∧R` (Distributive Law), for
`∧` and, "replacing `∧` with any other binary operator", for any `op`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_and.{u} {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.cond b P Q).and R =
    LaPToP.ProgramTheory.Spec.cond b (P.and R) (Q.and R)

theorem LaPToP.ProgramTheory.Spec.cond_and.{u}
  {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.cond b P
          Q).and
      R =
    LaPToP.ProgramTheory.Spec.cond b
      (P.and R) (Q.and R)

The `∧` instance of the Distributive Law, as printed in the book.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_seq.{u} {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ) (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.cond b P Q).seq R =
    LaPToP.ProgramTheory.Spec.cond b (P.seq R) (Q.seq R)

theorem LaPToP.ProgramTheory.Spec.cond_seq.{u}
  {σ : Type u}
  (P Q R : LaPToP.ProgramTheory.Spec σ)
  (b : σ → Prop) :
  (LaPToP.ProgramTheory.Spec.cond b P
          Q).seq
      R =
    LaPToP.ProgramTheory.Spec.cond b
      (P.seq R) (Q.seq R)

`if b then P else Q. R = if b then P. R else Q. R` (Distributive Law), for
`b` a binary expression of the prestate.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.assign_ite.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] (x : Var)
  (b : LaPToP.ProgramTheory.Spec.State Var Val → Prop)
  (e f : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  (LaPToP.ProgramTheory.Spec.assign x fun s =>
      if b s then e s else f s) =
    LaPToP.ProgramTheory.Spec.cond b
      (LaPToP.ProgramTheory.Spec.assign x e)
      (LaPToP.ProgramTheory.Spec.assign x f)

theorem LaPToP.ProgramTheory.Spec.assign_ite.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] (x : Var)
  (b :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Prop)
  (e f :
    LaPToP.ProgramTheory.Spec.State Var
        Val →
      Val) :
  (LaPToP.ProgramTheory.Spec.assign x
      fun s => if b s then e s else f s) =
    LaPToP.ProgramTheory.Spec.cond b
      (LaPToP.ProgramTheory.Spec.assign x
        e)
      (LaPToP.ProgramTheory.Spec.assign x
        f)

`x:= if b then e else f = if b then x:= e else x:= f` (Functional-Imperative Law).

Proof for Theorem 5.7

uses 0

Extensionality over prestate and poststate, then propositional reasoning; the laws about \mathbf{if} split on whether the prestate satisfies b.

Theorem5.8

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 5.3

Loading preview

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

Used by 9

Reverse dependency previews

Preview

Theorem 5.10

Loading preview

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

✓L∃∀N

EffortsmallTagsprogramslawshehner-4.0.1

The Substitution Law: for e an expression of the prestate, x := e.\ P = \langle x \cdot P\rangle\,e = (\text{substitute } e \text{ for } x \text{ in } P) — "an assignment followed by any specification is the same as the specification but with the assigned variable replaced by the assigned expression". In the state-function model this is P evaluated at the updated prestate. The book's worked calculations x := x + y = (x' = x + y \land y' = y), x := 3.\ y := x + y = (x' = 3 \land y' = 3 + y), and (x' = x \lor x' = x+1).\ (x' = x \lor x' = x+1) = (x' = x \lor x' = x+1 \lor x' = x+2) are checked. Uses Definition 5.3 and Definition 5.6.

Lean code for Theorem5.8●4 theorems

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

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

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

`x:= e. P = ⟨x· P⟩ e = (substitute e for x in P)` (Substitution Law), for
`e` an expression of the prestate: an assignment followed by any specification
is the specification evaluated at the updated prestate.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.assign_x_add_y
  (s s' : LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Spec.assign LaPToP.ProgramTheory.Examples.V.x
      (fun s =>
        s LaPToP.ProgramTheory.Examples.V.x +
          s LaPToP.ProgramTheory.Examples.V.y)
      s s' ↔
    s' LaPToP.ProgramTheory.Examples.V.x =
        s LaPToP.ProgramTheory.Examples.V.x +
          s LaPToP.ProgramTheory.Examples.V.y ∧
      s' LaPToP.ProgramTheory.Examples.V.y =
        s LaPToP.ProgramTheory.Examples.V.y

theorem LaPToP.ProgramTheory.Examples.assign_x_add_y
  (s s' :
    LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Spec.assign
      LaPToP.ProgramTheory.Examples.V.x
      (fun s =>
        s
            LaPToP.ProgramTheory.Examples.V.x +
          s
            LaPToP.ProgramTheory.Examples.V.y)
      s s' ↔
    s' LaPToP.ProgramTheory.Examples.V.x =
        s
            LaPToP.ProgramTheory.Examples.V.x +
          s
            LaPToP.ProgramTheory.Examples.V.y ∧
      s'
          LaPToP.ProgramTheory.Examples.V.y =
        s
          LaPToP.ProgramTheory.Examples.V.y

`x:= x+y = x′=x+y ∧ y′=y`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.assign_three_seq :
  (LaPToP.ProgramTheory.Spec.assign LaPToP.ProgramTheory.Examples.V.x
          fun x => 3).seq
      (LaPToP.ProgramTheory.Spec.assign
        LaPToP.ProgramTheory.Examples.V.y fun s =>
        s LaPToP.ProgramTheory.Examples.V.x +
          s LaPToP.ProgramTheory.Examples.V.y) =
    fun s s' =>
    s' LaPToP.ProgramTheory.Examples.V.x = 3 ∧
      s' LaPToP.ProgramTheory.Examples.V.y =
        3 + s LaPToP.ProgramTheory.Examples.V.y

theorem LaPToP.ProgramTheory.Examples.assign_three_seq :
  (LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.Examples.V.x
          fun x => 3).seq
      (LaPToP.ProgramTheory.Spec.assign
        LaPToP.ProgramTheory.Examples.V.y
        fun s =>
        s
            LaPToP.ProgramTheory.Examples.V.x +
          s
            LaPToP.ProgramTheory.Examples.V.y) =
    fun s s' =>
    s' LaPToP.ProgramTheory.Examples.V.x =
        3 ∧
      s'
          LaPToP.ProgramTheory.Examples.V.y =
        3 +
          s
            LaPToP.ProgramTheory.Examples.V.y

`x:= 3. y:= x+y = x′=3 ∧ y′=3+y`, the book's worked example.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.seq_step_step :
  (LaPToP.ProgramTheory.Spec.seq (fun x x' => x' = x ∨ x' = x + 1)
      fun x x' => x' = x ∨ x' = x + 1) =
    fun x x' => x' = x ∨ x' = x + 1 ∨ x' = x + 2

theorem LaPToP.ProgramTheory.Examples.seq_step_step :
  (LaPToP.ProgramTheory.Spec.seq
      (fun x x' => x' = x ∨ x' = x + 1)
      fun x x' => x' = x ∨ x' = x + 1) =
    fun x x' =>
    x' = x ∨ x' = x + 1 ∨ x' = x + 2

`(x′=x ∨ x′=x+1). (x′=x ∨ x′=x+1) = x′=x ∨ x′=x+1 ∨ x′=x+2`, in one
integer variable: "if we either leave `x` alone or add 1 to it, and then again
we either leave `x` alone or add 1 to it, the net result is that we leave it
alone, or add 1 to it, or add 2 to it".

Proof for Theorem 5.8

uses 0

Unfold sequential composition: the intermediate state is forced to be the updated prestate.

Theorem5.9

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 5.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 5.10

Loading preview

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

✓L∃∀N

EffortsmallTagsprogramsrefinementhehner-4.0.2

Refinement P \Leftarrow S is reflexive and transitive; "two specifications P and Q are equal if and only if each is satisfied whenever the other is" (mutual refinement is equality); \top \Leftarrow S for every S and S \Leftarrow \bot for every S; and "weaker specifications are easier to implement": if P \Leftarrow S and S is implementable then so is P. Uses Definition 5.1 and Theorem 5.5.

Lean code for Theorem5.9●8 theorems

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_refl.{u} {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) : P.Refines P

theorem LaPToP.ProgramTheory.Spec.refines_refl.{u}
  {σ : Type u}
  (P : LaPToP.ProgramTheory.Spec σ) :
  P.Refines P

`P ⇐ P`: refinement is reflexive.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_trans.{u} {σ : Type u}
  (P Q S : LaPToP.ProgramTheory.Spec σ) (h₁ : P.Refines Q)
  (h₂ : Q.Refines S) : P.Refines S

theorem LaPToP.ProgramTheory.Spec.refines_trans.{u}
  {σ : Type u}
  (P Q S : LaPToP.ProgramTheory.Spec σ)
  (h₁ : P.Refines Q) (h₂ : Q.Refines S) :
  P.Refines S

Refinement is transitive: a solution's solution solves the problem.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_antisymm.{u} {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ) (h₁ : P.Refines Q)
  (h₂ : Q.Refines P) : P = Q

theorem LaPToP.ProgramTheory.Spec.refines_antisymm.{u}
  {σ : Type u}
  (P Q : LaPToP.ProgramTheory.Spec σ)
  (h₁ : P.Refines Q) (h₂ : Q.Refines P) :
  P = Q

"Two specifications `P` and `Q` are equal if and only if each is satisfied
whenever the other is": mutual refinement is equality.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.top_refines.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec.top.Refines S

theorem LaPToP.ProgramTheory.Spec.top_refines.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  LaPToP.ProgramTheory.Spec.top.Refines S

`⊤ ⇐ S`: every specification refines `⊤`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_bot.{u} {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  S.Refines LaPToP.ProgramTheory.Spec.bot

theorem LaPToP.ProgramTheory.Spec.refines_bot.{u}
  {σ : Type u}
  (S : LaPToP.ProgramTheory.Spec σ) :
  S.Refines LaPToP.ProgramTheory.Spec.bot

`S ⇐ ⊥`: `⊥` refines every specification (but is unimplementable).

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.top_refines_ok.{u} {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Refines LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Spec.top_refines_ok.{u}
  {σ : Type u} :
  LaPToP.ProgramTheory.Spec.top.Refines
    LaPToP.ProgramTheory.Spec.ok

`⊤ ⇐ ok`: doing nothing implements the always-true specification.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.implementable_of_refines.{u} {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ) (h : P.Refines S)
  (hS : S.Implementable) : P.Implementable

theorem LaPToP.ProgramTheory.Spec.implementable_of_refines.{u}
  {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ)
  (h : P.Refines S)
  (hS : S.Implementable) : P.Implementable

"Weaker specifications are easier to implement": a refinement of an
implementable specification by `S` makes `P` implementable too.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_iff.{u} {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ) :
  P.Refines S ↔ ∀ (s s' : σ), S s s' → P s s'

theorem LaPToP.ProgramTheory.Spec.refines_iff.{u}
  {σ : Type u}
  (P S : LaPToP.ProgramTheory.Spec σ) :
  P.Refines S ↔
    ∀ (s s' : σ), S s s' → P s s'

`P ⇐ S` is `∀σ, σ′· P ⇐ S`: the book's definition, unfolded.

Theorem5.10

Group member previews

Preview

Definition 5.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

EffortsmallTagsprogramsrefinementhehner-4.0

The book's running example in two integer state variables x, y: x' = x+1 \land y' = y is implementable and deterministic for each prestate; x' > x is implementable and nondeterministic for each prestate; x \ge 0 \land y' = 0 is not implementable while x \ge 0 \Rightarrow y' = 0 is; and the four refinements x' > x \Leftarrow x' = x+1 \land y' = y, x' = x+1 \land y' = y \Leftarrow x := x+1, x' \le x \Leftarrow \mathbf{if}\ x = 0\ \mathbf{then}\ x' = x\ \mathbf{else}\ x' < x, x' > y' > x \Leftarrow y := x+1.\ x := y+1. Uses Theorem 5.9, Theorem 5.8 and Theorem 5.4.

Lean code for Theorem5.10●14 declarations

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

complete

inductive LaPToP.ProgramTheory.Examples.V : Type

inductive LaPToP.ProgramTheory.Examples.V : Type

The state variables of the book's running example.

Constructors

LaPToP.ProgramTheory.Examples.V.x :
  LaPToP.ProgramTheory.Examples.V

The state variable `x`.

LaPToP.ProgramTheory.Examples.V.y :
  LaPToP.ProgramTheory.Examples.V

The state variable `y`.

abbrevdefined in LaPToP/ProgramTheory/Specifications.lean

complete

abbrev LaPToP.ProgramTheory.Examples.St : Type

abbrev LaPToP.ProgramTheory.Examples.St : Type

States over the two integer variables `x` and `y`.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Examples.incr :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Examples.St

def LaPToP.ProgramTheory.Examples.incr :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Examples.St

`x′ = x+1 ∧ y′ = y`, "a computer that increases the value of `x` by 1 and
leaves `y` unchanged".

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.implementable_incr :
  LaPToP.ProgramTheory.Examples.incr.Implementable

theorem LaPToP.ProgramTheory.Examples.implementable_incr :
  LaPToP.ProgramTheory.Examples.incr.Implementable

`x′ = x+1 ∧ y′ = y` is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.deterministic_incr
  (s : LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Examples.incr.Deterministic s

theorem LaPToP.ProgramTheory.Examples.deterministic_incr
  (s : LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Examples.incr.Deterministic
    s

`x′ = x+1 ∧ y′ = y` is deterministic for each prestate.

defdefined in LaPToP/ProgramTheory/Specifications.lean

complete

def LaPToP.ProgramTheory.Examples.gt :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Examples.St

def LaPToP.ProgramTheory.Examples.gt :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Examples.St

`x′ > x`, "a computation that increases `x` by any amount".

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.implementable_gt :
  LaPToP.ProgramTheory.Examples.gt.Implementable

theorem LaPToP.ProgramTheory.Examples.implementable_gt :
  LaPToP.ProgramTheory.Examples.gt.Implementable

`x′ > x` is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.nondeterministic_gt
  (s : LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Examples.gt.Nondeterministic s

theorem LaPToP.ProgramTheory.Examples.nondeterministic_gt
  (s : LaPToP.ProgramTheory.Examples.St) :
  LaPToP.ProgramTheory.Examples.gt.Nondeterministic
    s

`x′ > x` is nondeterministic for each prestate.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.not_implementable_nonneg_and :
  ¬LaPToP.ProgramTheory.Spec.Implementable fun s s' =>
      s LaPToP.ProgramTheory.Examples.V.x ≥ 0 ∧
        s' LaPToP.ProgramTheory.Examples.V.y = 0

theorem LaPToP.ProgramTheory.Examples.not_implementable_nonneg_and :
  ¬LaPToP.ProgramTheory.Spec.Implementable
      fun s s' =>
      s
            LaPToP.ProgramTheory.Examples.V.x ≥
          0 ∧
        s'
            LaPToP.ProgramTheory.Examples.V.y =
          0

`x≥0 ∧ y′=0` is not implementable: "if the initial value of `x` is
negative, there is no way to satisfy the specification".

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.implementable_nonneg_imp :
  LaPToP.ProgramTheory.Spec.Implementable fun s s' =>
    s LaPToP.ProgramTheory.Examples.V.x ≥ 0 →
      s' LaPToP.ProgramTheory.Examples.V.y = 0

theorem LaPToP.ProgramTheory.Examples.implementable_nonneg_imp :
  LaPToP.ProgramTheory.Spec.Implementable
    fun s s' =>
    s LaPToP.ProgramTheory.Examples.V.x ≥
        0 →
      s'
          LaPToP.ProgramTheory.Examples.V.y =
        0

`x≥0 ⇒ y′=0`, the specifier's intended version, is implementable.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.refine₁ :
  LaPToP.ProgramTheory.Examples.gt.Refines
    LaPToP.ProgramTheory.Examples.incr

theorem LaPToP.ProgramTheory.Examples.refine₁ :
  LaPToP.ProgramTheory.Examples.gt.Refines
    LaPToP.ProgramTheory.Examples.incr

`x′>x ⇐ x′=x+1 ∧ y′=y`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.refine₂ :
  LaPToP.ProgramTheory.Examples.incr.Refines
    (LaPToP.ProgramTheory.Spec.assign LaPToP.ProgramTheory.Examples.V.x
      fun s => s LaPToP.ProgramTheory.Examples.V.x + 1)

theorem LaPToP.ProgramTheory.Examples.refine₂ :
  LaPToP.ProgramTheory.Examples.incr.Refines
    (LaPToP.ProgramTheory.Spec.assign
      LaPToP.ProgramTheory.Examples.V.x
      fun s =>
      s
          LaPToP.ProgramTheory.Examples.V.x +
        1)

`x′=x+1 ∧ y′=y ⇐ x:= x+1`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.refine₃ :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s' LaPToP.ProgramTheory.Examples.V.x ≤
        s LaPToP.ProgramTheory.Examples.V.x)
    (LaPToP.ProgramTheory.Spec.cond
      (fun s => s LaPToP.ProgramTheory.Examples.V.x = 0)
      (fun s s' =>
        s' LaPToP.ProgramTheory.Examples.V.x =
          s LaPToP.ProgramTheory.Examples.V.x)
      fun s s' =>
      s' LaPToP.ProgramTheory.Examples.V.x <
        s LaPToP.ProgramTheory.Examples.V.x)

theorem LaPToP.ProgramTheory.Examples.refine₃ :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s'
          LaPToP.ProgramTheory.Examples.V.x ≤
        s
          LaPToP.ProgramTheory.Examples.V.x)
    (LaPToP.ProgramTheory.Spec.cond
      (fun s =>
        s
            LaPToP.ProgramTheory.Examples.V.x =
          0)
      (fun s s' =>
        s'
            LaPToP.ProgramTheory.Examples.V.x =
          s
            LaPToP.ProgramTheory.Examples.V.x)
      fun s s' =>
      s'
          LaPToP.ProgramTheory.Examples.V.x <
        s
          LaPToP.ProgramTheory.Examples.V.x)

`x′≤x ⇐ if x=0 then x′=x else x′<x`.

theoremdefined in LaPToP/ProgramTheory/Specifications.lean

complete

theorem LaPToP.ProgramTheory.Examples.refine₄ :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s' LaPToP.ProgramTheory.Examples.V.x >
          s' LaPToP.ProgramTheory.Examples.V.y ∧
        s' LaPToP.ProgramTheory.Examples.V.y >
          s LaPToP.ProgramTheory.Examples.V.x)
    ((LaPToP.ProgramTheory.Spec.assign LaPToP.ProgramTheory.Examples.V.y
          fun s => s LaPToP.ProgramTheory.Examples.V.x + 1).seq
      (LaPToP.ProgramTheory.Spec.assign
        LaPToP.ProgramTheory.Examples.V.x fun s =>
        s LaPToP.ProgramTheory.Examples.V.y + 1))

theorem LaPToP.ProgramTheory.Examples.refine₄ :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s'
            LaPToP.ProgramTheory.Examples.V.x >
          s'
            LaPToP.ProgramTheory.Examples.V.y ∧
        s'
            LaPToP.ProgramTheory.Examples.V.y >
          s
            LaPToP.ProgramTheory.Examples.V.x)
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.Examples.V.y
          fun s =>
          s
              LaPToP.ProgramTheory.Examples.V.x +
            1).seq
      (LaPToP.ProgramTheory.Spec.assign
        LaPToP.ProgramTheory.Examples.V.x
        fun s =>
        s
            LaPToP.ProgramTheory.Examples.V.y +
          1))

`x′>y′>x ⇐ y:= x+1. x:= y+1`.

Proof for Theorem 5.10

uses 0

Unfold and decide by linear integer arithmetic; the counterexample for x \ge 0 \land y' = 0 is the prestate with x = -1.

Definition5.11

Group member previews

Preview

Definition 5.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 5.13

Loading preview

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

✓L∃∀N

"A program is a specification of computer behavior; ... a program is an implemented specification, that is, a specification for which an implementation has been provided, so that a computer can execute it." The programming notations of Chapter 4: (a) \mathit{ok} is a program; (b) x := e is a program for an implemented expression e of the initial values; (c) \mathbf{if}\ b\ \mathbf{then}\ P\ \mathbf{else}\ Q is a program for implemented b and programs P, Q; (d) P.\ Q is a program for programs P, Q; (e) an implementable specification that is refined by a program is a program. In Lean, Spec.IsProgram is the inductive predicate with exactly these five rules; every program is implementable. Two notes: the "implemented expression" restriction on e and b is about the expression language and has no counterpart in this semantic model; and the implementability hypothesis of rule (e) is redundant, since a specification refined by an implementable one is implementable. Uses Definition 5.2 and Theorem 5.4.

Lean code for Definition5.11●4 declarations

inductive(5 constructors, Prop, 4 parameters)defined in LaPToP/ProgramTheory/Programs.lean

complete

inductive LaPToP.ProgramTheory.Spec.IsProgram.{u, v} {Var : Type u} {Val : Type v}
  [DecidableEq Var] :
  LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val) →
    Prop

inductive LaPToP.ProgramTheory.Spec.IsProgram.{u, v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] :
  LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val) →
    Prop

"A program is an implemented specification": (a) `ok` is a program;
(b) `x:= e` is a program; (c) `if b then P else Q` is a program when `P`, `Q`
are; (d) `P. Q` is a program when `P`, `Q` are; (e) an implementable
specification that is refined by a program is a program.

Constructors

LaPToP.ProgramTheory.Spec.IsProgram.ok.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] :
  LaPToP.ProgramTheory.Spec.ok.IsProgram

(a) `ok` is a program.

LaPToP.ProgramTheory.Spec.IsProgram.assign.{u, v}
  {Var : Type u} {Val : Type v} [DecidableEq Var] (x : Var)
  (e : LaPToP.ProgramTheory.Spec.State Var Val → Val) :
  (LaPToP.ProgramTheory.Spec.assign x e).IsProgram

(b) `x:= e` is a program.

LaPToP.ProgramTheory.Spec.IsProgram.cond.{u, v}
  {Var : Type u} {Val : Type v} [DecidableEq Var]
  (b : LaPToP.ProgramTheory.Spec.State Var Val → Prop)
  {P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)} :
  P.IsProgram →
    Q.IsProgram →
      (LaPToP.ProgramTheory.Spec.cond b P Q).IsProgram

(c) `if b then P else Q` is a program when `P` and `Q` are.

LaPToP.ProgramTheory.Spec.IsProgram.seq.{u, v}
  {Var : Type u} {Val : Type v} [DecidableEq Var]
  {P Q :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)} :
  P.IsProgram → Q.IsProgram → (P.seq Q).IsProgram

(d) `P. Q` is a program when `P` and `Q` are.

LaPToP.ProgramTheory.Spec.IsProgram.refine.{u, v}
  {Var : Type u} {Val : Type v} [DecidableEq Var]
  {P S :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var Val)} :
  P.Implementable → P.Refines S → S.IsProgram → P.IsProgram

(e) an implementable specification refined by a program is a program.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.IsProgram.implementable.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var]
  {P :
    LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val)}
  (h : P.IsProgram) : P.Implementable

theorem LaPToP.ProgramTheory.Spec.IsProgram.implementable.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var]
  {P :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)}
  (h : P.IsProgram) : P.Implementable

Every program is implementable: "a computer can execute it".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.IsProgram.refine'.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var]
  {P S :
    LaPToP.ProgramTheory.Spec (LaPToP.ProgramTheory.Spec.State Var Val)}
  (h : P.Refines S) (hS : S.IsProgram) : P.IsProgram

theorem LaPToP.ProgramTheory.Spec.IsProgram.refine'.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var]
  {P S :
    LaPToP.ProgramTheory.Spec
      (LaPToP.ProgramTheory.Spec.State Var
        Val)}
  (h : P.Refines S) (hS : S.IsProgram) :
  P.IsProgram

Rule (e) without its implementability hypothesis, which is redundant: a
specification refined by a program is implementable.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.IsProgram.top.{u, v} {Var : Type u}
  {Val : Type v} [DecidableEq Var] :
  LaPToP.ProgramTheory.Spec.top.IsProgram

theorem LaPToP.ProgramTheory.Spec.IsProgram.top.{u,
    v}
  {Var : Type u} {Val : Type v}
  [DecidableEq Var] :
  LaPToP.ProgramTheory.Spec.top.IsProgram

`⊤` is a program (it is refined by `ok`).

Theorem5.12

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 5.7

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Theorem 5.13

Loading preview

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

✓L∃∀N

EffortsmallTagsprogramsrefinementhehner-4.1.0

The Refinement Laws of Section 4.1.0. Refinement by Steps (monotonicity, transitivity): if A \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ C\ \mathbf{else}\ D, C \Leftarrow E and D \Leftarrow F then A \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ E\ \mathbf{else}\ F; if A \Leftarrow B.\ C, B \Leftarrow D, C \Leftarrow E then A \Leftarrow D.\ E; if A \Leftarrow B, B \Leftarrow C then A \Leftarrow C. Refinement by Parts (monotonicity, conflation): if A \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ C\ \mathbf{else}\ D and E \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ F\ \mathbf{else}\ G then A \land E \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ C \land F\ \mathbf{else}\ D \land G; if A \Leftarrow B.\ C and D \Leftarrow E.\ F then A \land D \Leftarrow (B \land E).\ (C \land F); if A \Leftarrow B and C \Leftarrow D then A \land C \Leftarrow B \land D. Refinement by Cases: P \Leftarrow \mathbf{if}\ b\ \mathbf{then}\ Q\ \mathbf{else}\ R is a theorem if and only if P \Leftarrow b \land Q and P \Leftarrow \neg b \land R are theorems — illustrated on x' \le x \Leftarrow \mathbf{if}\ x = 0\ \mathbf{then}\ x' = x\ \mathbf{else}\ x' < x. The laws rest on monotonicity of \mathbf{if}, . and \land with respect to refinement. Uses Theorem 5.9 and Theorem 5.7.

Lean code for Theorem5.12●13 theorems

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_cond_mono.{u} {σ : Type u}
  {C D E F : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop)
  (h₁ : C.Refines E) (h₂ : D.Refines F) :
  (LaPToP.ProgramTheory.Spec.cond b C D).Refines
    (LaPToP.ProgramTheory.Spec.cond b E F)

theorem LaPToP.ProgramTheory.Spec.refines_cond_mono.{u}
  {σ : Type u}
  {C D E F : LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop) (h₁ : C.Refines E)
  (h₂ : D.Refines F) :
  (LaPToP.ProgramTheory.Spec.cond b C
        D).Refines
    (LaPToP.ProgramTheory.Spec.cond b E F)

`if` is monotonic in both branches.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_seq_mono.{u} {σ : Type u}
  {B C D E : LaPToP.ProgramTheory.Spec σ} (h₁ : B.Refines D)
  (h₂ : C.Refines E) : (B.seq C).Refines (D.seq E)

theorem LaPToP.ProgramTheory.Spec.refines_seq_mono.{u}
  {σ : Type u}
  {B C D E : LaPToP.ProgramTheory.Spec σ}
  (h₁ : B.Refines D) (h₂ : C.Refines E) :
  (B.seq C).Refines (D.seq E)

Sequential composition is monotonic in both operands.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_and_mono.{u} {σ : Type u}
  {A B C D : LaPToP.ProgramTheory.Spec σ} (h₁ : A.Refines B)
  (h₂ : C.Refines D) : (A.and C).Refines (B.and D)

theorem LaPToP.ProgramTheory.Spec.refines_and_mono.{u}
  {σ : Type u}
  {A B C D : LaPToP.ProgramTheory.Spec σ}
  (h₁ : A.Refines B) (h₂ : C.Refines D) :
  (A.and C).Refines (B.and D)

Conjunction is monotonic in both operands.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.steps_cond.{u} {σ : Type u}
  {A C D E F : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop)
  (hA : A.Refines (LaPToP.ProgramTheory.Spec.cond b C D))
  (hC : C.Refines E) (hD : D.Refines F) :
  A.Refines (LaPToP.ProgramTheory.Spec.cond b E F)

theorem LaPToP.ProgramTheory.Spec.steps_cond.{u}
  {σ : Type u}
  {A C D E F :
    LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop)
  (hA :
    A.Refines
      (LaPToP.ProgramTheory.Spec.cond b C
        D))
  (hC : C.Refines E) (hD : D.Refines F) :
  A.Refines
    (LaPToP.ProgramTheory.Spec.cond b E F)

Refinement by Steps: "if `A ⇐ if b then C else D` and `C ⇐ E` and `D ⇐ F`
are theorems, then `A ⇐ if b then E else F` is a theorem".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.steps_seq.{u} {σ : Type u}
  {A B C D E : LaPToP.ProgramTheory.Spec σ} (hA : A.Refines (B.seq C))
  (hB : B.Refines D) (hC : C.Refines E) : A.Refines (D.seq E)

theorem LaPToP.ProgramTheory.Spec.steps_seq.{u}
  {σ : Type u}
  {A B C D E :
    LaPToP.ProgramTheory.Spec σ}
  (hA : A.Refines (B.seq C))
  (hB : B.Refines D) (hC : C.Refines E) :
  A.Refines (D.seq E)

Refinement by Steps: "if `A ⇐ B. C` and `B ⇐ D` and `C ⇐ E` are theorems,
then `A ⇐ D. E` is a theorem".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.steps_trans.{u} {σ : Type u}
  {A B C : LaPToP.ProgramTheory.Spec σ} (hA : A.Refines B)
  (hB : B.Refines C) : A.Refines C

theorem LaPToP.ProgramTheory.Spec.steps_trans.{u}
  {σ : Type u}
  {A B C : LaPToP.ProgramTheory.Spec σ}
  (hA : A.Refines B) (hB : B.Refines C) :
  A.Refines C

Refinement by Steps: "if `A ⇐ B` and `B ⇐ C` are theorems, then `A ⇐ C` is
a theorem" (transitivity).

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.cond_and_cond_refines.{u} {σ : Type u}
  {C D F G : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop) :
  ((LaPToP.ProgramTheory.Spec.cond b C D).and
        (LaPToP.ProgramTheory.Spec.cond b F G)).Refines
    (LaPToP.ProgramTheory.Spec.cond b (C.and F) (D.and G))

theorem LaPToP.ProgramTheory.Spec.cond_and_cond_refines.{u}
  {σ : Type u}
  {C D F G : LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop) :
  ((LaPToP.ProgramTheory.Spec.cond b C
            D).and
        (LaPToP.ProgramTheory.Spec.cond b
          F G)).Refines
    (LaPToP.ProgramTheory.Spec.cond b
      (C.and F) (D.and G))

`if b then C∧F else D∧G` refines `(if b then C else D) ∧ (if b then F else G)`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.parts_cond.{u} {σ : Type u}
  {A C D E F G : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop)
  (hA : A.Refines (LaPToP.ProgramTheory.Spec.cond b C D))
  (hE : E.Refines (LaPToP.ProgramTheory.Spec.cond b F G)) :
  (A.and E).Refines
    (LaPToP.ProgramTheory.Spec.cond b (C.and F) (D.and G))

theorem LaPToP.ProgramTheory.Spec.parts_cond.{u}
  {σ : Type u}
  {A C D E F G :
    LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop)
  (hA :
    A.Refines
      (LaPToP.ProgramTheory.Spec.cond b C
        D))
  (hE :
    E.Refines
      (LaPToP.ProgramTheory.Spec.cond b F
        G)) :
  (A.and E).Refines
    (LaPToP.ProgramTheory.Spec.cond b
      (C.and F) (D.and G))

Refinement by Parts: "if `A ⇐ if b then C else D` and `E ⇐ if b then F else G`
are theorems, then `A∧E ⇐ if b then C∧F else D∧G` is a theorem".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.seq_and_seq_refines.{u} {σ : Type u}
  {B C E F : LaPToP.ProgramTheory.Spec σ} :
  ((B.seq C).and (E.seq F)).Refines ((B.and E).seq (C.and F))

theorem LaPToP.ProgramTheory.Spec.seq_and_seq_refines.{u}
  {σ : Type u}
  {B C E F :
    LaPToP.ProgramTheory.Spec σ} :
  ((B.seq C).and (E.seq F)).Refines
    ((B.and E).seq (C.and F))

`(B∧E). (C∧F)` refines `(B. C) ∧ (E. F)`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.parts_seq.{u} {σ : Type u}
  {A B C D E F : LaPToP.ProgramTheory.Spec σ} (hA : A.Refines (B.seq C))
  (hD : D.Refines (E.seq F)) :
  (A.and D).Refines ((B.and E).seq (C.and F))

theorem LaPToP.ProgramTheory.Spec.parts_seq.{u}
  {σ : Type u}
  {A B C D E F :
    LaPToP.ProgramTheory.Spec σ}
  (hA : A.Refines (B.seq C))
  (hD : D.Refines (E.seq F)) :
  (A.and D).Refines
    ((B.and E).seq (C.and F))

Refinement by Parts: "if `A ⇐ B. C` and `D ⇐ E. F` are theorems, then
`A∧D ⇐ B∧E. C∧F` is a theorem".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.parts_and.{u} {σ : Type u}
  {A B C D : LaPToP.ProgramTheory.Spec σ} (hA : A.Refines B)
  (hC : C.Refines D) : (A.and C).Refines (B.and D)

theorem LaPToP.ProgramTheory.Spec.parts_and.{u}
  {σ : Type u}
  {A B C D : LaPToP.ProgramTheory.Spec σ}
  (hA : A.Refines B) (hC : C.Refines D) :
  (A.and C).Refines (B.and D)

Refinement by Parts: "if `A ⇐ B` and `C ⇐ D` are theorems, then `A∧C ⇐ B∧D`
is a theorem" (conflation).

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Spec.refines_cond_iff.{u} {σ : Type u}
  {P Q R : LaPToP.ProgramTheory.Spec σ} (b : σ → Prop) :
  P.Refines (LaPToP.ProgramTheory.Spec.cond b Q R) ↔
    P.Refines (LaPToP.ProgramTheory.Spec.and (fun s x => b s) Q) ∧
      P.Refines (LaPToP.ProgramTheory.Spec.and (fun s x => ¬b s) R)

theorem LaPToP.ProgramTheory.Spec.refines_cond_iff.{u}
  {σ : Type u}
  {P Q R : LaPToP.ProgramTheory.Spec σ}
  (b : σ → Prop) :
  P.Refines
      (LaPToP.ProgramTheory.Spec.cond b Q
        R) ↔
    P.Refines
        (LaPToP.ProgramTheory.Spec.and
          (fun s x => b s) Q) ∧
      P.Refines
        (LaPToP.ProgramTheory.Spec.and
          (fun s x => ¬b s) R)

Refinement by Cases: "`P ⇐ if b then Q else R` is a theorem if and only if
`P ⇐ b ∧ Q` and `P ⇐ ¬b ∧ R` are theorems".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.Examples.refine₃_by_cases :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s' LaPToP.ProgramTheory.Examples.V.x ≤
        s LaPToP.ProgramTheory.Examples.V.x)
    (LaPToP.ProgramTheory.Spec.cond
      (fun s => s LaPToP.ProgramTheory.Examples.V.x = 0)
      (fun s s' =>
        s' LaPToP.ProgramTheory.Examples.V.x =
          s LaPToP.ProgramTheory.Examples.V.x)
      fun s s' =>
      s' LaPToP.ProgramTheory.Examples.V.x <
        s LaPToP.ProgramTheory.Examples.V.x)

theorem LaPToP.ProgramTheory.Examples.refine₃_by_cases :
  LaPToP.ProgramTheory.Spec.Refines
    (fun s s' =>
      s'
          LaPToP.ProgramTheory.Examples.V.x ≤
        s
          LaPToP.ProgramTheory.Examples.V.x)
    (LaPToP.ProgramTheory.Spec.cond
      (fun s =>
        s
            LaPToP.ProgramTheory.Examples.V.x =
          0)
      (fun s s' =>
        s'
            LaPToP.ProgramTheory.Examples.V.x =
          s
            LaPToP.ProgramTheory.Examples.V.x)
      fun s s' =>
      s'
          LaPToP.ProgramTheory.Examples.V.x <
        s
          LaPToP.ProgramTheory.Examples.V.x)

`x′≤x ⇐ if x=0 then x′=x else x′<x` proved by Refinement by Cases, from
`x′≤x ⇐ x=0 ∧ x′=x` and `x′≤x ⇐ x⧧0 ∧ x′<x`.

Proof for Theorem 5.12

uses 0

Monotonicity by unfolding; Steps is monotonicity followed by transitivity; Parts additionally uses that \mathbf{if}\ b\ \mathbf{then}\ C \land F\ \mathbf{else}\ D \land G refines (\mathbf{if}\ b\ \mathbf{then}\ C\ \mathbf{else}\ D) \land (\mathbf{if}\ b\ \mathbf{then}\ F\ \mathbf{else}\ G) and that (B \land E).\ (C \land F) refines (B.\ C) \land (E.\ F); Cases by splitting the disjunction in \mathbf{if}.

Theorem5.13

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 5

Statement dependency previews

Preview

Definition 3.8

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 5.15

Loading preview

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

✓L∃∀N

EffortmediumTagsprogramsdevelopmenthehner-4.1.1

The book's first program development (Exercise 174): "write a program to find the sum of a list of numbers". With L the list (a state constant), s the accumulator and n the number of items summed, the problem s' = \Sigma L is refined in four steps: s' = \Sigma L \Leftarrow s := 0.\ n := 0.\ B where B = (s' = s + \Sigma L[n;..\# L]); B \Leftarrow \mathbf{if}\ n = \# L\ \mathbf{then}\ C\ \mathbf{else}\ D (Case Creation) with C = (n = \# L \Rightarrow B), D = (n \neq \# L \Rightarrow B); C \Leftarrow \mathit{ok}; and D \Leftarrow s := s + L\,n.\ n := n + 1.\ B, "proved by two applications of the Substitution Law". Refinement by Steps then assembles the compiler's view B \Leftarrow \mathbf{if}\ n = \# L\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ (s := s + L\,n.\ n := n + 1.\ B) and the whole development. The book's implicit bound 0 \le n \le \# L ("the notation n;..\# L is defined only for n \le \# L") is made explicit in B, as the book itself suggests. The last refinement refers to B again — a recursive call, which is not a program in the sense of Definition 5.11 until execution time and termination (Section 4.2) and recursion (Chapter 6) are treated; A and B are shown implementable so that rule (e) applies once they are. Uses Theorem 5.12, Theorem 5.8, Theorem 3.16 and Definition 3.8.

Lean code for Theorem5.13●19 declarations

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

complete

inductive LaPToP.ProgramTheory.ListSummation.SV : Type

inductive LaPToP.ProgramTheory.ListSummation.SV :
  Type

The state variables: `s`, the sum so far, and `n`, the number of items summed.

Constructors

LaPToP.ProgramTheory.ListSummation.SV.s :
  LaPToP.ProgramTheory.ListSummation.SV

The accumulator `s`.

LaPToP.ProgramTheory.ListSummation.SV.n :
  LaPToP.ProgramTheory.ListSummation.SV

The index `n`.

abbrevdefined in LaPToP/ProgramTheory/Programs.lean

complete

abbrev LaPToP.ProgramTheory.ListSummation.St : Type

abbrev LaPToP.ProgramTheory.ListSummation.St :
  Type

States over the two integer variables `s` and `n`.

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.len
  (L : LaPToP.DataStructures.HList ℤ) : ℤ

def LaPToP.ProgramTheory.ListSummation.len
  (L : LaPToP.DataStructures.HList ℤ) : ℤ

`#L`, the length of the list, as an integer.

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.sumFrom
  (L : LaPToP.DataStructures.HList ℤ) (n : ℤ) : ℤ

def LaPToP.ProgramTheory.ListSummation.sumFrom
  (L : LaPToP.DataStructures.HList ℤ)
  (n : ℤ) : ℤ

`Σ L [n;..#L]`, the sum of the items of `L` from index `n` on.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_zero
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.ListSummation.sumFrom L 0 = List.sum L.contents

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_zero
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.ListSummation.sumFrom
      L 0 =
    List.sum L.contents

`Σ L [0;..#L] = ΣL`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_len
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.ListSummation.sumFrom L
      (LaPToP.ProgramTheory.ListSummation.len L) =
    0

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_len
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.ListSummation.sumFrom
      L
      (LaPToP.ProgramTheory.ListSummation.len
        L) =
    0

`Σ L [#L;..#L] = 0`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_succ
  (L : LaPToP.DataStructures.HList ℤ) {n : ℤ} (h0 : 0 ≤ n)
  (hn : n < LaPToP.ProgramTheory.ListSummation.len L) :
  LaPToP.ProgramTheory.ListSummation.sumFrom L n =
    L.at n.toNat + LaPToP.ProgramTheory.ListSummation.sumFrom L (n + 1)

theorem LaPToP.ProgramTheory.ListSummation.sumFrom_succ
  (L : LaPToP.DataStructures.HList ℤ)
  {n : ℤ} (h0 : 0 ≤ n)
  (hn :
    n <
      LaPToP.ProgramTheory.ListSummation.len
        L) :
  LaPToP.ProgramTheory.ListSummation.sumFrom
      L n =
    L.at n.toNat +
      LaPToP.ProgramTheory.ListSummation.sumFrom
        L (n + 1)

`Σ L [n;..#L] = L n + Σ L [n+1;..#L]` for `0 ≤ n < #L`.

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.A
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ListSummation.St

def LaPToP.ProgramTheory.ListSummation.A
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ListSummation.St

The problem: `s′ = ΣL`.

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.B
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ListSummation.St

def LaPToP.ProgramTheory.ListSummation.B
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ListSummation.St

`0 ≤ n ≤ #L ⇒ s′ = s + Σ L [n;..#L]`: `n` items have been summed and the
rest remain to be summed (with the book's implicit bound on `n` made explicit).

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.C
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ListSummation.St

def LaPToP.ProgramTheory.ListSummation.C
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ListSummation.St

`n=#L ⇒ B`.

defdefined in LaPToP/ProgramTheory/Programs.lean

complete

def LaPToP.ProgramTheory.ListSummation.D
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.ListSummation.St

def LaPToP.ProgramTheory.ListSummation.D
  (L : LaPToP.DataStructures.HList ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.ListSummation.St

`n⧧#L ⇒ B`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_A
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s fun x => 0).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n fun x => 0).seq
        (LaPToP.ProgramTheory.ListSummation.B L)))

theorem LaPToP.ProgramTheory.ListSummation.refine_A
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A
        L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s
          fun x => 0).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n
            fun x => 0).seq
        (LaPToP.ProgramTheory.ListSummation.B
          L)))

`s′ = ΣL ⇐ s:= 0. n:= 0. B`: "we must begin by assigning 0 to both `s` and
`n` ... we complete the task by adding the remaining items". Proved "by two
applications of the Substitution Law".

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_B
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B L).Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun st =>
        st LaPToP.ProgramTheory.ListSummation.SV.n =
          LaPToP.ProgramTheory.ListSummation.len L)
      (LaPToP.ProgramTheory.ListSummation.C L)
      (LaPToP.ProgramTheory.ListSummation.D L))

theorem LaPToP.ProgramTheory.ListSummation.refine_B
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B
        L).Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun st =>
        st
            LaPToP.ProgramTheory.ListSummation.SV.n =
          LaPToP.ProgramTheory.ListSummation.len
            L)
      (LaPToP.ProgramTheory.ListSummation.C
        L)
      (LaPToP.ProgramTheory.ListSummation.D
        L))

`B ⇐ if n=#L then C else D` (Case Creation).

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_C
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.C L).Refines
    LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.ListSummation.refine_C
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.C
        L).Refines
    LaPToP.ProgramTheory.Spec.ok

`C ⇐ ok`: "one is trivial" — all items have been summed.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_D
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.D L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s fun st =>
          st LaPToP.ProgramTheory.ListSummation.SV.s +
            L.at (st LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n fun st =>
            st LaPToP.ProgramTheory.ListSummation.SV.n + 1).seq
        (LaPToP.ProgramTheory.ListSummation.B L)))

theorem LaPToP.ProgramTheory.ListSummation.refine_D
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.D
        L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s
          fun st =>
          st
              LaPToP.ProgramTheory.ListSummation.SV.s +
            L.at
              (st
                  LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n
            fun st =>
            st
                LaPToP.ProgramTheory.ListSummation.SV.n +
              1).seq
        (LaPToP.ProgramTheory.ListSummation.B
          L)))

`D ⇐ s:= s + L n. n:= n+1. B`: "let us add one more item to the sum. To
complete the refinement, we must also add any remaining items." Proved "by two
applications of the Substitution Law". The right side refers to `B` again: a
recursive call.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_B_expanded
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B L).Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun st =>
        st LaPToP.ProgramTheory.ListSummation.SV.n =
          LaPToP.ProgramTheory.ListSummation.len L)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.s fun st =>
            st LaPToP.ProgramTheory.ListSummation.SV.s +
              L.at
                (st LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
        ((LaPToP.ProgramTheory.Spec.assign
              LaPToP.ProgramTheory.ListSummation.SV.n fun st =>
              st LaPToP.ProgramTheory.ListSummation.SV.n + 1).seq
          (LaPToP.ProgramTheory.ListSummation.B L))))

theorem LaPToP.ProgramTheory.ListSummation.refine_B_expanded
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B
        L).Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun st =>
        st
            LaPToP.ProgramTheory.ListSummation.SV.n =
          LaPToP.ProgramTheory.ListSummation.len
            L)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.s
            fun st =>
            st
                LaPToP.ProgramTheory.ListSummation.SV.s +
              L.at
                (st
                    LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
        ((LaPToP.ProgramTheory.Spec.assign
              LaPToP.ProgramTheory.ListSummation.SV.n
              fun st =>
              st
                  LaPToP.ProgramTheory.ListSummation.SV.n +
                1).seq
          (LaPToP.ProgramTheory.ListSummation.B
            L))))

The compiler's view, after macro-expanding `C` and `D` by Refinement by
Steps: `B ⇐ if n=#L then ok else s:= s + L n. n:= n+1. B`.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.refine_A_expanded
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s fun x => 0).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n fun x => 0).seq
        (LaPToP.ProgramTheory.Spec.cond
          (fun st =>
            st LaPToP.ProgramTheory.ListSummation.SV.n =
              LaPToP.ProgramTheory.ListSummation.len L)
          LaPToP.ProgramTheory.Spec.ok
          ((LaPToP.ProgramTheory.Spec.assign
                LaPToP.ProgramTheory.ListSummation.SV.s fun st =>
                st LaPToP.ProgramTheory.ListSummation.SV.s +
                  L.at
                    (st
                        LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
            ((LaPToP.ProgramTheory.Spec.assign
                  LaPToP.ProgramTheory.ListSummation.SV.n fun st =>
                  st LaPToP.ProgramTheory.ListSummation.SV.n + 1).seq
              (LaPToP.ProgramTheory.ListSummation.B L))))))

theorem LaPToP.ProgramTheory.ListSummation.refine_A_expanded
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A
        L).Refines
    ((LaPToP.ProgramTheory.Spec.assign
          LaPToP.ProgramTheory.ListSummation.SV.s
          fun x => 0).seq
      ((LaPToP.ProgramTheory.Spec.assign
            LaPToP.ProgramTheory.ListSummation.SV.n
            fun x => 0).seq
        (LaPToP.ProgramTheory.Spec.cond
          (fun st =>
            st
                LaPToP.ProgramTheory.ListSummation.SV.n =
              LaPToP.ProgramTheory.ListSummation.len
                L)
          LaPToP.ProgramTheory.Spec.ok
          ((LaPToP.ProgramTheory.Spec.assign
                LaPToP.ProgramTheory.ListSummation.SV.s
                fun st =>
                st
                    LaPToP.ProgramTheory.ListSummation.SV.s +
                  L.at
                    (st
                        LaPToP.ProgramTheory.ListSummation.SV.n).toNat).seq
            ((LaPToP.ProgramTheory.Spec.assign
                  LaPToP.ProgramTheory.ListSummation.SV.n
                  fun st =>
                  st
                      LaPToP.ProgramTheory.ListSummation.SV.n +
                    1).seq
              (LaPToP.ProgramTheory.ListSummation.B
                L))))))

`s′ = ΣL ⇐ s:= 0. n:= 0. if n=#L then ok else (s:= s + L n. n:= n+1. B)`,
the whole development assembled by Refinement by Steps.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.implementable_A
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A L).Implementable

theorem LaPToP.ProgramTheory.ListSummation.implementable_A
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.A
      L).Implementable

`A` is implementable.

theoremdefined in LaPToP/ProgramTheory/Programs.lean

complete

theorem LaPToP.ProgramTheory.ListSummation.implementable_B
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B L).Implementable

theorem LaPToP.ProgramTheory.ListSummation.implementable_B
  (L : LaPToP.DataStructures.HList ℤ) :
  (LaPToP.ProgramTheory.ListSummation.B
      L).Implementable

The specifications `A`, `B`, `C`, `D` are implementable (so rule (e) may
be applied to them once their solutions are programs).

Proof for Theorem 5.13

uses 0

Each step by the Substitution Law (assign_seq) and the list facts \Sigma L[0;..\# L] = \Sigma L, \Sigma L[\# L;..\# L] = 0, and \Sigma L[n;..\# L] = L\,n + \Sigma L[n+1;..\# L] for 0 \le n < \# L.

Definition5.14

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 2.9

Loading preview

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

Used by 8

Reverse dependency previews

Preview

Theorem 5.15

Loading preview

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

✓L∃∀N

"To talk about time, we just add a time variable. We do not change the theory; the time variable is treated just like any other variable, as part of the state." The state \sigma = t; x; y; \ldots has a time variable t (initial time) and t' is the final time; "to allow for nontermination we take the domain of time to be a number system extended with \infty". In Lean the book's example state is a structure with t : \mathit{xnat} (as ℕ∞, cf. Definition 2.9) and one integer variable x; since t and x have different types, assignments x := e and t := e are the relations assignX, assignT (in particular tick is t := t+1), each obeying the Substitution Law of Theorem 5.8. "Time cannot decrease, therefore a specification S with time is implementable if and only if \forall\sigma\cdot\exists\sigma'\cdot S \land t' \ge t": ImplementableT, which holds for \mathit{ok}, x := e, t := t+1 and is preserved by \mathbf{if} and .. Extends Definition 5.2 and Theorem 5.4.

Lean code for Definition5.14●15 declarations

structure(2 fields)defined in LaPToP/ProgramTheory/Time.lean

complete

structure LaPToP.ProgramTheory.Time.TSt : Type

structure LaPToP.ProgramTheory.Time.TSt : Type

A state with a time variable `t` (an extended natural, `∞ = ⊤`) and one
integer memory variable `x`: the book's `σ = t; x`.

Fields

t : ℕ∞

The time variable.

x : ℤ

The memory variable `x`.

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.assignX
  (e : LaPToP.ProgramTheory.Time.TSt → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.assignX
  (e :
    LaPToP.ProgramTheory.Time.TSt → ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

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

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.assignT
  (e : LaPToP.ProgramTheory.Time.TSt → ℕ∞) :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.assignT
  (e :
    LaPToP.ProgramTheory.Time.TSt → ℕ∞) :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

`t:= e`, for `e` an expression of the initial state. "Assignments to the
time variable are not executed; they are there for reasoning about time."

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.tick :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.tick :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

`t:= t+1`, one unit of time.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

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

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

The Substitution Law for `x:= e`: `x:= e. P = (substitute e for x in P)`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.assignT_seq
  (e : LaPToP.ProgramTheory.Time.TSt → ℕ∞)
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt) :
  (LaPToP.ProgramTheory.Time.assignT e).seq P = fun s s' =>
    P { t := e s, x := s.x } s'

theorem LaPToP.ProgramTheory.Time.assignT_seq
  (e : LaPToP.ProgramTheory.Time.TSt → ℕ∞)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt) :
  (LaPToP.ProgramTheory.Time.assignT
          e).seq
      P =
    fun s s' =>
    P { t := e s, x := s.x } s'

The Substitution Law for `t:= e`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.tick_seq
  (P : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt) :
  LaPToP.ProgramTheory.Time.tick.seq P = fun s s' =>
    P { t := s.t + 1, x := s.x } s'

theorem LaPToP.ProgramTheory.Time.tick_seq
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt) :
  LaPToP.ProgramTheory.Time.tick.seq P =
    fun s s' =>
    P { t := s.t + 1, x := s.x } s'

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

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.ImplementableT
  (S : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt) : Prop

def LaPToP.ProgramTheory.Time.ImplementableT
  (S :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt) :
  Prop

"A specification `S` with time is implementable if and only if
`∀σ· ∃σ′· S ∧ t′ ≥ t`": for each initial state there is a satisfactory final
state in which time has not decreased.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_iff
  (S : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt) :
  LaPToP.ProgramTheory.Time.ImplementableT S ↔
    (S.and fun s s' => s.t ≤ s'.t).Implementable

theorem LaPToP.ProgramTheory.Time.implementableT_iff
  (S :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt) :
  LaPToP.ProgramTheory.Time.ImplementableT
      S ↔
    (S.and fun s s' =>
        s.t ≤ s'.t).Implementable

Implementability with time is implementability of `S ∧ t′ ≥ t`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.ImplementableT.implementable
  {S : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt}
  (h : LaPToP.ProgramTheory.Time.ImplementableT S) : S.Implementable

theorem LaPToP.ProgramTheory.Time.ImplementableT.implementable
  {S :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt}
  (h :
    LaPToP.ProgramTheory.Time.ImplementableT
      S) :
  S.Implementable

Implementable with time implies implementable.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_ok :
  LaPToP.ProgramTheory.Time.ImplementableT LaPToP.ProgramTheory.Spec.ok

theorem LaPToP.ProgramTheory.Time.implementableT_ok :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Spec.ok

`ok` is implementable with time.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_assignX
  (e : LaPToP.ProgramTheory.Time.TSt → ℤ) :
  LaPToP.ProgramTheory.Time.ImplementableT
    (LaPToP.ProgramTheory.Time.assignX e)

theorem LaPToP.ProgramTheory.Time.implementableT_assignX
  (e :
    LaPToP.ProgramTheory.Time.TSt → ℤ) :
  LaPToP.ProgramTheory.Time.ImplementableT
    (LaPToP.ProgramTheory.Time.assignX e)

`x:= e` is implementable with time.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_tick :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.tick

theorem LaPToP.ProgramTheory.Time.implementableT_tick :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.tick

`t:= t+1` is implementable with time.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_cond
  (b : LaPToP.ProgramTheory.Time.TSt → Prop)
  {P Q : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt}
  (hP : LaPToP.ProgramTheory.Time.ImplementableT P)
  (hQ : LaPToP.ProgramTheory.Time.ImplementableT Q) :
  LaPToP.ProgramTheory.Time.ImplementableT
    (LaPToP.ProgramTheory.Spec.cond b P Q)

theorem LaPToP.ProgramTheory.Time.implementableT_cond
  (b :
    LaPToP.ProgramTheory.Time.TSt → Prop)
  {P Q :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt}
  (hP :
    LaPToP.ProgramTheory.Time.ImplementableT
      P)
  (hQ :
    LaPToP.ProgramTheory.Time.ImplementableT
      Q) :
  LaPToP.ProgramTheory.Time.ImplementableT
    (LaPToP.ProgramTheory.Spec.cond b P Q)

`if b then P else Q` is implementable with time when `P`, `Q` are.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_seq
  {P Q : LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt}
  (hP : LaPToP.ProgramTheory.Time.ImplementableT P)
  (hQ : LaPToP.ProgramTheory.Time.ImplementableT Q) :
  LaPToP.ProgramTheory.Time.ImplementableT (P.seq Q)

theorem LaPToP.ProgramTheory.Time.implementableT_seq
  {P Q :
    LaPToP.ProgramTheory.Spec
      LaPToP.ProgramTheory.Time.TSt}
  (hP :
    LaPToP.ProgramTheory.Time.ImplementableT
      P)
  (hQ :
    LaPToP.ProgramTheory.Time.ImplementableT
      Q) :
  LaPToP.ProgramTheory.Time.ImplementableT
    (P.seq Q)

`P. Q` is implementable with time when `P`, `Q` are: time does not decrease
across the intermediate state.

Theorem5.15

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 5.11

Loading preview

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

used by 1✓L∃∀N

EffortmediumTagsprogramstimehehner-4.2

The book's example P \Leftarrow \mathbf{if}\ x = 0\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ x := x - 1.\ P with time. Recursive time ("each recursive call costs time 1; all else is free"): P \Leftarrow \mathbf{if}\ x = 0\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ x := x - 1.\ t := t + 1.\ P is a theorem for P = \mathbf{if}\ x \ge 0\ \mathbf{then}\ x' = 0 \land t' = t + x\ \mathbf{else}\ t' = \infty and for P = x' = 0 \land \mathbf{if}\ x \ge 0\ \mathbf{then}\ t' = t + x\ \mathbf{else}\ t' = \infty. Real time, with the \mathbf{if}, the assignment and the call each taking time 1: P \Leftarrow t := t+1.\ \mathbf{if}\ x = 0\ \mathbf{then}\ \mathit{ok}\ \mathbf{else}\ t := t+1.\ x := x-1.\ t := t+1.\ P is a theorem for P = \mathbf{if}\ x \ge 0\ \mathbf{then}\ x' = 0 \land t' = t + 3 \times x + 1\ \mathbf{else}\ t' = \infty — "when x starts with a nonnegative value, execution of this program sets x to 0, and takes time 3 \times x + 1 to do so; when x starts with a negative value, execution takes infinite time". (Both measures are taken in \mathit{xnat} here.) As in Theorem 5.13, the recursive call is not yet a program in the sense of Definition 5.11. Uses Definition 5.14 and Theorem 5.12.

Lean code for Theorem5.15●7 declarations

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.cast_toNat_pred_add_one {x : ℤ} (hx : 1 ≤ x) :
  ↑(x - 1).toNat + 1 = ↑x.toNat

theorem LaPToP.ProgramTheory.Time.cast_toNat_pred_add_one
  {x : ℤ} (hx : 1 ≤ x) :
  ↑(x - 1).toNat + 1 = ↑x.toNat

`(x–1).toNat + 1 = x.toNat` for `x ≥ 1`, in `ℕ∞`.

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.Prec :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.Prec :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

Recursive time: `P = if x≥0 then x′=0 ∧ t′=t+x else t′=∞`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refine_Prec :
  LaPToP.ProgramTheory.Time.Prec.Refines
    (LaPToP.ProgramTheory.Spec.cond (fun s => s.x = 0)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Time.assignX fun s => s.x - 1).seq
        (LaPToP.ProgramTheory.Time.tick.seq
          LaPToP.ProgramTheory.Time.Prec)))

theorem LaPToP.ProgramTheory.Time.refine_Prec :
  LaPToP.ProgramTheory.Time.Prec.Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun s => s.x = 0)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Time.assignX
            fun s => s.x - 1).seq
        (LaPToP.ProgramTheory.Time.tick.seq
          LaPToP.ProgramTheory.Time.Prec)))

`P ⇐ if x=0 then ok else x:= x–1. t:= t+1. P` (recursive time: "each
recursive call costs time 1; all else is free") is a theorem for
`P = if x≥0 then x′=0 ∧ t′=t+x else t′=∞`.

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.Prec' :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.Prec' :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

Recursive time, the book's second form: `P = x′=0 ∧ if x≥0 then t′=t+x else t′=∞`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refine_Prec' :
  LaPToP.ProgramTheory.Time.Prec'.Refines
    (LaPToP.ProgramTheory.Spec.cond (fun s => s.x = 0)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Time.assignX fun s => s.x - 1).seq
        (LaPToP.ProgramTheory.Time.tick.seq
          LaPToP.ProgramTheory.Time.Prec')))

theorem LaPToP.ProgramTheory.Time.refine_Prec' :
  LaPToP.ProgramTheory.Time.Prec'.Refines
    (LaPToP.ProgramTheory.Spec.cond
      (fun s => s.x = 0)
      LaPToP.ProgramTheory.Spec.ok
      ((LaPToP.ProgramTheory.Time.assignX
            fun s => s.x - 1).seq
        (LaPToP.ProgramTheory.Time.tick.seq
          LaPToP.ProgramTheory.Time.Prec')))

The same refinement is a theorem for `P = x′=0 ∧ if x≥0 then t′=t+x else t′=∞`.

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.Preal :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.Preal :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

Real time, with the `if`, the assignment and the call each taking time 1:
`P = if x≥0 then x′=0 ∧ t′ = t + 3×x + 1 else t′=∞`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refine_Preal :
  LaPToP.ProgramTheory.Time.Preal.Refines
    (LaPToP.ProgramTheory.Time.tick.seq
      (LaPToP.ProgramTheory.Spec.cond (fun s => s.x = 0)
        LaPToP.ProgramTheory.Spec.ok
        (LaPToP.ProgramTheory.Time.tick.seq
          ((LaPToP.ProgramTheory.Time.assignX fun s => s.x - 1).seq
            (LaPToP.ProgramTheory.Time.tick.seq
              LaPToP.ProgramTheory.Time.Preal)))))

theorem LaPToP.ProgramTheory.Time.refine_Preal :
  LaPToP.ProgramTheory.Time.Preal.Refines
    (LaPToP.ProgramTheory.Time.tick.seq
      (LaPToP.ProgramTheory.Spec.cond
        (fun s => s.x = 0)
        LaPToP.ProgramTheory.Spec.ok
        (LaPToP.ProgramTheory.Time.tick.seq
          ((LaPToP.ProgramTheory.Time.assignX
                fun s => s.x - 1).seq
            (LaPToP.ProgramTheory.Time.tick.seq
              LaPToP.ProgramTheory.Time.Preal)))))

`P ⇐ t:= t+1. if x=0 then ok else t:= t+1. x:= x–1. t:= t+1. P` (real
time, unit costs) is a theorem for `P = if x≥0 then x′=0 ∧ t′ = t + 3×x + 1 else t′=∞`:
"when `x` starts with a nonnegative value, execution of this program sets `x`
to 0, and takes time `3×x + 1` to do so; when `x` starts with a negative value,
execution takes infinite time".

Proof for Theorem 5.15

uses 0

Case split on x = 0; the recursive case is the Substitution Law for x := x-1 and t := t+1 followed by a case split on x - 1 \ge 0, with the \mathit{xnat} identity (x-1) + 1 = x for x \ge 1.

Theorem5.16

Group member previews

Preview

Definition 5.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 5.9

Loading preview

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

used by 0✓L∃∀N

EffortsmallTagsprogramstimehehner-4.2.2

"Here are four specifications, each of which says that variable x has final value 2": (a) x' = 2; (b) x' = 2 \land t' < \infty; (c) x' = 2 \land (t < \infty \Rightarrow t' < \infty); (d) x' = 2 \land t' \le t + 1. (a) is refined by the infinite loop x' = 2 \Leftarrow t := t+1.\ x' = 2 — "an unkind refinement, but the customer has no ground for complaint". (b) is unimplementable: "(b) \land\ t' \ge t is unsatisfiable for t = \infty", so "the programmer has to reject (b)". (c) is implementable "but surprisingly, it can be refined with exactly the same construction as (a)": x' = 2 \land (t < \infty \Rightarrow t' < \infty) \Leftarrow t := t+1.\ x' = 2 \land (t < \infty \Rightarrow t' < \infty). (d) is implementable, stronger than (c), and "an infinite loop is no longer possible because x' = 2 \land t' \le t + 1 \Leftarrow t := t+1.\ x' = 2 \land t' \le t + 1 is not a theorem". Uses Definition 5.14 and Theorem 5.9.

Lean code for Theorem5.16●12 declarations

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.specA :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.specA :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

(a) `x′=2`: "says nothing about when the final value is wanted".

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.specB :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.specB :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

(b) `x′=2 ∧ t′<∞`: "insists that the final state be delivered at a finite time".

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.specC :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.specC :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

(c) `x′=2 ∧ (t<∞ ⇒ t′<∞)`: "if the computation starts at a finite time, it
must end at a finite time".

defdefined in LaPToP/ProgramTheory/Time.lean

complete

def LaPToP.ProgramTheory.Time.specD :
  LaPToP.ProgramTheory.Spec LaPToP.ProgramTheory.Time.TSt

def LaPToP.ProgramTheory.Time.specD :
  LaPToP.ProgramTheory.Spec
    LaPToP.ProgramTheory.Time.TSt

(d) `x′=2 ∧ t′≤t+1`: "measuring time in seconds", at most one second.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refine_a :
  LaPToP.ProgramTheory.Time.specA.Refines
    (LaPToP.ProgramTheory.Time.tick.seq LaPToP.ProgramTheory.Time.specA)

theorem LaPToP.ProgramTheory.Time.refine_a :
  LaPToP.ProgramTheory.Time.specA.Refines
    (LaPToP.ProgramTheory.Time.tick.seq
      LaPToP.ProgramTheory.Time.specA)

(a) can be refined by an infinite loop: `x′=2 ⇐ t:= t+1. x′=2`. "It may be an
unkind refinement, but the customer has no ground for complaint."

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.unsatisfiable_b (x : ℤ) :
  (LaPToP.ProgramTheory.Time.specB.and fun s s' =>
        s.t ≤ s'.t).Unsatisfiable
    { t := ⊤, x := x }

theorem LaPToP.ProgramTheory.Time.unsatisfiable_b
  (x : ℤ) :
  (LaPToP.ProgramTheory.Time.specB.and
        fun s s' =>
        s.t ≤ s'.t).Unsatisfiable
    { t := ⊤, x := x }

(b) is unimplementable: "(b) ∧ t′≥t is unsatisfiable for t=∞".

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.not_implementableT_b :
  ¬LaPToP.ProgramTheory.Time.ImplementableT
      LaPToP.ProgramTheory.Time.specB

theorem LaPToP.ProgramTheory.Time.not_implementableT_b :
  ¬LaPToP.ProgramTheory.Time.ImplementableT
      LaPToP.ProgramTheory.Time.specB

Hence (b) is not implementable with time; "the programmer has to reject (b)".

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_c :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.specC

theorem LaPToP.ProgramTheory.Time.implementableT_c :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.specC

(c) is implementable.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refine_c :
  LaPToP.ProgramTheory.Time.specC.Refines
    (LaPToP.ProgramTheory.Time.tick.seq LaPToP.ProgramTheory.Time.specC)

theorem LaPToP.ProgramTheory.Time.refine_c :
  LaPToP.ProgramTheory.Time.specC.Refines
    (LaPToP.ProgramTheory.Time.tick.seq
      LaPToP.ProgramTheory.Time.specC)

(c) "can be refined with exactly the same construction as (a)":
`x′=2 ∧ (t<∞ ⇒ t′<∞) ⇐ t:= t+1. x′=2 ∧ (t<∞ ⇒ t′<∞)`.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.implementableT_d :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.specD

theorem LaPToP.ProgramTheory.Time.implementableT_d :
  LaPToP.ProgramTheory.Time.ImplementableT
    LaPToP.ProgramTheory.Time.specD

(d) is implementable.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.refines_c_d :
  LaPToP.ProgramTheory.Time.specC.Refines
    LaPToP.ProgramTheory.Time.specD

theorem LaPToP.ProgramTheory.Time.refines_c_d :
  LaPToP.ProgramTheory.Time.specC.Refines
    LaPToP.ProgramTheory.Time.specD

(d) is stronger than (c): a computation that takes at most a second ends
at a finite time if it starts at one.

theoremdefined in LaPToP/ProgramTheory/Time.lean

complete

theorem LaPToP.ProgramTheory.Time.not_refine_d :
  ¬LaPToP.ProgramTheory.Time.specD.Refines
      (LaPToP.ProgramTheory.Time.tick.seq
        LaPToP.ProgramTheory.Time.specD)

theorem LaPToP.ProgramTheory.Time.not_refine_d :
  ¬LaPToP.ProgramTheory.Time.specD.Refines
      (LaPToP.ProgramTheory.Time.tick.seq
        LaPToP.ProgramTheory.Time.specD)

For (d) "an infinite loop is no longer possible because
`x′=2 ∧ t′≤t+1 ⇐ t:= t+1. x′=2 ∧ t′≤t+1` is not a theorem".

Proof for Theorem 5.16

uses 0

Direct from the definitions; the non-theorem is refuted by the prestate t = 0, x = 0 and poststate t = 2, x = 2.