7. Recursion and Concurrency🔗

Definition7.1

Group: Recursive programs, time bounds, and concurrent composition as developed in later chapters of A Practical Theory of Programming . Recursive data definition (Section 6.0) is formalized in LaPToP.RecursiveDefinition.Nat and LaPToP.RecursiveDefinition.DataConstruction , and recursive program definition (Section 6.1) in LaPToP.RecursiveDefinition.Programs . (11)

Group member previews

Preview

Theorem 7.2

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 7.4

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Definition 7.4

Loading preview

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

✓L∃∀N

A recursive program is the least fixed point of a monotonic transformer on specifications. Termination and partial-correctness arguments are expressed in the same predicate calculus as straight-line code.

"A fixed-point of a function f is an element x of its domain such that f maps x to itself: x = f\,x. A least fixed-point of f is a smallest such x." The notions are defined generally (IsFixedPoint, IsLeastFixedPoint, unique when it exists); their use for recursive data definition is Definition 7.4, and the specification-level account of recursive programs is Theorem 7.8.

Lean code for Definition7.1●3 declarations

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.IsFixedPoint.{u} {α : Type u} (f : α → α)
  (x : α) : Prop

def LaPToP.RecursiveDefinition.IsFixedPoint.{u}
  {α : Type u} (f : α → α) (x : α) : Prop

`x` is a *fixed point* of `f`: `f x = x`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.IsLeastFixedPoint.{u} {α : Type u} [LE α]
  (f : α → α) (x : α) : Prop

def LaPToP.RecursiveDefinition.IsLeastFixedPoint.{u}
  {α : Type u} [LE α] (f : α → α)
  (x : α) : Prop

`x` is a *least fixed point* of `f`: a fixed point below every fixed point.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.IsLeastFixedPoint.unique.{u} {α : Type u}
  [PartialOrder α] {f : α → α} {x y : α}
  (hx : LaPToP.RecursiveDefinition.IsLeastFixedPoint f x)
  (hy : LaPToP.RecursiveDefinition.IsLeastFixedPoint f y) : x = y

theorem LaPToP.RecursiveDefinition.IsLeastFixedPoint.unique.{u}
  {α : Type u} [PartialOrder α]
  {f : α → α} {x y : α}
  (hx :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      f x)
  (hy :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      f y) :
  x = y

A least fixed point is unique.

Theorem7.2

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 2.11

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Theorem 7.3

Loading preview

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

✓L∃∀N

EffortsmallTagsrecursionnathehner-6.0.0

"To define \mathit{nat}, we need to say what its elements are": the construction axioms 0 : \mathit{nat}, \mathit{nat}+1 : \mathit{nat} ("0 and \mathit{nat}+1 are called the nat constructors") and the induction axiom 0, B+1 : B \Rightarrow \mathit{nat} : B ("of all these bunches, nat is the smallest"). "In predicate notation, the nat induction axiom can be stated as follows: if P : \mathit{nat} \to \mathit{bin}, P\,0 \land (\forall n : \mathit{nat} \cdot P\,n \Rightarrow P(n+1)) \Rightarrow \forall n : \mathit{nat} \cdot P\,n", and construction as the reverse implication. The book proves the bunch and predicate forms equivalent — taking B = \S n : \mathit{nat} \cdot P\,n in one direction and P = \langle n : \mathit{nat} \cdot n : B \rangle in the other — and both derivations are reproduced as derivations (each form as a hypothesis yields the other). "A corollary is that nat can be defined by the single axiom P\,0 \land (\forall n : \mathit{nat} \cdot P\,n \Rightarrow P(n+1)) = \forall n : \mathit{nat} \cdot P\,n." Uses Theorem 2.11, Definition 3.5 and Definition 3.6.

Lean code for Theorem7.2●14 declarations

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.natConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.natConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) :
  LaPToP.BasicTheories.Bunch ℤ

The *nat constructor* `B ↦ 0, B+1`: "`0` and `nat+1` are called the nat
constructors".

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.natConstructor_subset :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat ⊆
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.natConstructor_subset :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat ⊆
    LaPToP.BasicTheories.Bunch.nat

`0, nat+1: nat` (nat construction), restated with the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.nat_subset_of_natConstructor_subset
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h : LaPToP.RecursiveDefinition.natConstructor B ⊆ B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

theorem LaPToP.RecursiveDefinition.nat_subset_of_natConstructor_subset
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h :
    LaPToP.RecursiveDefinition.natConstructor
        B ⊆
      B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

`0, B+1: B ⇒ nat: B` (nat induction): "of all these bunches, nat is the smallest".

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.mem_natConstructor
  {B : LaPToP.BasicTheories.Bunch ℤ} {n : ℤ} :
  n ∈ LaPToP.RecursiveDefinition.natConstructor B ↔
    n = 0 ∨ ∃ m ∈ B, m + 1 = n

theorem LaPToP.RecursiveDefinition.mem_natConstructor
  {B : LaPToP.BasicTheories.Bunch ℤ}
  {n : ℤ} :
  n ∈
      LaPToP.RecursiveDefinition.natConstructor
        B ↔
    n = 0 ∨ ∃ m ∈ B, m + 1 = n

Membership in the constructor's image, unfolded.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version0 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version0
  (P : ℤ → Prop) : Prop

Version 0, the nat induction axiom in predicate form:
`P 0 ∧ (∀n: nat· P n ⇒ P(n+1)) ⇒ ∀n: nat· P n`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.ConstructionPred (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.ConstructionPred
  (P : ℤ → Prop) : Prop

The predicate form of nat construction:
`P 0 ∧ (∀n: nat· P n ⇒ P(n+1)) ⇐ ∀n: nat· P n`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.mem_nat {n : ℤ} :
  n ∈ LaPToP.BasicTheories.Bunch.nat ↔ 0 ≤ n

theorem LaPToP.RecursiveDefinition.mem_nat
  {n : ℤ} :
  n ∈ LaPToP.BasicTheories.Bunch.nat ↔
    0 ≤ n

`n ∈ nat ↔ 0 ≤ n`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version0_of_bunchInduction
  (h :
    ∀ (B : LaPToP.BasicTheories.Bunch ℤ),
      LaPToP.RecursiveDefinition.natConstructor B ⊆ B →
        LaPToP.BasicTheories.Bunch.nat ⊆ B)
  (P : ℤ → Prop) : LaPToP.RecursiveDefinition.Version0 P

theorem LaPToP.RecursiveDefinition.version0_of_bunchInduction
  (h :
    ∀ (B : LaPToP.BasicTheories.Bunch ℤ),
      LaPToP.RecursiveDefinition.natConstructor
            B ⊆
          B →
        LaPToP.BasicTheories.Bunch.nat ⊆
          B)
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version0 P

"The bunch form implies the predicate form": from nat induction for all
bunches, version 0 for all predicates, taking `B = §n: nat· P n`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.bunchInduction_of_version0
  (h : ∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version0 P)
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (hB : LaPToP.RecursiveDefinition.natConstructor B ⊆ B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

theorem LaPToP.RecursiveDefinition.bunchInduction_of_version0
  (h :
    ∀ (P : ℤ → Prop),
      LaPToP.RecursiveDefinition.Version0
        P)
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (hB :
    LaPToP.RecursiveDefinition.natConstructor
        B ⊆
      B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

"The reverse is proved similarly": from version 0 for all predicates, nat
induction for all bunches, taking `P = ⟨n: nat· n: B⟩`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.constructionPred_of_bunchConstruction
  (h :
    LaPToP.RecursiveDefinition.natConstructor
        LaPToP.BasicTheories.Bunch.nat ⊆
      LaPToP.BasicTheories.Bunch.nat)
  (P : ℤ → Prop) : LaPToP.RecursiveDefinition.ConstructionPred P

theorem LaPToP.RecursiveDefinition.constructionPred_of_bunchConstruction
  (h :
    LaPToP.RecursiveDefinition.natConstructor
        LaPToP.BasicTheories.Bunch.nat ⊆
      LaPToP.BasicTheories.Bunch.nat)
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.ConstructionPred
    P

"The bunch form implies the predicate form" of construction, from nat
construction.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.bunchConstruction_of_constructionPred
  (h :
    ∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.ConstructionPred P) :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat ⊆
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.bunchConstruction_of_constructionPred
  (h :
    ∀ (P : ℤ → Prop),
      LaPToP.RecursiveDefinition.ConstructionPred
        P) :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat ⊆
    LaPToP.BasicTheories.Bunch.nat

"The predicate form implies the bunch form" of construction, taking
`P = ⟨n: nat· n: nat⟩`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version0 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version0 P

theorem LaPToP.RecursiveDefinition.version0
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version0 P

Version 0 holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.constructionPred (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.ConstructionPred P

theorem LaPToP.RecursiveDefinition.constructionPred
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.ConstructionPred
    P

The predicate form of construction holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.single_axiom (P : ℤ → Prop) :
  (P 0 ∧ ∀ n ∈ LaPToP.BasicTheories.Bunch.nat, P n → P (n + 1)) ↔
    ∀ n ∈ LaPToP.BasicTheories.Bunch.nat, P n

theorem LaPToP.RecursiveDefinition.single_axiom
  (P : ℤ → Prop) :
  (P 0 ∧
      ∀
        n ∈
          LaPToP.BasicTheories.Bunch.nat,
        P n → P (n + 1)) ↔
    ∀ n ∈ LaPToP.BasicTheories.Bunch.nat,
      P n

"A corollary is that nat can be defined by the single axiom
`P 0 ∧ (∀n: nat· P n ⇒ P(n+1)) = ∀n: nat· P n`."

Proof for Theorem 7.2

uses 0

Bunch ⟹ predicate: apply bunch induction to \{n \mid n : \mathit{nat} \land P\,n\}; predicate ⟹ bunch: apply predicate induction to n \mapsto n : B. Construction likewise, with P = \langle n : \mathit{nat} \cdot n : \mathit{nat} \rangle.

Theorem7.3

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 6.4

Loading preview

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

used by 0✓L∃∀N

EffortmediumTagsrecursionnathehner-6.0.0

"There are other predicate versions of induction; here is the usual one again plus five more":

P\,0 \land (\forall n : \mathit{nat} \cdot P\,n \Rightarrow P(n+1)) \Rightarrow \forall n : \mathit{nat} \cdot P\,n;
P\,0 \lor (\exists n : \mathit{nat} \cdot \neg P\,n \land P(n+1)) \Leftarrow \exists n : \mathit{nat} \cdot P\,n;
(\forall n : \mathit{nat} \cdot P\,n \Rightarrow P(n+1)) \Rightarrow \forall n : \mathit{nat} \cdot P\,0 \Rightarrow P\,n;
(\exists n : \mathit{nat} \cdot \neg P\,n \land P(n+1)) \Leftarrow \exists n : \mathit{nat} \cdot \neg P\,0 \land P\,n;
(\forall n : \mathit{nat} \cdot (\forall m : \mathit{nat} \cdot m < n \Rightarrow P\,m) \Rightarrow P\,n) \Rightarrow \forall n : \mathit{nat} \cdot P\,n;
(\exists n : \mathit{nat} \cdot (\forall m : \mathit{nat} \cdot m < n \Rightarrow \neg P\,m) \land P\,n) \Leftarrow \exists n : \mathit{nat} \cdot P\,n. "These six versions are all equivalent to each other, and all equivalent to the bunch form of induction." Each is proved outright; the book's remarks are proved too — "version 1 is obtained from version 0 by the duality laws and a renaming" (version 1 for P is version 0 for \neg P, and likewise 3 from 2 and 5 from 4), version 2 ("the prettiest", "related to the for-loop rule" of Definition 6.4) and version 4 (strong induction) are interderivable with version 0 by changing the predicate; finally each version, taken for all predicates, is equivalent to bunch induction. Uses Theorem 7.2.

Lean code for Theorem7.3●18 declarations

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version1 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version1
  (P : ℤ → Prop) : Prop

Version 1: `P 0 ∨ (∃n: nat· ¬P n ∧ P(n+1)) ⇐ ∃n: nat· P n`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version2 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version2
  (P : ℤ → Prop) : Prop

Version 2, "the prettiest": `(∀n: nat· P n ⇒ P(n+1)) ⇒ ∀n: nat· P 0 ⇒ P n` —
"if you can “go” from any natural to the next, then you can “go” from 0 to any natural".

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version3 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version3
  (P : ℤ → Prop) : Prop

Version 3: `(∃n: nat· ¬P n ∧ P(n+1)) ⇐ ∃n: nat· ¬P 0 ∧ P n`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version4 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version4
  (P : ℤ → Prop) : Prop

Version 4 (strong induction): `(∀n: nat· (∀m: nat· m<n ⇒ P m) ⇒ P n) ⇒ ∀n: nat· P n`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.Version5 (P : ℤ → Prop) : Prop

def LaPToP.RecursiveDefinition.Version5
  (P : ℤ → Prop) : Prop

Version 5 (least element): `(∃n: nat· (∀m: nat· m<n ⇒ ¬P m) ∧ P n) ⇐ ∃n: nat· P n`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version2_of_version0
  (h : ∀ (Q : ℤ → Prop), LaPToP.RecursiveDefinition.Version0 Q)
  (P : ℤ → Prop) : LaPToP.RecursiveDefinition.Version2 P

theorem LaPToP.RecursiveDefinition.version2_of_version0
  (h :
    ∀ (Q : ℤ → Prop),
      LaPToP.RecursiveDefinition.Version0
        Q)
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version2 P

Version 2 from version 0, changing the predicate to `P 0 ⇒ P n`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version0_of_version2 {P : ℤ → Prop}
  (h : LaPToP.RecursiveDefinition.Version2 P) :
  LaPToP.RecursiveDefinition.Version0 P

theorem LaPToP.RecursiveDefinition.version0_of_version2
  {P : ℤ → Prop}
  (h :
    LaPToP.RecursiveDefinition.Version2
      P) :
  LaPToP.RecursiveDefinition.Version0 P

Version 0 from version 2 (same predicate).

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version4_of_version0
  (h : ∀ (Q : ℤ → Prop), LaPToP.RecursiveDefinition.Version0 Q)
  (P : ℤ → Prop) : LaPToP.RecursiveDefinition.Version4 P

theorem LaPToP.RecursiveDefinition.version4_of_version0
  (h :
    ∀ (Q : ℤ → Prop),
      LaPToP.RecursiveDefinition.Version0
        Q)
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version4 P

Version 4 (strong induction) from version 0, changing the predicate to
`∀m: nat· m ≤ n ⇒ P m`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version0_of_version4 {P : ℤ → Prop}
  (h : LaPToP.RecursiveDefinition.Version4 P) :
  LaPToP.RecursiveDefinition.Version0 P

theorem LaPToP.RecursiveDefinition.version0_of_version4
  {P : ℤ → Prop}
  (h :
    LaPToP.RecursiveDefinition.Version4
      P) :
  LaPToP.RecursiveDefinition.Version0 P

Version 0 from version 4 (same predicate).

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version1_iff_version0_not (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version1 P ↔
    LaPToP.RecursiveDefinition.Version0 fun n => ¬P n

theorem LaPToP.RecursiveDefinition.version1_iff_version0_not
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version1 P ↔
    LaPToP.RecursiveDefinition.Version0
      fun n => ¬P n

"Version 1 is obtained from version 0 by the duality laws and a renaming":
version 1 for `P` is version 0 for `¬P`.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version3_iff_version2_not (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version3 P ↔
    LaPToP.RecursiveDefinition.Version2 fun n => ¬P n

theorem LaPToP.RecursiveDefinition.version3_iff_version2_not
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version3 P ↔
    LaPToP.RecursiveDefinition.Version2
      fun n => ¬P n

"Version 3 is obtained from version 2 by the duality laws and a renaming".

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version5_iff_version4_not (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version5 P ↔
    LaPToP.RecursiveDefinition.Version4 fun n => ¬P n

theorem LaPToP.RecursiveDefinition.version5_iff_version4_not
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version5 P ↔
    LaPToP.RecursiveDefinition.Version4
      fun n => ¬P n

Version 5 is the dual of version 4.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version1 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version1 P

theorem LaPToP.RecursiveDefinition.version1
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version1 P

Version 1 holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version2 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version2 P

theorem LaPToP.RecursiveDefinition.version2
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version2 P

Version 2 holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version3 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version3 P

theorem LaPToP.RecursiveDefinition.version3
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version3 P

Version 3 holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version4 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version4 P

theorem LaPToP.RecursiveDefinition.version4
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version4 P

Version 4 holds.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.version5 (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version5 P

theorem LaPToP.RecursiveDefinition.version5
  (P : ℤ → Prop) :
  LaPToP.RecursiveDefinition.Version5 P

Version 5 holds: every nonempty set of naturals has a least element.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.versions_equivalent :
  (∀ (B : LaPToP.BasicTheories.Bunch ℤ),
      LaPToP.RecursiveDefinition.natConstructor B ⊆ B →
        LaPToP.BasicTheories.Bunch.nat ⊆ B) ↔
    (∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version0 P) ∧
      (∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version1 P) ∧
        (∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version2 P) ∧
          (∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version3 P) ∧
            (∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version4 P) ∧
              ∀ (P : ℤ → Prop), LaPToP.RecursiveDefinition.Version5 P

theorem LaPToP.RecursiveDefinition.versions_equivalent :
  (∀ (B : LaPToP.BasicTheories.Bunch ℤ),
      LaPToP.RecursiveDefinition.natConstructor
            B ⊆
          B →
        LaPToP.BasicTheories.Bunch.nat ⊆
          B) ↔
    (∀ (P : ℤ → Prop),
        LaPToP.RecursiveDefinition.Version0
          P) ∧
      (∀ (P : ℤ → Prop),
          LaPToP.RecursiveDefinition.Version1
            P) ∧
        (∀ (P : ℤ → Prop),
            LaPToP.RecursiveDefinition.Version2
              P) ∧
          (∀ (P : ℤ → Prop),
              LaPToP.RecursiveDefinition.Version3
                P) ∧
            (∀ (P : ℤ → Prop),
                LaPToP.RecursiveDefinition.Version4
                  P) ∧
              ∀ (P : ℤ → Prop),
                LaPToP.RecursiveDefinition.Version5
                  P

"These six versions are all equivalent to each other, and all equivalent to
the bunch form of induction": each, taken for all predicates, is equivalent to
nat induction for all bunches.

Proof for Theorem 7.3

uses 0

Duality by classical contraposition; version 2 from version 0 at P\,0 \Rightarrow P\,n; version 4 from version 0 at \forall m : \mathit{nat} \cdot m \le n \Rightarrow P\,m; the converses by instantiation.

Definition7.4

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 2.14

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Definition 7.1

Loading preview

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

✓L∃∀N

"We now prove two similar-looking theorems: \mathit{nat} = 0, \mathit{nat}+1 (nat fixed-point construction) and B = 0, B+1 \Rightarrow \mathit{nat} : B (nat fixed-point induction). ... Fixed-point construction has the form \mathit{name} = (\text{expression involving } \mathit{name}) and so it says that \mathit{name} is a fixed-point of the expression on the right. Fixed-point induction tells us that \mathit{name} is the smallest bunch satisfying fixed-point construction, and in that sense it is the least fixed-point of the constructor." Fixed-point construction "is stronger than nat construction, so the proof will also have to use nat induction"; fixed-point induction follows "just by strengthening the antecedent of nat induction". Hence \mathit{nat} is the least fixed point of its (monotonic) constructor B \mapsto 0, B+1: "we could have defined nat ... as the least fixed-point of its constructor". Uses Definition 7.1, Theorem 7.2 and Theorem 2.14.

Lean code for Definition7.4●8 declarations

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.IsFixedPoint.{u} {α : Type u} (f : α → α)
  (x : α) : Prop

def LaPToP.RecursiveDefinition.IsFixedPoint.{u}
  {α : Type u} (f : α → α) (x : α) : Prop

`x` is a *fixed point* of `f`: `f x = x`.

defdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

def LaPToP.RecursiveDefinition.IsLeastFixedPoint.{u} {α : Type u} [LE α]
  (f : α → α) (x : α) : Prop

def LaPToP.RecursiveDefinition.IsLeastFixedPoint.{u}
  {α : Type u} [LE α] (f : α → α)
  (x : α) : Prop

`x` is a *least fixed point* of `f`: a fixed point below every fixed point.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.IsLeastFixedPoint.unique.{u} {α : Type u}
  [PartialOrder α] {f : α → α} {x y : α}
  (hx : LaPToP.RecursiveDefinition.IsLeastFixedPoint f x)
  (hy : LaPToP.RecursiveDefinition.IsLeastFixedPoint f y) : x = y

theorem LaPToP.RecursiveDefinition.IsLeastFixedPoint.unique.{u}
  {α : Type u} [PartialOrder α]
  {f : α → α} {x y : α}
  (hx :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      f x)
  (hy :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      f y) :
  x = y

A least fixed point is unique.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.nat_fixedPoint_construction :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat =
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.nat_fixedPoint_construction :
  LaPToP.RecursiveDefinition.natConstructor
      LaPToP.BasicTheories.Bunch.nat =
    LaPToP.BasicTheories.Bunch.nat

`nat = 0, nat+1` (nat fixed-point construction): "stronger than nat
construction, so the proof will also have to use nat induction".

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.nat_fixedPoint_induction
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h : LaPToP.RecursiveDefinition.natConstructor B = B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

theorem LaPToP.RecursiveDefinition.nat_fixedPoint_induction
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h :
    LaPToP.RecursiveDefinition.natConstructor
        B =
      B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

`B = 0, B+1 ⇒ nat: B` (nat fixed-point induction), "just by strengthening
the antecedent of nat induction".

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.nat_isFixedPoint :
  LaPToP.RecursiveDefinition.IsFixedPoint
    LaPToP.RecursiveDefinition.natConstructor
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.nat_isFixedPoint :
  LaPToP.RecursiveDefinition.IsFixedPoint
    LaPToP.RecursiveDefinition.natConstructor
    LaPToP.BasicTheories.Bunch.nat

`nat` is a fixed point of its constructor.

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.nat_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.natConstructor
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.nat_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.natConstructor
    LaPToP.BasicTheories.Bunch.nat

"We could have defined nat ... as the least fixed-point of its constructor."

theoremdefined in LaPToP/RecursiveDefinition/Nat.lean

complete

theorem LaPToP.RecursiveDefinition.natConstructor_mono
  {A B : LaPToP.BasicTheories.Bunch ℤ} (h : A ⊆ B) :
  LaPToP.RecursiveDefinition.natConstructor A ⊆
    LaPToP.RecursiveDefinition.natConstructor B

theorem LaPToP.RecursiveDefinition.natConstructor_mono
  {A B : LaPToP.BasicTheories.Bunch ℤ}
  (h : A ⊆ B) :
  LaPToP.RecursiveDefinition.natConstructor
      A ⊆
    LaPToP.RecursiveDefinition.natConstructor
      B

The constructor is monotonic.

Definition7.5

Group member previews

Preview

Definition 7.1

Loading preview

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

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 7.6

Loading preview

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

✓L∃∀N

"Recursive construction is a procedure for constructing solutions from constructors. It usually works, but not always. We seek a solution of \mathit{name} :: (\text{expression involving } \mathit{name}) or \mathit{name} = (\text{expression involving } \mathit{name})." The steps:

construct \mathit{name}_0 = \mathit{null}, \mathit{name}_{n+1} = (\text{expression involving } \mathit{name}_n);
find an expression for \mathit{name}_n not involving \mathit{name};
form \mathit{name}_\infty by replacing n with \infty;
test that \mathit{name}_\infty is a solution;
for the smallest solution, test B = (\text{expression involving } B) \Rightarrow \mathit{name}_\infty : B. For a monotone constructor the general facts are proved: the sequence is increasing, its union (the honest reading of step 2) is included in every fixed point — so step 4 is automatic — and if the union passes the test of step 3 it is the least fixed point; the union is always a post-fixed point. The book's caveat stands: "the bunch \mathit{name}_\infty is usually a solution, but not always, so we must test it" — when the test fails the procedure yields nothing, and the property ("continuity") that would guarantee success is "left to other books". Uses Definition 7.4.

Lean code for Definition7.5●8 declarations

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.chain.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α) :
  ℕ → LaPToP.BasicTheories.Bunch α

def LaPToP.RecursiveDefinition.chain.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α) :
  ℕ → LaPToP.BasicTheories.Bunch α

Step 0: `name₀ = null`, `nameₙ₊₁ = (expression involving nameₙ)`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.chain_succ.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (n : ℕ) :
  LaPToP.RecursiveDefinition.chain C (n + 1) =
    C (LaPToP.RecursiveDefinition.chain C n)

theorem LaPToP.RecursiveDefinition.chain_succ.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (n : ℕ) :
  LaPToP.RecursiveDefinition.chain C
      (n + 1) =
    C
      (LaPToP.RecursiveDefinition.chain C
        n)

"`nameₙ` represents our knowledge of `name` after `n` uses of its constructor."

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.limit.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch α

def LaPToP.RecursiveDefinition.limit.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch α

Step 2, read honestly: `name∞` is the union of all the `nameₙ`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.chain_mono.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) : Monotone (LaPToP.RecursiveDefinition.chain C)

theorem LaPToP.RecursiveDefinition.chain_mono.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) :
  Monotone
    (LaPToP.RecursiveDefinition.chain C)

For a monotone constructor the sequence is increasing.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.chain_subset_of_prefixed.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) {B : LaPToP.BasicTheories.Bunch α} (hB : C B ⊆ B)
  (n : ℕ) : LaPToP.RecursiveDefinition.chain C n ⊆ B

theorem LaPToP.RecursiveDefinition.chain_subset_of_prefixed.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C)
  {B : LaPToP.BasicTheories.Bunch α}
  (hB : C B ⊆ B) (n : ℕ) :
  LaPToP.RecursiveDefinition.chain C n ⊆ B

Every `nameₙ` is included in every pre-fixed point `C B ⊆ B`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.limit_subset_of_fixedPoint.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) {B : LaPToP.BasicTheories.Bunch α}
  (hB : LaPToP.RecursiveDefinition.IsFixedPoint C B) :
  LaPToP.RecursiveDefinition.limit C ⊆ B

theorem LaPToP.RecursiveDefinition.limit_subset_of_fixedPoint.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C)
  {B : LaPToP.BasicTheories.Bunch α}
  (hB :
    LaPToP.RecursiveDefinition.IsFixedPoint
      C B) :
  LaPToP.RecursiveDefinition.limit C ⊆ B

Step 4 is automatic: the limit is included in every fixed point.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.isLeastFixedPoint_of_test.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C)
  (h :
    LaPToP.RecursiveDefinition.IsFixedPoint C
      (LaPToP.RecursiveDefinition.limit C)) :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint C
    (LaPToP.RecursiveDefinition.limit C)

theorem LaPToP.RecursiveDefinition.isLeastFixedPoint_of_test.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C)
  (h :
    LaPToP.RecursiveDefinition.IsFixedPoint
      C
      (LaPToP.RecursiveDefinition.limit
        C)) :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    C (LaPToP.RecursiveDefinition.limit C)

Step 3 decides: if the limit is a fixed point, it is the least fixed point.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.limit_subset_apply.{u} {α : Type u}
  (C : LaPToP.BasicTheories.Bunch α → LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) :
  LaPToP.RecursiveDefinition.limit C ⊆
    C (LaPToP.RecursiveDefinition.limit C)

theorem LaPToP.RecursiveDefinition.limit_subset_apply.{u}
  {α : Type u}
  (C :
    LaPToP.BasicTheories.Bunch α →
      LaPToP.BasicTheories.Bunch α)
  (hC : Monotone C) :
  LaPToP.RecursiveDefinition.limit C ⊆
    C (LaPToP.RecursiveDefinition.limit C)

One inclusion of the test always holds for a monotone constructor: the
limit is a *post*-fixed point, `limit ⊆ C limit`.

Theorem7.6

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 2.14

Loading preview

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

used by 0✓L∃∀N

EffortsmallTagsrecursiondatahehner-6.0.2

The book's illustration: \mathit{pow} = 1, 2 \times \mathit{pow} and B = 1, 2 \times B \Rightarrow \mathit{pow} : B. Step 0: \mathit{pow}_0 = \mathit{null}, \mathit{pow}_1 = 1, \mathit{pow}_2 = 1, 2, \mathit{pow}_3 = 1, 2, 4. Step 1: "perhaps now we can guess \mathit{pow}_n = 2^{0,..n}. We could prove this by nat induction, but it is not really necessary" (it is proved here). Step 2: \mathit{pow}_\infty = 2^{0,..\infty} = 2^{\mathit{nat}}, the union of the \mathit{pow}_n. Step 3: 2^{\mathit{nat}} = 1, 2 \times 2^{\mathit{nat}} "\Leftarrow \mathit{nat} = 0, \mathit{nat}+1, nat fixed-point construction". Step 4: 2^{\mathit{nat}} : B \Leftarrow B = 1, 2 \times B, "use the predicate form of nat induction". "Since 2^{\mathit{nat}} is the least fixed-point of the pow constructor, we conclude \mathit{pow} = 2^{\mathit{nat}}" — any bunch satisfying both axioms equals it, by uniqueness of least fixed points; the same conclusion follows from the general procedure. Uses Definition 7.5, Theorem 7.2 and Theorem 2.14 (2 \times B distributes over union).

Lean code for Theorem7.6●15 declarations

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.powConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.powConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) :
  LaPToP.BasicTheories.Bunch ℤ

The `pow` constructor `B ↦ 1, 2×B`; "`2×B`" is the bunch of doubles of
elements of `B` (`×` distributes over bunch union).

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powConstructor_mono :
  Monotone LaPToP.RecursiveDefinition.powConstructor

theorem LaPToP.RecursiveDefinition.powConstructor_mono :
  Monotone
    LaPToP.RecursiveDefinition.powConstructor

The pow constructor is monotone.

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.powN : ℕ → LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.powN :
  ℕ → LaPToP.BasicTheories.Bunch ℤ

`powₙ`, the construction sequence of `pow`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powN_zero :
  LaPToP.RecursiveDefinition.powN 0 = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.RecursiveDefinition.powN_zero :
  LaPToP.RecursiveDefinition.powN 0 =
    LaPToP.BasicTheories.Bunch.null

`pow₀ = null`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powN_one :
  LaPToP.RecursiveDefinition.powN 1 = LaPToP.BasicTheories.Bunch.elem 1

theorem LaPToP.RecursiveDefinition.powN_one :
  LaPToP.RecursiveDefinition.powN 1 =
    LaPToP.BasicTheories.Bunch.elem 1

`pow₁ = 1`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powN_two :
  LaPToP.RecursiveDefinition.powN 2 =
    LaPToP.BasicTheories.Bunch.elem 1 ∪
      LaPToP.BasicTheories.Bunch.elem 2

theorem LaPToP.RecursiveDefinition.powN_two :
  LaPToP.RecursiveDefinition.powN 2 =
    LaPToP.BasicTheories.Bunch.elem 1 ∪
      LaPToP.BasicTheories.Bunch.elem 2

`pow₂ = 1, 2`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powN_three :
  LaPToP.RecursiveDefinition.powN 3 =
    LaPToP.BasicTheories.Bunch.elem 1 ∪
        LaPToP.BasicTheories.Bunch.elem 2 ∪
      LaPToP.BasicTheories.Bunch.elem 4

theorem LaPToP.RecursiveDefinition.powN_three :
  LaPToP.RecursiveDefinition.powN 3 =
    LaPToP.BasicTheories.Bunch.elem 1 ∪
        LaPToP.BasicTheories.Bunch.elem
          2 ∪
      LaPToP.BasicTheories.Bunch.elem 4

`pow₃ = 1, 2, 4`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powN_eq (n : ℕ) :
  LaPToP.RecursiveDefinition.powN n = (fun k => 2 ^ k) '' {k | k < n}

theorem LaPToP.RecursiveDefinition.powN_eq
  (n : ℕ) :
  LaPToP.RecursiveDefinition.powN n =
    (fun k => 2 ^ k) '' {k | k < n}

Step 1, the guess `powₙ = 2^(0,..n)`: "we could prove this by nat
induction, but it is not really necessary" — here it is anyway.

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.powInf : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.powInf :
  LaPToP.BasicTheories.Bunch ℤ

Step 2: `pow∞ = 2^(0,..∞) = 2^nat`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powInf_eq_limit :
  LaPToP.RecursiveDefinition.powInf =
    LaPToP.RecursiveDefinition.limit
      LaPToP.RecursiveDefinition.powConstructor

theorem LaPToP.RecursiveDefinition.powInf_eq_limit :
  LaPToP.RecursiveDefinition.powInf =
    LaPToP.RecursiveDefinition.limit
      LaPToP.RecursiveDefinition.powConstructor

`pow∞` is the limit of the `powₙ` ("replacing `n` with `∞`").

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powConstructor_powInf :
  LaPToP.RecursiveDefinition.powConstructor
      LaPToP.RecursiveDefinition.powInf =
    LaPToP.RecursiveDefinition.powInf

theorem LaPToP.RecursiveDefinition.powConstructor_powInf :
  LaPToP.RecursiveDefinition.powConstructor
      LaPToP.RecursiveDefinition.powInf =
    LaPToP.RecursiveDefinition.powInf

Step 3, the test: `2^nat = 1, 2×2^nat`, "⇐ `nat = 0, nat+1`, nat fixed-point construction".

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powInf_subset_of_fixedPoint
  {B : LaPToP.BasicTheories.Bunch ℤ}
  (hB : LaPToP.RecursiveDefinition.powConstructor B = B) :
  LaPToP.RecursiveDefinition.powInf ⊆ B

theorem LaPToP.RecursiveDefinition.powInf_subset_of_fixedPoint
  {B : LaPToP.BasicTheories.Bunch ℤ}
  (hB :
    LaPToP.RecursiveDefinition.powConstructor
        B =
      B) :
  LaPToP.RecursiveDefinition.powInf ⊆ B

Step 4, the test for leastness: `2^nat: B ⇐ B = 1, 2×B`, "using the
predicate form of nat induction".

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.powInf_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.powConstructor
    LaPToP.RecursiveDefinition.powInf

theorem LaPToP.RecursiveDefinition.powInf_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.powConstructor
    LaPToP.RecursiveDefinition.powInf

"Since `2^nat` is the least fixed-point of the pow constructor, we conclude
`pow = 2^nat`."

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.pow_eq_powInf
  {pow : LaPToP.BasicTheories.Bunch ℤ}
  (hpow :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      LaPToP.RecursiveDefinition.powConstructor pow) :
  pow = LaPToP.RecursiveDefinition.powInf

theorem LaPToP.RecursiveDefinition.pow_eq_powInf
  {pow : LaPToP.BasicTheories.Bunch ℤ}
  (hpow :
    LaPToP.RecursiveDefinition.IsLeastFixedPoint
      LaPToP.RecursiveDefinition.powConstructor
      pow) :
  pow = LaPToP.RecursiveDefinition.powInf

Any `pow` satisfying the fixed-point construction and induction axioms is `2^nat`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.limit_powConstructor_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.powConstructor
    (LaPToP.RecursiveDefinition.limit
      LaPToP.RecursiveDefinition.powConstructor)

theorem LaPToP.RecursiveDefinition.limit_powConstructor_isLeastFixedPoint :
  LaPToP.RecursiveDefinition.IsLeastFixedPoint
    LaPToP.RecursiveDefinition.powConstructor
    (LaPToP.RecursiveDefinition.limit
      LaPToP.RecursiveDefinition.powConstructor)

The same conclusion by the general procedure: the limit passes the test.

Proof for Theorem 7.6

uses 0

The closed form by induction on n; the tests by case analysis on the exponent (2^0 = 1, 2^{k+1} = 2 \times 2^k); leastness by induction on the exponent inside a fixed point.

Theorem7.7

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 3.6

Loading preview

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

used by 0✓L∃∀N

EffortsmallTagsrecursiondatahehner-6.0.2

"Whenever we add axioms, we must be careful to remain consistent with the theory we already have. A badly chosen axiom can cause inconsistency. ... Suppose we make \mathit{bad} = \S n : \mathit{nat} \cdot \neg\, n : \mathit{bad} an axiom. Thus \mathit{bad} is defined as the bunch of all naturals that are not in \mathit{bad}. From this axiom we find 0 : \mathit{bad} = \neg\, 0 : \mathit{bad} is a theorem ... also an antitheorem. To avoid the inconsistency, we must withdraw this axiom." Proved: no bunch satisfies the axiom. "Sometimes recursive construction does not produce any answer": the sequence \mathit{bad}_0 = \mathit{null}, \mathit{bad}_1 = \mathit{nat}, \mathit{bad}_2 = \mathit{null}, "and so on, alternating between \mathit{null} and \mathit{nat}. We cannot say what \mathit{bad}_\infty is" — the constructor is antitone, not monotone, and the sequence is not increasing. Uses Definition 7.5 and Definition 3.6.

Lean code for Theorem7.7●10 declarations

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.badConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.badConstructor
  (B : LaPToP.BasicTheories.Bunch ℤ) :
  LaPToP.BasicTheories.Bunch ℤ

The `bad` constructor `B ↦ §n: nat· ¬ n: B`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.zero_mem_iff_not_mem
  {B : LaPToP.BasicTheories.Bunch ℤ}
  (hB : LaPToP.RecursiveDefinition.badConstructor B = B) : 0 ∈ B ↔ 0 ∉ B

theorem LaPToP.RecursiveDefinition.zero_mem_iff_not_mem
  {B : LaPToP.BasicTheories.Bunch ℤ}
  (hB :
    LaPToP.RecursiveDefinition.badConstructor
        B =
      B) :
  0 ∈ B ↔ 0 ∉ B

`0: bad = ¬ 0: bad` for any `bad` satisfying the axiom.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.not_exists_bad :
  ¬∃ B, LaPToP.RecursiveDefinition.badConstructor B = B

theorem LaPToP.RecursiveDefinition.not_exists_bad :
  ¬∃ B,
      LaPToP.RecursiveDefinition.badConstructor
          B =
        B

The axiom is inconsistent: no bunch satisfies `bad = §n: nat· ¬ n: bad`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badConstructor_antitone :
  Antitone LaPToP.RecursiveDefinition.badConstructor

theorem LaPToP.RecursiveDefinition.badConstructor_antitone :
  Antitone
    LaPToP.RecursiveDefinition.badConstructor

The `bad` constructor is antitone, not monotone — the procedure's
hypothesis fails.

defdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

def LaPToP.RecursiveDefinition.badN : ℕ → LaPToP.BasicTheories.Bunch ℤ

def LaPToP.RecursiveDefinition.badN :
  ℕ → LaPToP.BasicTheories.Bunch ℤ

`badₙ`, the construction sequence of `bad`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badN_zero :
  LaPToP.RecursiveDefinition.badN 0 = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.RecursiveDefinition.badN_zero :
  LaPToP.RecursiveDefinition.badN 0 =
    LaPToP.BasicTheories.Bunch.null

`bad₀ = null`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badN_one :
  LaPToP.RecursiveDefinition.badN 1 = LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.RecursiveDefinition.badN_one :
  LaPToP.RecursiveDefinition.badN 1 =
    LaPToP.BasicTheories.Bunch.nat

`bad₁ = nat`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badN_two :
  LaPToP.RecursiveDefinition.badN 2 = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.RecursiveDefinition.badN_two :
  LaPToP.RecursiveDefinition.badN 2 =
    LaPToP.BasicTheories.Bunch.null

`bad₂ = null`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badN_add_two (n : ℕ) :
  LaPToP.RecursiveDefinition.badN (n + 2) =
    LaPToP.RecursiveDefinition.badN n

theorem LaPToP.RecursiveDefinition.badN_add_two
  (n : ℕ) :
  LaPToP.RecursiveDefinition.badN
      (n + 2) =
    LaPToP.RecursiveDefinition.badN n

"And so on, alternating between `null` and `nat`": `badₙ₊₂ = badₙ`.

theoremdefined in LaPToP/RecursiveDefinition/DataConstruction.lean

complete

theorem LaPToP.RecursiveDefinition.badN_not_mono :
  ¬Monotone LaPToP.RecursiveDefinition.badN

theorem LaPToP.RecursiveDefinition.badN_not_mono :
  ¬Monotone
      LaPToP.RecursiveDefinition.badN

"We cannot say what `bad∞` is": the sequence has no limit in the sense of
the procedure — `bad₁ ⊄ bad₂`.

Theorem7.8

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 5.14

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Definition 7.1

Loading preview

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

✓L∃∀N

EffortmediumTagsrecursionprogramshehner-6.1

"Programs, and more generally, specifications, can be defined by axioms just as data can. For our first example, let x and y be integer variables. The name \mathit{zap} is introduced, and the fixed-point equation \mathit{zap} = \mathbf{if}\ x = 0\ \mathbf{then}\ y := 0\ \mathbf{else}\ x := x - 1.\ t := t + 1.\ \mathit{zap} is given as an axiom. The right side of the equation is the constructor." The book's six solutions — (a) x \ge 0 \Rightarrow x' = y' = 0 \land t' = t + x; (b) \mathbf{if}\ x \ge 0\ \mathbf{then}\ x' = y' = 0 \land t' = t + x\ \mathbf{else}\ t' = \infty; (c) x' = y' = 0 \land (x \ge 0 \Rightarrow t' = t + x); (d) x' = y' = 0 \land \mathbf{if}\ x \ge 0\ \mathbf{then}\ t' = t + x\ \mathbf{else}\ t' = \infty; (e) x' = y' = 0 \land t' = t + x; (f) x \ge 0 \land x' = y' = 0 \land t' = t + x — are each proved to be fixed points; their refinement order is the book's picture ((a) weakest, (f) strongest, with (b),(c) and (d),(e) incomparable, "the solutions are not totally ordered"); (a)–(d) are implementable with nondecreasing time, "(e) and (f) are so strong that they are unimplementable", and (d) "is also deterministic, a strongest implementable solution". Since (e) and (f) contain t' = t + x for negative x, the time variable ranges over the extended integers \mathit{xint} without -\infty here, in which t + x is total and \infty + x = \infty. Fixed-point induction "\forall\sigma, \sigma' \cdot (Z = \mathrm{constructor}\ Z) \Rightarrow \forall\sigma, \sigma' \cdot \mathit{zap} \Leftarrow Z" is proved as a theorem about every solution (indeed about every Z with \mathrm{constructor}\ Z \Leftarrow Z), so (a) is the weakest fixed point, and any \mathit{zap} satisfying the equation "refines the weakest solution (a) \Leftarrow \mathit{zap}, so we can use it to solve problems, and it is refined by its constructor \mathit{zap} \Leftarrow \mathrm{constructor}\ \mathit{zap}, so we can execute it". Uses Definition 7.1, Definition 7.4, Definition 5.14 and Theorem 5.15.

Lean code for Theorem7.8●50 declarations

structure(3 fields)defined in LaPToP/RecursiveDefinition/Programs.lean

complete

structure LaPToP.RecursiveDefinition.ZS : Type

structure LaPToP.RecursiveDefinition.ZS : Type

A state with a time variable in the extended integers (`∞ = ⊤`) and
integer variables `x`, `y`.

Fields

t : WithTop ℤ

The time variable.

x : ℤ

The variable `x`.

y : ℤ

The variable `y`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.assignX
  (e : LaPToP.RecursiveDefinition.ZS → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.assignX
  (e :
    LaPToP.RecursiveDefinition.ZS → ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

`x:= e`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.assignY
  (e : LaPToP.RecursiveDefinition.ZS → ℤ) :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.assignY
  (e :
    LaPToP.RecursiveDefinition.ZS → ℤ) :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

`y:= e`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.tick :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.tick :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

`t:= t+1`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

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

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

Substitution Law for `x:= e`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

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

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

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

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.timeNondecreasing :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.timeNondecreasing :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

Time does not decrease: `t′ ≥ t`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.ImplementableT
  (S : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS) : Prop

def LaPToP.RecursiveDefinition.Zap.ImplementableT
  (S :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS) :
  Prop

Implementable with nondecreasing time: `∀σ· ∃σ′· S ∧ t′≥t`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.zapC
  (Z : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS) :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.zapC
  (Z :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS) :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

The constructor `Z ↦ if x=0 then y:= 0 else x:= x–1. t:= t+1. Z`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.step
  (s : LaPToP.RecursiveDefinition.ZS) : LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.step
  (s : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.ZS

The state after `x:= x–1. t:= t+1`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_apply
  (Z : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS)
  (s s' : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.zapC Z s s' ↔
    s.x = 0 ∧ s' = { t := s.t, x := s.x, y := 0 } ∨
      s.x ≠ 0 ∧ Z (LaPToP.RecursiveDefinition.Zap.step s) s'

theorem LaPToP.RecursiveDefinition.Zap.zapC_apply
  (Z :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS)
  (s s' : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.zapC Z s
      s' ↔
    s.x = 0 ∧
        s' =
          { t := s.t, x := s.x, y := 0 } ∨
      s.x ≠ 0 ∧
        Z
          (LaPToP.RecursiveDefinition.Zap.step
            s)
          s'

Unfolding the constructor.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.XY (s' : LaPToP.RecursiveDefinition.ZS) :
  Prop

def LaPToP.RecursiveDefinition.Zap.XY
  (s' : LaPToP.RecursiveDefinition.ZS) :
  Prop

`x′ = y′ = 0`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.T
  (s s' : LaPToP.RecursiveDefinition.ZS) : Prop

def LaPToP.RecursiveDefinition.Zap.T
  (s s' : LaPToP.RecursiveDefinition.ZS) :
  Prop

`t′ = t + x`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.T_step
  (s s' : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.T
      (LaPToP.RecursiveDefinition.Zap.step s) s' ↔
    LaPToP.RecursiveDefinition.Zap.T s s'

theorem LaPToP.RecursiveDefinition.Zap.T_step
  (s s' : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.T
      (LaPToP.RecursiveDefinition.Zap.step
        s)
      s' ↔
    LaPToP.RecursiveDefinition.Zap.T s s'

`t′ = t + x` is unaffected by one step `x:= x–1. t:= t+1`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solA :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solA :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(a) `x≥0 ⇒ x′=y′=0 ∧ t′=t+x`, the weakest solution.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solB :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solB :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(b) `if x≥0 then x′=y′=0 ∧ t′=t+x else t′=∞`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solC :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solC :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(c) `x′=y′=0 ∧ (x≥0 ⇒ t′=t+x)`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solD :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solD :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(d) `x′=y′=0 ∧ if x≥0 then t′=t+x else t′=∞`, "a strongest implementable solution".

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solE :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solE :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(e) `x′=y′=0 ∧ t′=t+x`.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.solF :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.solF :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

(f) `x≥0 ∧ x′=y′=0 ∧ t′=t+x`, the strongest solution.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.base_iff
  {s s' : LaPToP.RecursiveDefinition.ZS} (hx : s.x = 0) :
  s' = { t := s.t, x := s.x, y := 0 } ↔
    LaPToP.RecursiveDefinition.Zap.XY s' ∧
      LaPToP.RecursiveDefinition.Zap.T s s'

theorem LaPToP.RecursiveDefinition.Zap.base_iff
  {s s' : LaPToP.RecursiveDefinition.ZS}
  (hx : s.x = 0) :
  s' = { t := s.t, x := s.x, y := 0 } ↔
    LaPToP.RecursiveDefinition.Zap.XY s' ∧
      LaPToP.RecursiveDefinition.Zap.T s
        s'

The base case `x = 0`: `y:= 0` gives `x′=y′=0 ∧ t′=t+x`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solA :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solA =
    LaPToP.RecursiveDefinition.Zap.solA

theorem LaPToP.RecursiveDefinition.Zap.zapC_solA :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solA =
    LaPToP.RecursiveDefinition.Zap.solA

(a) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solB :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solB =
    LaPToP.RecursiveDefinition.Zap.solB

theorem LaPToP.RecursiveDefinition.Zap.zapC_solB :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solB =
    LaPToP.RecursiveDefinition.Zap.solB

(b) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solC :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solC =
    LaPToP.RecursiveDefinition.Zap.solC

theorem LaPToP.RecursiveDefinition.Zap.zapC_solC :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solC =
    LaPToP.RecursiveDefinition.Zap.solC

(c) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solD :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solD =
    LaPToP.RecursiveDefinition.Zap.solD

theorem LaPToP.RecursiveDefinition.Zap.zapC_solD :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solD =
    LaPToP.RecursiveDefinition.Zap.solD

(d) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solE :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solE =
    LaPToP.RecursiveDefinition.Zap.solE

theorem LaPToP.RecursiveDefinition.Zap.zapC_solE :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solE =
    LaPToP.RecursiveDefinition.Zap.solE

(e) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapC_solF :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solF =
    LaPToP.RecursiveDefinition.Zap.solF

theorem LaPToP.RecursiveDefinition.Zap.zapC_solF :
  LaPToP.RecursiveDefinition.Zap.zapC
      LaPToP.RecursiveDefinition.Zap.solF =
    LaPToP.RecursiveDefinition.Zap.solF

(f) is a fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_solB :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    LaPToP.RecursiveDefinition.Zap.solB

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_solB :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    LaPToP.RecursiveDefinition.Zap.solB

(a) ⇐ (b).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_solC :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    LaPToP.RecursiveDefinition.Zap.solC

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_solC :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    LaPToP.RecursiveDefinition.Zap.solC

(a) ⇐ (c).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solB_refines_solD :
  LaPToP.RecursiveDefinition.Zap.solB.Refines
    LaPToP.RecursiveDefinition.Zap.solD

theorem LaPToP.RecursiveDefinition.Zap.solB_refines_solD :
  LaPToP.RecursiveDefinition.Zap.solB.Refines
    LaPToP.RecursiveDefinition.Zap.solD

(b) ⇐ (d).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solC_refines_solD :
  LaPToP.RecursiveDefinition.Zap.solC.Refines
    LaPToP.RecursiveDefinition.Zap.solD

theorem LaPToP.RecursiveDefinition.Zap.solC_refines_solD :
  LaPToP.RecursiveDefinition.Zap.solC.Refines
    LaPToP.RecursiveDefinition.Zap.solD

(c) ⇐ (d).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solC_refines_solE :
  LaPToP.RecursiveDefinition.Zap.solC.Refines
    LaPToP.RecursiveDefinition.Zap.solE

theorem LaPToP.RecursiveDefinition.Zap.solC_refines_solE :
  LaPToP.RecursiveDefinition.Zap.solC.Refines
    LaPToP.RecursiveDefinition.Zap.solE

(c) ⇐ (e).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solD_refines_solF :
  LaPToP.RecursiveDefinition.Zap.solD.Refines
    LaPToP.RecursiveDefinition.Zap.solF

theorem LaPToP.RecursiveDefinition.Zap.solD_refines_solF :
  LaPToP.RecursiveDefinition.Zap.solD.Refines
    LaPToP.RecursiveDefinition.Zap.solF

(d) ⇐ (f).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solE_refines_solF :
  LaPToP.RecursiveDefinition.Zap.solE.Refines
    LaPToP.RecursiveDefinition.Zap.solF

theorem LaPToP.RecursiveDefinition.Zap.solE_refines_solF :
  LaPToP.RecursiveDefinition.Zap.solE.Refines
    LaPToP.RecursiveDefinition.Zap.solF

(e) ⇐ (f).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_solB_refines_solC :
  ¬LaPToP.RecursiveDefinition.Zap.solB.Refines
      LaPToP.RecursiveDefinition.Zap.solC

theorem LaPToP.RecursiveDefinition.Zap.not_solB_refines_solC :
  ¬LaPToP.RecursiveDefinition.Zap.solB.Refines
      LaPToP.RecursiveDefinition.Zap.solC

(b) and (c) are not comparable: (b) is not refined by (c) ...

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_solC_refines_solB :
  ¬LaPToP.RecursiveDefinition.Zap.solC.Refines
      LaPToP.RecursiveDefinition.Zap.solB

theorem LaPToP.RecursiveDefinition.Zap.not_solC_refines_solB :
  ¬LaPToP.RecursiveDefinition.Zap.solC.Refines
      LaPToP.RecursiveDefinition.Zap.solB

... and (c) is not refined by (b): "the solutions are not totally ordered".

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_solD_refines_solE :
  ¬LaPToP.RecursiveDefinition.Zap.solD.Refines
      LaPToP.RecursiveDefinition.Zap.solE

theorem LaPToP.RecursiveDefinition.Zap.not_solD_refines_solE :
  ¬LaPToP.RecursiveDefinition.Zap.solD.Refines
      LaPToP.RecursiveDefinition.Zap.solE

(d) and (e) are not comparable either: (d) is not refined by (e) ...

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_solE_refines_solD :
  ¬LaPToP.RecursiveDefinition.Zap.solE.Refines
      LaPToP.RecursiveDefinition.Zap.solD

theorem LaPToP.RecursiveDefinition.Zap.not_solE_refines_solD :
  ¬LaPToP.RecursiveDefinition.Zap.solE.Refines
      LaPToP.RecursiveDefinition.Zap.solD

... and (e) is not refined by (d).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solA :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solA

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solA :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solA

(a) is implementable with nondecreasing time.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solB :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solB

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solB :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solB

(b) is implementable with nondecreasing time.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solC :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solC

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solC :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solC

(c) is implementable with nondecreasing time.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solD :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solD

theorem LaPToP.RecursiveDefinition.Zap.implementableT_solD :
  LaPToP.RecursiveDefinition.Zap.ImplementableT
    LaPToP.RecursiveDefinition.Zap.solD

(d) is implementable with nondecreasing time.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_implementableT_solE :
  ¬LaPToP.RecursiveDefinition.Zap.ImplementableT
      LaPToP.RecursiveDefinition.Zap.solE

theorem LaPToP.RecursiveDefinition.Zap.not_implementableT_solE :
  ¬LaPToP.RecursiveDefinition.Zap.ImplementableT
      LaPToP.RecursiveDefinition.Zap.solE

(e) is not implementable with nondecreasing time: for `x < 0` it requires
`t′ = t + x < t`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.not_implementable_solF :
  ¬LaPToP.RecursiveDefinition.Zap.solF.Implementable

theorem LaPToP.RecursiveDefinition.Zap.not_implementable_solF :
  ¬LaPToP.RecursiveDefinition.Zap.solF.Implementable

(f) is not even implementable: for `x < 0` it has no satisfactory poststate.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.deterministic_solD
  (s : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.solD.Deterministic s

theorem LaPToP.RecursiveDefinition.Zap.deterministic_solD
  (s : LaPToP.RecursiveDefinition.ZS) :
  LaPToP.RecursiveDefinition.Zap.solD.Deterministic
    s

(d) is deterministic for each prestate.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_of_prefixed
  {Z : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : (LaPToP.RecursiveDefinition.Zap.zapC Z).Refines Z) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines Z

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_of_prefixed
  {Z :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    (LaPToP.RecursiveDefinition.Zap.zapC
          Z).Refines
      Z) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    Z

Every pre-fixed point of the constructor (`constructor Z ⇐ Z`) refines (a):
the book's induction axiom `∀σ,σ′· (constructor Z ⇐ Z) ⇒ ∀σ,σ′· zap ⇐ Z`
holds with `zap := (a)`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.refines_of_eq
  {P Q : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : P = Q) : P.Refines Q

theorem LaPToP.RecursiveDefinition.Zap.refines_of_eq
  {P Q :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h : P = Q) : P.Refines Q

A specification refines an equal one.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_of_fixedPoint
  {Z : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.Zap.zapC Z = Z) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines Z

theorem LaPToP.RecursiveDefinition.Zap.solA_refines_of_fixedPoint
  {Z :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.Zap.zapC
        Z =
      Z) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
    Z

Fixed-point induction: every solution `Z = constructor Z` refines (a).

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_weakest :
  LaPToP.RecursiveDefinition.Zap.zapC
        LaPToP.RecursiveDefinition.Zap.solA =
      LaPToP.RecursiveDefinition.Zap.solA ∧
    ∀ (Z : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS),
      LaPToP.RecursiveDefinition.Zap.zapC Z = Z →
        LaPToP.RecursiveDefinition.Zap.solA.Refines Z

theorem LaPToP.RecursiveDefinition.Zap.solA_weakest :
  LaPToP.RecursiveDefinition.Zap.zapC
        LaPToP.RecursiveDefinition.Zap.solA =
      LaPToP.RecursiveDefinition.Zap.solA ∧
    ∀
      (Z :
        LaPToP.ProgramTheory.Spec
          LaPToP.RecursiveDefinition.ZS),
      LaPToP.RecursiveDefinition.Zap.zapC
            Z =
          Z →
        LaPToP.RecursiveDefinition.Zap.solA.Refines
          Z

(a) is the weakest fixed point of the constructor: a fixed point refined by
every fixed point.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zap_use_and_execute
  {zap : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.Zap.zapC zap = zap) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines zap ∧
    zap.Refines (LaPToP.RecursiveDefinition.Zap.zapC zap)

theorem LaPToP.RecursiveDefinition.Zap.zap_use_and_execute
  {zap :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.Zap.zapC
        zap =
      zap) :
  LaPToP.RecursiveDefinition.Zap.solA.Refines
      zap ∧
    zap.Refines
      (LaPToP.RecursiveDefinition.Zap.zapC
        zap)

Any `zap` defined by the fixed-point equation "refines the weakest solution
`(a) ⇐ zap`, so we can use it to solve problems, and it is refined by its
constructor `zap ⇐ constructor zap`, so we can execute it".

Proof for Theorem 7.8

uses 0

Each fixed-point check unfolds the constructor by the Substitution Law into the case x = 0 (where y := 0 gives x' = y' = 0 \land t' = t) and the case x \ne 0, where t' = t + x is invariant under x := x - 1.\ t := t + 1. The weakest-fixed-point theorem is by induction on x for x \ge 0.

Theorem7.9

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 7.2

Loading preview

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

used by 0✓L∃∀N

EffortsmallTagsrecursionprogramshehner-6.1.0

"We start with \mathit{zap}_0 describing the computation as well as we can without looking at the definition of zap ... a specification that is satisfied by every computation, \mathit{zap}_0 = \top. We obtain the next description of zap by substituting \mathit{zap}_0 for zap in the constructor, and so on. ... In general, \mathit{zap}_n describes the computation as well as possible after n uses of the constructor. We can now guess (and prove using nat induction if we want) \mathit{zap}_n = (0 \le x < n \Rightarrow x' = y' = 0 \land t' = t + x). The next step is to replace n with \infty": \mathit{zap}_\infty is solution (a), which "satisfies the fixed-point equation, and in fact it is the weakest fixed-point". Proved: the closed form of \mathit{zap}_n by induction, and (a) as the intersection of all \mathit{zap}_n. Uses Theorem 7.8 and Theorem 7.2.

Lean code for Theorem7.9●5 declarations

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.Zap.zapN :
  ℕ → LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.Zap.zapN :
  ℕ →
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS

`zap₀ = ⊤`, `zapₙ₊₁ = constructor zapₙ`: "we obtain the next description of
zap by substituting `zapₙ` for zap in the constructor".

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapN_eq (n : ℕ) :
  LaPToP.RecursiveDefinition.Zap.zapN n = fun s s' =>
    0 ≤ s.x ∧ s.x < ↑n →
      LaPToP.RecursiveDefinition.Zap.XY s' ∧
        LaPToP.RecursiveDefinition.Zap.T s s'

theorem LaPToP.RecursiveDefinition.Zap.zapN_eq
  (n : ℕ) :
  LaPToP.RecursiveDefinition.Zap.zapN n =
    fun s s' =>
    0 ≤ s.x ∧ s.x < ↑n →
      LaPToP.RecursiveDefinition.Zap.XY
          s' ∧
        LaPToP.RecursiveDefinition.Zap.T s
          s'

`zapₙ = 0≤x<n ⇒ x′=y′=0 ∧ t′=t+x`: "describes the computation as well as
possible after `n` uses of the constructor", "proved using nat induction".

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapN_one :
  LaPToP.RecursiveDefinition.Zap.zapN 1 = fun s s' =>
    0 ≤ s.x ∧ s.x < 1 →
      LaPToP.RecursiveDefinition.Zap.XY s' ∧
        LaPToP.RecursiveDefinition.Zap.T s s'

theorem LaPToP.RecursiveDefinition.Zap.zapN_one :
  LaPToP.RecursiveDefinition.Zap.zapN 1 =
    fun s s' =>
    0 ≤ s.x ∧ s.x < 1 →
      LaPToP.RecursiveDefinition.Zap.XY
          s' ∧
        LaPToP.RecursiveDefinition.Zap.T s
          s'

`zap₁ = 0≤x<1 ⇒ x′=y′=0 ∧ t′=t`, the book's first step.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.zapN_refines_solA (n : ℕ) :
  (LaPToP.RecursiveDefinition.Zap.zapN n).Refines
    LaPToP.RecursiveDefinition.Zap.solA

theorem LaPToP.RecursiveDefinition.Zap.zapN_refines_solA
  (n : ℕ) :
  (LaPToP.RecursiveDefinition.Zap.zapN
        n).Refines
    LaPToP.RecursiveDefinition.Zap.solA

Each `zapₙ` is refined by (a): the `zapₙ` approximate `zap∞ = (a)` from above.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.Zap.solA_eq_iInf_zapN :
  LaPToP.RecursiveDefinition.Zap.solA = fun s s' =>
    ∀ (n : ℕ), LaPToP.RecursiveDefinition.Zap.zapN n s s'

theorem LaPToP.RecursiveDefinition.Zap.solA_eq_iInf_zapN :
  LaPToP.RecursiveDefinition.Zap.solA =
    fun s s' =>
    ∀ (n : ℕ),
      LaPToP.RecursiveDefinition.Zap.zapN
        n s s'

"The next step is to replace `n` with `∞`": (a) is the intersection of all
the `zapₙ`.

Definition7.10

Group member previews

Preview

Definition 7.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 5.14

Loading preview

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

used by 0✓L∃∀N

"Loops can be defined by construction and induction. The axioms for the while-loop are t' \ge t \Leftarrow \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od}; \mathbf{if}\ b\ \mathbf{then}\ P.\ t := t+1.\ \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od}\ \mathbf{else}\ \mathit{ok} \Leftarrow \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od}; \forall\sigma, \sigma' \cdot (t' \ge t \land \mathbf{if}\ b\ \mathbf{then}\ P.\ t := t+1.\ W\ \mathbf{else}\ \mathit{ok} \Leftarrow W) \Rightarrow \forall\sigma, \sigma' \cdot \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od} \Leftarrow W. ... These three axioms are closely analogous to the axioms 0 : \mathit{nat}, \mathit{nat}+1 : \mathit{nat}, 0, B+1 : B \Rightarrow \mathit{nat} : B that define nat." The axioms are a structure WhileAxioms; from them the fixed-point theorems \mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od} = t' \ge t \land \mathbf{if}\ b\ \mathbf{then}\ P.\ t := t+1.\ \mathbf{while} \ldots\ \mathbf{else}\ \mathit{ok} and fixed-point induction are derived, the axioms are shown consistent (the union of all pre-fixed points satisfies them) and to determine the loop uniquely. "This account differs from that presented in Section 5.2; we have gained some theorems, and lost some theorems. For example, from this least fixed-point definition, we cannot prove x' \ge x \Leftarrow \mathbf{while}\ b\ \mathbf{do}\ x' \ge x\ \mathbf{od}, which was easily proved according to Section 5.2" — both halves are proved: the refinement is a theorem for Definition 6.1, while any loop satisfying the axioms (for b = \top) admits every final state at time \infty, so the refinement fails. Uses Theorem 7.8, Theorem 7.2 and Definition 5.14.

Lean code for Definition7.10●12 declarations

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.LoopDefinition.whileC
  (b : LaPToP.RecursiveDefinition.ZS → Prop)
  (P W : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS) :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.LoopDefinition.whileC
  (b :
    LaPToP.RecursiveDefinition.ZS → Prop)
  (P W :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS) :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

The while-loop constructor with recursive timing:
`W ↦ t′≥t ∧ if b then P. t:= t+1. W else ok`.

structure(3 fields)defined in LaPToP/RecursiveDefinition/Programs.lean

complete

structure LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
  (Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS)
  (b : LaPToP.RecursiveDefinition.ZS → Prop)
  (P : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS) : Prop

structure LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
  (Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS)
  (b :
    LaPToP.RecursiveDefinition.ZS → Prop)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS) :
  Prop

The three axioms for `while b do P od` (recursive timing):
`t′≥t ⇐ while b do P od`; `if b then P. t:= t+1. while b do P od else ok ⇐ while b do P od`;
and induction `∀σ,σ′· (t′≥t ∧ if b then P. t:= t+1. W else ok ⇐ W) ⇒ ∀σ,σ′· while b do P od ⇐ W`.
"These three axioms are closely analogous to the axioms `0: nat`, `nat+1: nat`,
`0, B+1: B ⇒ nat: B` that define nat."

Fields

time : LaPToP.RecursiveDefinition.Zap.timeNondecreasing.Refines Wh

"A base case saying that at least time does not decrease."

unroll : (LaPToP.ProgramTheory.Spec.cond b (P.seq (LaPToP.RecursiveDefinition.Zap.tick.seq Wh))
      LaPToP.ProgramTheory.Spec.ok).Refines
  Wh

"Takes a single step, saying that `while b do P od` refines (implements) its first unrolling."

induction : ∀ (W : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS),
  (LaPToP.RecursiveDefinition.LoopDefinition.whileC b P W).Refines W → Wh.Refines W

"Induction, says that it is the weakest specification that satisfies the first two axioms."

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.whileC_mono
  {b : LaPToP.RecursiveDefinition.ZS → Prop}
  {P W W' : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : W.Refines W') :
  (LaPToP.RecursiveDefinition.LoopDefinition.whileC b P W).Refines
    (LaPToP.RecursiveDefinition.LoopDefinition.whileC b P W')

theorem LaPToP.RecursiveDefinition.LoopDefinition.whileC_mono
  {b :
    LaPToP.RecursiveDefinition.ZS → Prop}
  {P W W' :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h : W.Refines W') :
  (LaPToP.RecursiveDefinition.LoopDefinition.whileC
        b P W).Refines
    (LaPToP.RecursiveDefinition.LoopDefinition.whileC
      b P W')

The constructor is monotonic.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.prefixed
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  {b : LaPToP.RecursiveDefinition.ZS → Prop}
  {P : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh b P) :
  (LaPToP.RecursiveDefinition.LoopDefinition.whileC b P Wh).Refines Wh

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.prefixed
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  {b :
    LaPToP.RecursiveDefinition.ZS → Prop}
  {P :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh b P) :
  (LaPToP.RecursiveDefinition.LoopDefinition.whileC
        b P Wh).Refines
    Wh

The first two axioms say that `while b do P od` is a pre-fixed point of the constructor.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.fixedPoint
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  {b : LaPToP.RecursiveDefinition.ZS → Prop}
  {P : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh b P) :
  LaPToP.RecursiveDefinition.LoopDefinition.whileC b P Wh = Wh

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.fixedPoint
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  {b :
    LaPToP.RecursiveDefinition.ZS → Prop}
  {P :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh b P) :
  LaPToP.RecursiveDefinition.LoopDefinition.whileC
      b P Wh =
    Wh

Fixed-point construction: `while b do P od = t′≥t ∧ if b then P. t:= t+1. while b do P od else ok`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.fixedPoint_induction
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  {b : LaPToP.RecursiveDefinition.ZS → Prop}
  {P : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh b P)
  (W : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS)
  (hW : LaPToP.RecursiveDefinition.LoopDefinition.whileC b P W = W) :
  Wh.Refines W

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.fixedPoint_induction
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  {b :
    LaPToP.RecursiveDefinition.ZS → Prop}
  {P :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh b P)
  (W :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS)
  (hW :
    LaPToP.RecursiveDefinition.LoopDefinition.whileC
        b P W =
      W) :
  Wh.Refines W

Fixed-point induction: `∀σ,σ′· (W = t′≥t ∧ if b then P. t:= t+1. W else ok) ⇒ ∀σ,σ′· while b do P od ⇐ W`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.exists_whileAxioms
  (b : LaPToP.RecursiveDefinition.ZS → Prop)
  (P : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS) :
  ∃ Wh, LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh b P

theorem LaPToP.RecursiveDefinition.LoopDefinition.exists_whileAxioms
  (b :
    LaPToP.RecursiveDefinition.ZS → Prop)
  (P :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS) :
  ∃ Wh,
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh b P

The axioms are consistent: the union of all specifications `W` with
`t′≥t ∧ if b then P. t:= t+1. W else ok ⇐ W` satisfies them.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.unique
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  {b : LaPToP.RecursiveDefinition.ZS → Prop}
  {P Wh' : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h : LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh b P)
  (h' : LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh' b P) :
  Wh = Wh'

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.unique
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  {b :
    LaPToP.RecursiveDefinition.ZS → Prop}
  {P Wh' :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh b P)
  (h' :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh' b P) :
  Wh = Wh'

Two specifications satisfying the axioms are equal.

defdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

def LaPToP.RecursiveDefinition.LoopDefinition.xGe :
  LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS

def LaPToP.RecursiveDefinition.LoopDefinition.xGe :
  LaPToP.ProgramTheory.Spec
    LaPToP.RecursiveDefinition.ZS

`x′ ≥ x`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.whileRefines_xGe
  (b : LaPToP.RecursiveDefinition.ZS → Prop) :
  LaPToP.RecursiveDefinition.LoopDefinition.xGe.WhileRefines b
    LaPToP.RecursiveDefinition.LoopDefinition.xGe

theorem LaPToP.RecursiveDefinition.LoopDefinition.whileRefines_xGe
  (b :
    LaPToP.RecursiveDefinition.ZS →
      Prop) :
  LaPToP.RecursiveDefinition.LoopDefinition.xGe.WhileRefines
    b
    LaPToP.RecursiveDefinition.LoopDefinition.xGe

In the refinement-notation reading of Section 5.2, `x′≥x ⇐ while b do x′≥x od`
is a theorem, for any `b`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.refines_top_time
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh
      (fun x => True) LaPToP.RecursiveDefinition.LoopDefinition.xGe) :
  Wh.Refines fun x s' => s'.t = ⊤

theorem LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms.refines_top_time
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh (fun x => True)
      LaPToP.RecursiveDefinition.LoopDefinition.xGe) :
  Wh.Refines fun x s' => s'.t = ⊤

In the least-fixed-point reading, `while ⊤ do x′≥x od` allows every final
state at time `∞`: any `Wh` satisfying the axioms is refined by `t′ = ∞`.

theoremdefined in LaPToP/RecursiveDefinition/Programs.lean

complete

theorem LaPToP.RecursiveDefinition.LoopDefinition.not_xGe_refines_while
  {Wh : LaPToP.ProgramTheory.Spec LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms Wh
      (fun x => True) LaPToP.RecursiveDefinition.LoopDefinition.xGe) :
  ¬LaPToP.RecursiveDefinition.LoopDefinition.xGe.Refines Wh

theorem LaPToP.RecursiveDefinition.LoopDefinition.not_xGe_refines_while
  {Wh :
    LaPToP.ProgramTheory.Spec
      LaPToP.RecursiveDefinition.ZS}
  (h :
    LaPToP.RecursiveDefinition.LoopDefinition.WhileAxioms
      Wh (fun x => True)
      LaPToP.RecursiveDefinition.LoopDefinition.xGe) :
  ¬LaPToP.RecursiveDefinition.LoopDefinition.xGe.Refines
      Wh

Hence `x′≥x ⇐ while ⊤ do x′≥x od` is *not* derivable from the axioms: the
loop may end with `x′ < x` (at time `∞`).

Theorem7.11

Group member previews

Preview

Definition 7.1

Loading preview

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

uses 1used by 0✓L∃∀N

EffortsmallTagsrecursionnat

Repeating a step zero times is the identity on states represented as natural numbers: \mathsf{repeat}\, f\, 0\, n = n. A kernel-level stand-in for the base case of Definition 7.1.

Proof for Theorem 7.11

uses 0

By the definition of Nat.repeat.

Lean code for Theorem7.11

theorem nat_repeat_zero (f : Nat → Nat) (n : Nat) :
    Nat.repeat f 0 n = n := rfl

Definition7.12

Group member previews

Preview

Definition 7.1

Loading preview

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

uses 1used by 0XL∃∀N

Concurrent composition combines independent (or weakly dependent) processes. LaPToP treats concurrency in the same refinement framework as sequential programs, once communication and timing are modeled. This node depends on Definition 7.1 for looping clients of concurrent servers.