Kleene algebra with tests

TheoremA one-step simulation lifts to finite iteration#✓fully proved

A one-step simulation lifts to arbitrary finite iteration. The simulator p need not be invertible or a test.

theorem star_simulation {K : Type*} [KleeneAlgebra K] {p a b : K}
    (h : p * a ≤ b * p) : p * a∗ ≤ b∗ * p

Used by 1

Used byTests preserved by one step are preserved by iteration

TheoremTests preserved by one step are preserved by iteration#✓fully proved

An idempotent subidentity preserved by one step is preserved by iteration. This is a corollary of star_simulation; the test assumptions are explicit, with no additional algebraic structure.

theorem test_star_absorption {K : Type*} [KleeneAlgebra K] {p a : K}
    (hp : p ≤ 1) (hpp : p * p = p) (h : p * a = p * a * p) :
    p * a∗ = p * a∗ * p

Uses 1

Proof usesA one-step simulation lifts to finite iteration

DefinitionDiagonal test relation of an assertion#✓fully proved

The diagonal relation restricted to an assertion.

def testSet (P : Set World) : SquareRelations World :=
  {(s, t) | s = t ∧ s ∈ P}

Used by 15

Used byMembership in a diagonal test relation · Postcondition absorption characterizes partial correctness · Verification inequality characterizes partial correctness · Partial correctness as unreachability of the negated postcondition · Test of a negated assertion is the complement within identity · Test of the false assertion is the zero relation · Diagonal tests are subidentities · Composing diagonal tests conjoins their assertions · Test of a union of assertions is the union of tests · Test of the true assertion is the identity relation · Hoare triples as KAT absorption equations · Hoare triples as KAT test inequalities · Test absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation · Tests are interpreted by PDL satisfaction

TheoremMembership in a diagonal test relation#✓fully proved

Membership in a diagonal test.

@[simp] theorem mem_testSet {P : Set World} {s t : World} :
    testSet P (s, t) ↔ s = t ∧ s ∈ P

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremDiagonal tests are subidentities#✓fully proved

A test is a subidentity, not an arbitrary relation.

theorem testSet_le_one (P : Set World) : testSet P ≤ 1

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremComposing diagonal tests conjoins their assertions#✓fully proved

Sequential tests conjoin their assertions without changing state.

@[simp] theorem testSet_mul_testSet (P Q : Set World) :
    testSet P * testSet Q = testSet (P ∩ Q)

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremVerification inequality characterizes partial correctness#✓fully proved

The verification inequality is precisely universal partial correctness: every execution from P ends in Q.

theorem test_mul_le_mul_test_iff (P Q : Set World)
    (R : SquareRelations World) :
    testSet P * R ≤ R * testSet Q ↔ P ⊆ SetRel.core R Q

Uses 1 · Used by 1

Statement usesDiagonal test relation of an assertion

Used byHoare triples as KAT test inequalities

TheoremPostcondition absorption characterizes partial correctness#✓fully proved

A postcondition can be absorbed on the right exactly when it holds on every execution starting in the precondition.

theorem test_mul_eq_test_mul_test_iff (P Q : Set World)
    (R : SquareRelations World) :
    testSet P * R = testSet P * R * testSet Q ↔
      P ⊆ SetRel.core R Q

Uses 1 · Used by 1

Statement usesDiagonal test relation of an assertion

Used byHoare triples as KAT absorption equations

TheoremPartial correctness as unreachability of the negated postcondition#✓fully proved

Classically, verification means that no execution from P can reach the complement of Q.

theorem test_mul_test_compl_eq_bot_iff (P Q : Set World)
    (R : SquareRelations World) :
    testSet P * R * testSet Qᶜ = ⊥ ↔ P ⊆ SetRel.core R Q

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremTest of the false assertion is the zero relation#✓fully proved

The false assertion is the zero relation.

@[simp] theorem testSet_empty : testSet (∅ : Set World) = ⊥

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremTest of the true assertion is the identity relation#✓fully proved

The true assertion is the identity relation.

@[simp] theorem testSet_univ : testSet (Set.univ : Set World) = 1

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremTest of a negated assertion is the complement within identity#✓fully proved

Boolean test negation is complement relative to identity, not the full relation-algebra complement (which includes off-diagonal pairs).

theorem testSet_compl (P : Set World) :
    testSet Pᶜ = (testSet P)ᶜ ⊓ 1

Uses 1

Statement usesDiagonal test relation of an assertion

TheoremTest of a union of assertions is the union of tests#✓fully proved

Union of assertions is union of their diagonal tests.

theorem testSet_union (P Q : Set World) :
    testSet (P ∪ Q) = testSet P ⊔ testSet Q

Uses 1

Statement usesDiagonal test relation of an assertion

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.