Following a proof through a circuit

Static snapshot of CircuitProofs.lean · source revision dated 2026-10-19T10:47:08.000Z · source SHA-256 b63362090205432edb452733fc4b5471a4123ef60723d8e6c5a96674472c5675. Saved results, shown as recorded. Each result is shown as its check last saved it, compared only with this saved source and not with the reader's Lean environment. Nothing was checked or run to show it. This static page does not check or update results.

import Gimle.Forseti
L1–1
import Mathlib.Tactic.Linarith
L2–2

Conditions belong to the wires. This circuit doubles a value, then triples it. The three Hoare theorems identify what is known before, between and after those components. Use Conditions to hide the labels, or select one triple to inspect its component. Click a wire label to see the predicate and its theorem.

namespace Notebook.CircuitProofs
L13–13
open Gimle.Asgard Gimle.Forseti
L14–14

Definition P : Predicate 1 L16–16

Namespace Notebook.CircuitProofs

⟨fun  x  =>  0  ≤  x  0  ∧  x  0  ≤  1⟩\langle \text{fun}\;\text{x}\;=>\;0\;\le \;\text{x}\;0\;\land \;\text{x}\;0\;\le \;1\rangle
Lean source · 1 line
def P : Predicate 1 := ⟨fun x => 0 ≤ x 0 ∧ x 0 ≤ 1⟩

Definition M : Predicate 1 L17–17

Namespace Notebook.CircuitProofs

⟨fun  x  =>  0  ≤  x  0  ∧  x  0  ≤  2⟩\langle \text{fun}\;\text{x}\;=>\;0\;\le \;\text{x}\;0\;\land \;\text{x}\;0\;\le \;2\rangle
Lean source · 1 line
def M : Predicate 1 := ⟨fun x => 0 ≤ x 0 ∧ x 0 ≤ 2⟩

Definition Q : Predicate 1 L18–18

Namespace Notebook.CircuitProofs

⟨fun  x  =>  0  ≤  x  0  ∧  x  0  ≤  6⟩\langle \text{fun}\;\text{x}\;=>\;0\;\le \;\text{x}\;0\;\land \;\text{x}\;0\;\le \;6\rangle
Lean source · 1 line
def Q : Predicate 1 := ⟨fun x => 0 ≤ x 0 ∧ x 0 ≤ 6⟩

Definition double : Circuit 1 1 L19–19

Namespace Notebook.CircuitProofs

.scalar  2.\text{scalar}\;2
Lean source · 1 line
def double : Circuit 1 1 := .scalar 2

Definition triple : Circuit 1 1 L20–20

Namespace Notebook.CircuitProofs

.scalar  3.\text{scalar}\;3
Lean source · 1 line
def triple : Circuit 1 1 := .scalar 3

Definition pipeline : Circuit 1 1 L21–21

Namespace Notebook.CircuitProofs

.compose  double  triple.\text{compose}\;\text{double}\;\text{triple}
Lean source · 1 line
def pipeline : Circuit 1 1 := .compose double triple

Theorem first Kernel checkedAs recorded L23–28

Namespace Notebook.CircuitProofs

Doubling maps the unit interval into the interval from zero to two.

Statement
ExactHoare  P  double  M\text{ExactHoare}\;\text{P}\;\text{double}\;\text{M}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Doubling maps the unit interval into the interval from zero to two. -/
theorem first : ExactHoare P double M := by
  intro x hx
  change 0 ≤ x 0 ∧ x 0 ≤ 1 at hx
  change 0 ≤ 2 * x 0 ∧ 2 * x 0 ≤ 2
  constructor <;> linarith [hx.1, hx.2]

Theorem second Kernel checkedAs recorded L30–35

Namespace Notebook.CircuitProofs

Tripling establishes the final bound from the intermediate bound.

Statement
ExactHoare  M  triple  Q\text{ExactHoare}\;\text{M}\;\text{triple}\;\text{Q}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Tripling establishes the final bound from the intermediate bound. -/
theorem second : ExactHoare M triple Q := by
  intro x hx
  change 0 ≤ x 0 ∧ x 0 ≤ 2 at hx
  change 0 ≤ 3 * x 0 ∧ 3 * x 0 ≤ 6
  constructor <;> linarith [hx.1, hx.2]

Theorem whole Kernel checkedAs recorded L37–39

Namespace Notebook.CircuitProofs

The intermediate condition connects the two checked component triples.

Statement
ExactHoare  P  pipeline  Q\text{ExactHoare}\;\text{P}\;\text{pipeline}\;\text{Q}
uses first second

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines
/-- The intermediate condition connects the two checked component triples. -/
theorem whole : ExactHoare P pipeline Q := by
  exact exactHoareSequential first second

circuit diagram pipeline L41–41

Typed circuit · Hoare conditionsin 0out 0× (2) · 1 inputs, 1 outputs× (2)× (3) · 1 inputs, 1 outputs× (3)P · Notebook.CircuitProofs.firstPM · Notebook.CircuitProofs.firstMQ · Notebook.CircuitProofs.secondQ
Hoare triple · Notebook.CircuitProofs.first · declaration
Precondition P
fun x => 0 ≤ x 0 ∧ x 0 ≤ 1
Postcondition M
fun x => 0 ≤ x 0 ∧ x 0 ≤ 2

Conditions describe this component’s whole input and output tuples.

Hoare triple · Notebook.CircuitProofs.second · declaration
Precondition M
fun x => 0 ≤ x 0 ∧ x 0 ≤ 2
Postcondition Q
fun x => 0 ≤ x 0 ∧ x 0 ≤ 6

Conditions describe this component’s whole input and output tuples.

Hoare triple · Notebook.CircuitProofs.whole · declaration
Precondition P
fun x => 0 ≤ x 0 ∧ x 0 ≤ 1
Postcondition Q
fun x => 0 ≤ x 0 ∧ x 0 ≤ 6

Conditions describe this component’s whole input and output tuples.

A condition on a bundle

The input condition below relates both coordinates. Its bracket spans both wires; it is not a separate bound on either coordinate. Swapping the coordinates preserves the same region.

Definition unitDisk : Predicate 2 L51–51

Namespace Notebook.CircuitProofs

⟨fun  x  =>  x  0  ⋅  x  0  +  x  1  ⋅  x  1  ≤  1⟩\langle \text{fun}\;\text{x}\;=>\;\text{x}\;0\;\cdot \;\text{x}\;0\;+\;\text{x}\;1\;\cdot \;\text{x}\;1\;\le \;1\rangle
Lean source · 1 line
def unitDisk : Predicate 2 := ⟨fun x => x 0 * x 0 + x 1 * x 1 ≤ 1⟩

Definition exchange : Circuit 2 2 L52–52

Namespace Notebook.CircuitProofs

.swap.\text{swap}
Lean source · 1 line
def exchange : Circuit 2 2 := .swap

Theorem exchange_preserves Kernel checkedAs recorded L54–59

Namespace Notebook.CircuitProofs

Exchanging coordinates preserves their joint quadratic bound.

Statement
ExactHoare  unitDisk  exchange  unitDisk\text{ExactHoare}\;\text{unitDisk}\;\text{exchange}\;\text{unitDisk}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Exchanging coordinates preserves their joint quadratic bound. -/
theorem exchange_preserves : ExactHoare unitDisk exchange unitDisk := by
  intro x hx
  change x 0 * x 0 + x 1 * x 1 ≤ 1 at hx
  change x 1 * x 1 + x 0 * x 0 ≤ 1
  linarith

circuit diagram exchange L61–61

Typed circuit · Hoare conditionsin 0in 1out 0out 1swap · 2 inputs, 2 outputsunitDisk · Notebook.CircuitProofs.exchange_preservesunitDiskunitDisk · Notebook.CircuitProofs.exchange_preservesunitDisk
Hoare triple · Notebook.CircuitProofs.exchange_preserves · declaration
Precondition unitDisk
fun x => x 0 * x 0 + x 1 * x 1 ≤ 1
Postcondition unitDisk
fun x => x 0 * x 0 + x 1 * x 1 ≤ 1

Conditions describe this component’s whole input and output tuples.

end Notebook.CircuitProofs
L63–63