theorem todo_rename {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : SetRel α β) (g : SetRel β γ) (A : Set α) (B : Set β) (C : Set γ) (h₁ : B ⊆ f.image A) (h₂ : C ⊆ g.image B) : C ⊆ (f.comp g).image A

def Relation.lcomp₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] (R₁ : Set (α × β × γ)) (W : Set (γ × β)) : Set (α × β)

Equations

• R₁ ∘ᵣ₁ W = {(x, c) : α × β | ∃ (y : γ) (a : β) (b : β), (x, a, y) ∈ R₁ ∧ (y, b) ∈ W ∧ c = a * b}

def Relation.lcomp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] (R₁ : Set (α × β × γ)) (R₂ : Set (γ × β × δ)) : Set (α × β × δ)

Equations

• R₁ ∘ᵣ₂ R₂ = {(x, c, z) : α × β × δ | ∃ (y : γ) (a : β) (b : β), (x, a, y) ∈ R₁ ∧ (y, b, z) ∈ R₂ ∧ c = a * b}

def «term_∘ᵣ₁_» : Lean.TrailingParserDescr

Equations

• «term_∘ᵣ₁_» = Lean.ParserDescr.trailingNode `«term_∘ᵣ₁_» 140 141 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ᵣ₁ ") (Lean.ParserDescr.cat `term 140))

def «term_∘ᵣ₂_» : Lean.TrailingParserDescr

Equations

• «term_∘ᵣ₂_» = Lean.ParserDescr.trailingNode `«term_∘ᵣ₂_» 140 141 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ᵣ₂ ") (Lean.ParserDescr.cat `term 140))

def Relation.Idle {α : Type u_1} {β : Type u_2} [Monoid β] : Set (α × β × α)

The idle transition: no state change, empty trace. Unit of both compositions above (lcomp₁.left_id_eq, lcomp₂.left_id_eq/.right_id_eq), base case of a statement list's semantics (GuardedPlusCal.Block.listReducing), semantics of a branch with no precondition (AtomicBranch.reducing), and the reflexive half of Relation.starFun.

Exposed for the same reason the two compositions are: proofs destructure membership directly with rintro ⟨rfl, rfl⟩.

Equations

• Relation.Idle = {(x, e, y) : α × β × α | x = y ∧ e = 1}

theorem Relation.lcomp₁.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R₁ R₁' : Set (α × β × γ)} {W₂ W₂' : Set (γ × β)} (R₁_sub : R₁ ≤ R₁') (W₂_sub : W₂ ≤ W₂') : R₁ ∘ᵣ₁ W₂ ≤ R₁' ∘ᵣ₁ W₂'

theorem Relation.lcomp₂.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R₁ R₁' : Set (α × β × γ)} {R₂ R₂' : Set (γ × β × δ)} (R₁_sub : R₁ ≤ R₁') (R₂_sub : R₂ ≤ R₂') : R₁ ∘ᵣ₂ R₂ ≤ R₁' ∘ᵣ₂ R₂'

theorem Set.union_le_union {α : Type u_1} {s s' t t' : Set α} (h₁ : s ≤ s') (h₂ : t ≤ t') : s ∪ t ≤ s' ∪ t'

Set.union_subset_union restated at ≤. Mathlib tags only the ⊆ form for gcongr, while the two composition lemmas above are tagged at ≤, so a goal mixing a union with a composition — which is every monotonicity obligation of a semantic functional — matches at neither relation and gcongr reports no progress. Registering the ≤ form is what lets it descend through both.

theorem Relation.mem_lcomp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R₁ : Set (α × β × γ)} {R₂ : Set (γ × β × δ)} {a : α} {c : δ} {e : β} : (a, e, c) ∈ R₁ ∘ᵣ₂ R₂ ↔ ∃ (b : γ) (e₁ : β) (e₂ : β), (a, e₁, b) ∈ R₁ ∧ (b, e₂, c) ∈ R₂ ∧ e = e₁ * e₂

theorem Relation.mem_lcomp₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R₁ : Set (α × β × γ)} {W : Set (γ × β)} {a : α} {e : β} : (a, e) ∈ R₁ ∘ᵣ₁ W ↔ ∃ (b : γ) (e₁ : β) (e₂ : β), (a, e₁, b) ∈ R₁ ∧ (b, e₂) ∈ W ∧ e = e₁ * e₂

theorem Relation.lcomp₂.intro {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R₁ : Set (α × β × γ)} {R₂ : Set (γ × β × δ)} {a : α} {b : γ} {c : δ} {e₁ e₂ : β} (h₁ : (a, e₁, b) ∈ R₁) (h₂ : (b, e₂, c) ∈ R₂) : (a, e₁ * e₂, c) ∈ R₁ ∘ᵣ₂ R₂

theorem Relation.lcomp₁.intro {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R₁ : Set (α × β × γ)} {W : Set (γ × β)} {a : α} {b : γ} {e₁ e₂ : β} (h₁ : (a, e₁, b) ∈ R₁) (h₂ : (b, e₂) ∈ W) : (a, e₁ * e₂) ∈ R₁ ∘ᵣ₁ W

theorem Relation.lcomp₂.right_union_eq_union {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R : Set (α × β × γ)} {x y : Set (γ × β × δ)} : R ∘ᵣ₂ (x ∪ y) = R ∘ᵣ₂ x ∪ R ∘ᵣ₂ y

theorem Relation.lcomp₁.right_union_eq_union {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R : Set (α × β × γ)} {x y : Set (γ × β)} : R ∘ᵣ₁ (x ∪ y) = R ∘ᵣ₁ x ∪ R ∘ᵣ₁ y

theorem Relation.lcomp₁.subset_of_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R : Set (α × β × γ)} {x y : Set (γ × β)} (x_sub_y : x ⊆ y) : R ∘ᵣ₁ x ⊆ R ∘ᵣ₁ y

theorem Relation.lcomp₁.subset_of_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R₁ R₂ : Set (α × β × γ)} {x : Set (γ × β)} (R₁_sub_R₂ : R₁ ⊆ R₂) : R₁ ∘ᵣ₁ x ⊆ R₂ ∘ᵣ₁ x

theorem Relation.lcomp₁.right_empty_eq_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R : Set (α × β × γ)} : R ∘ᵣ₁ ∅ = ∅

theorem Relation.lcomp₂.left_id_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R : Set (α × β × γ)} : Idle ∘ᵣ₂ R = R

theorem Relation.lcomp₁.left_id_eq {α : Type u_1} {β : Type u_2} [Monoid β] {R : Set (α × β)} : Idle ∘ᵣ₁ R = R

theorem Relation.lcomp₂.right_id_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] {R : Set (α × β × γ)} : R ∘ᵣ₂ Idle = R

theorem Relation.lcomp₂.assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} [Monoid β] {R₁ : Set (α × β × γ)} {R₂ : Set (γ × β × δ)} {R₃ : Set (δ × β × ε)} : R₁ ∘ᵣ₂ R₂ ∘ᵣ₂ R₃ = (R₁ ∘ᵣ₂ R₂) ∘ᵣ₂ R₃

theorem Relation.lcomp₁.left_lcomp₂_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R₁ : Set (α × β × γ)} {R₂ : Set (γ × β × δ)} {R₃ : Set (δ × β)} : (R₁ ∘ᵣ₂ R₂) ∘ᵣ₁ R₃ = R₁ ∘ᵣ₁ R₂ ∘ᵣ₁ R₃

theorem Relation.lcomp₁.union_lcomp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] {R : Set (α × β × γ)} {S : Set (γ × β × δ)} {A : Set (α × β)} {X : Set (γ × β)} {Y : Set (δ × β)} : A ∪ R ∘ᵣ₁ X ∪ (R ∘ᵣ₂ S) ∘ᵣ₁ Y = A ∪ R ∘ᵣ₁ (X ∪ S ∘ᵣ₁ Y)

Refolding a two-step run's aborting set: the abort that happens after both steps can be attached to the second step alone. Read left to right it is how a cons of aborting semantics is taken apart; read right to left it is how the tail of an induction is put back together.

theorem Relation.lcomp₁.le_of_left_le_idle {α : Type u_1} {β : Type u_2} [Monoid β] {R : Set (α × β × α)} {X : Set (α × β)} (h : R ≤ Idle) : R ∘ᵣ₁ X ≤ X

A step that changes nothing can be dropped off the front of a run that fails after it.

theorem Relation.lcomp₁.commute_step {α : Type u_1} {β : Type u_2} [Monoid β] {Q Q' R : Set (α × β × α)} {Qa Qa' Ra Xa Ya Z : Set (α × β)} (hcomm : Q ∘ᵣ₂ R = R ∘ᵣ₂ Q') (hhead : Qa ∪ Q ∘ᵣ₁ Ra ≤ Ra ∪ R ∘ᵣ₁ Qa') (hmid : Z ≤ Ra ∪ R ∘ᵣ₁ Xa) (htail : Qa' ∪ Q' ∘ᵣ₁ Xa ≤ Ya) : Qa ∪ Q ∘ᵣ₁ Z ≤ Ra ∪ R ∘ᵣ₁ Ya

One step of an "aborting commutes past" induction. Q is the statement being moved leftwards and R what it is moved past; Qa/Ra are their aborting sets, Q'/Qa' what Q becomes on the far side.

The three hypotheses are the three things such a step ever needs: that the reducing relations commute (hcomm), that Q's own aborts are covered once it has crossed R (hhead), and that the rest of the run is covered (htail). hmid absorbs a preceding inclusion — the induction hypothesis, where there is one, and le_rfl where the run is already in this shape.

Stated on bare relations because every user is the same algebra over different statements: a guard substituted into, a guard whose index was bumped, and a whole walk.

theorem Set.ωSup_is_iUnion {α : Type u_1} {chain : OmegaCompletePartialOrder.Chain (Set α)} : OmegaCompletePartialOrder.ωSup chain = ⋃ (i : ℕ), chain i

theorem Set.ωSup_is_iInter {α : Type u_1} {chain : OmegaCompletePartialOrder.Chain (Set α)ᵒᵈ} : OmegaCompletePartialOrder.ωSup chain = ⋂ (i : ℕ), chain i

theorem Relation.lcomp₁.ωcontinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] (R : Set (α × β × γ)) : OmegaCompletePartialOrder.ωScottContinuous fun (x : Set (γ × β)) => R ∘ᵣ₁ x

theorem Relation.lcomp₁.ωcontinuous_of_union {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid β] (R₁ : Set (α × β)) (R₂ : Set (α × β × γ)) : OmegaCompletePartialOrder.ωScottContinuous fun (x : Set (γ × β)) => R₁ ∪ R₂ ∘ᵣ₁ x

theorem Relation.lcomp₂.ωcontinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Monoid β] (R : Set (α × β × γ)) : OmegaCompletePartialOrder.ωScottContinuous fun (x : Set (γ × β × δ)) => R ∘ᵣ₂ x

Infinite iteration

R^∞: the executions that take infinitely many R-steps. Defined directly, from a sequence of states and a sequence of emitted traces, rather than as the greatest fixed point of X ↦ R ∘ᵣ₁ X.

The gfp is the wrong denotation, in a way that has nothing to do with how hard it is to reason about. A step emitting the empty trace makes that functional non-contractive — R ∘ᵣ₁ x ⊇ x — so at R = {(σ, 1, σ)} it is the identity, whose greatest fixed point is ⊤: every trace whatsoever, paired with a state that merely diverges silently. R^∞ gives that execution the trace 1, which is what it actually emits. The two agree only when R has no infinite chain of empty-trace steps, which Algebra.step certainly does (while TRUE { x := x + 1 }).

def Monoid.partialProd {ε : Type u_1} [Monoid ε] (e : ℕ → ε) : ℕ → ε

e 0 * ⋯ * e (n-1), and 1 when n = 0.

Equations

• Monoid.partialProd e 0 = 1
• Monoid.partialProd e n.succ = Monoid.partialProd e n * e n

@[simp]

theorem Monoid.partialProd_zero {ε : Type u_1} [Monoid ε] {e : ℕ → ε} : partialProd e 0 = 1

@[simp]

theorem Monoid.partialProd_succ {ε : Type u_1} [Monoid ε] {e : ℕ → ε} {n : ℕ} : partialProd e (n + 1) = partialProd e n * e n

theorem Monoid.partialProd_succ' {ε : Type u_1} [Monoid ε] (e : ℕ → ε) (n : ℕ) : partialProd e (n + 1) = e 0 * partialProd (fun (i : ℕ) => e (i + 1)) n

The same product peeled from the left instead of the right. partialProd folds right-to-left, but a run built forwards from a starting state produces its factors left-to-right, so relating the two is what lets a prefix of a run be recognised as a partialProd.

theorem Monoid.partialProd_add {ε : Type u_1} [Monoid ε] (e : ℕ → ε) (n₁ n₂ : ℕ) : partialProd e (n₁ + n₂) = partialProd e n₁ * partialProd (fun (i : ℕ) => e (n₁ + i)) n₂

A product splits wherever its index does. What lets the trace of two runs concatenated be read as the two runs' traces multiplied.

theorem Monoid.partialProd_eq_one {ε : Type u_1} [Monoid ε] {e : ℕ → ε} {n : ℕ} (h : ∀ i < n, e i = 1) : partialProd e n = 1

A product of ones is one.

theorem Monoid.partialProd_eq_of_ones {ε : Type u_1} [Monoid ε] {e : ℕ → ε} {a b : ℕ} (hab : a ≤ b) (h : ∀ (i : ℕ), a ≤ i → i < b → e i = 1) : partialProd e b = partialProd e a

Skipping a stretch of ones. Extending a product past factors that are all 1 does not change it — the gap-splitting fact a reindexed product needs, since deleting 1s from a sequence is exactly refusing to extend across them. partialProd_add does the splitting; this says the second factor is trivial.

class ωMonoid (ε : Type u_1) [Monoid ε] : Type u_1

A monoid in which an infinite sequence of factors has a well-behaved product. A mixin over Monoid rather than an extension of it, so that the existing [Monoid ε] binders throughout the refinement framework are untouched and no instance diamond arises. Carries the five laws refinement proofs consume, so that they read them from the instance instead of threading them as explicit hypotheses.

• ωProd : (ℕ → ε) → ε

  The product of infinitely many factors.

• partialProd_dvd (e : ℕ → ε) (n : ℕ) : ∃ (r : ε), ωProd e = Monoid.partialProd e n * r

  Every finite prefix of an infinite product divides it.

• unfold (e : ℕ → ε) : ωProd e = e 0 * ωProd fun (i : ℕ) => e (i + 1)

  The first factor of an infinite product comes out in front.

• productLimit (e r : ℕ → ε) (x : ε) : (∀ (n : ℕ), x = Monoid.partialProd e n * r n) → (∀ (n : ℕ), ∃ (m : ℕ), n ≤ m ∧ e m ≠ 1) → x = ωProd e

  An element having every partial product as a left factor is the infinite product, provided the sequence keeps contributing.

• ωProd_comp (e : ℕ → ε) (n : ℕ → ℕ) : StrictMono n → (∀ (i : ℕ), (∀ (j : ℕ), n j ≠ i) → e i = 1) → ωProd e = ωProd (e ∘ n)

  Deleting factors that are 1 does not change the product.

def Relation.omega {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] (R : Set (α × ε × α)) : Set (α × ε)

R^∞ — the states from which R can step forever, paired with the trace the whole infinite run emits.

Equations

• Relation.omega R = {x : α × ε | ∃ (σs : ℕ → α) (es : ℕ → ε), σs 0 = x.1 ∧ (∀ (i : ℕ), (σs i, es i, σs (i + 1)) ∈ R) ∧ x.2 = ωMonoid.ωProd es}

theorem Relation.omega.mono {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {R S : Set (α × ε × α)} (h : R ≤ S) : omega R ≤ omega S

theorem Relation.omega.of_idle {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {R : Set (α × ε × α)} {σs : ℕ → α} {es : ℕ → ε} (hstep : ∀ (i : ℕ), (σs i, es i, σs (i + 1)) ∈ R ∨ σs (i + 1) = σs i ∧ es i = 1) (hinf : ∀ (N : ℕ), ∃ (i : ℕ), N ≤ i ∧ (σs i, es i, σs (i + 1)) ∈ R) : (σs 0, ωMonoid.ωProd es) ∈ omega R

Deleting idle steps from an infinite run. A run in which every index either steps or stands still — emitting 1 when it stands still — is a run of the stepping relation alone, provided it steps cofinally often.

This is what a stuttering simulation needs and cannot get from Relation.omega.mono: Relation.omega (R ∪ Idle) ≤ Relation.omega R is false outright, since standing still forever is a witness of the left and of nothing on the right. Cofinality is exactly the missing side condition, and a caller supplies it from whatever well-founded measure forbids an infinite idle tail.

The compressed run is indexed by the moving indices, so its product is the original's with the idle factors deleted; ωMonoid.ωProd_comp handles that.

theorem Relation.omega.tail {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {R : Set (α × ε × α)} {σs : ℕ → α} {es : ℕ → ε} (hstep : ∀ (i : ℕ), (σs i, es i, σs (i + 1)) ∈ R) : (σs 1, ωMonoid.ωProd fun (i : ℕ) => es (i + 1)) ∈ omega R

Dropping the first step of an infinite run leaves an infinite run. Every proof that destructures a Relation.omega membership and then has to put the tail back together needs this, so it is stated once here rather than re-instantiated at each site.

Finite iteration

R*. Stated in the same ℕ-indexed shape as Relation.omega rather than reusing Relation.TraceReflTransGen (VerifiedCompiler/Relation.lean), which is Prop-valued. Sharing the shape is what lets the two refinement lemmas — one for R*, one for R^∞ — be proved by the same kind of induction over the index.

def Relation.star {α : Type u_1} {ε : Type u_2} [Monoid ε] (R : Set (α × ε × α)) : Set (α × ε × α)

R* — finitely many R-steps, with the concatenated trace.

Equations

• Relation.star R = {x : α × ε × α | ∃ (n : ℕ) (σs : ℕ → α) (es : ℕ → ε), σs 0 = x.1 ∧ σs n = x.2.2 ∧ (∀ i < n, (σs i, es i, σs (i + 1)) ∈ R) ∧ x.2.1 = Monoid.partialProd es n}

theorem Relation.star.refl {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} (a : α) : (a, 1, a) ∈ star R

Zero steps.

theorem Relation.star.head {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {a b c : α} {e e' : ε} (h : (a, e, b) ∈ R) (h' : (b, e', c) ∈ star R) : (a, e * e', c) ∈ star R

One step in front of a run.

theorem Relation.star.mono {α : Type u_1} {ε : Type u_2} [Monoid ε] {R S : Set (α × ε × α)} (h : R ≤ S) : star R ≤ star S

theorem Relation.star.dest {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {a c : α} {e : ε} (h : (a, e, c) ∈ star R) : a = c ∧ e = 1 ∨ ∃ (b : α) (e₁ : ε) (e₂ : ε), (a, e₁, b) ∈ R ∧ (b, e₂, c) ∈ star R ∧ e = e₁ * e₂

A run is either empty or a step followed by a run. The eliminator the closed form below needs, since Relation.star is indexed by a length rather than defined inductively.

theorem Relation.star.lcomp₁_absorb {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {Y : Set (α × ε)} : R ∘ᵣ₁ star R ∘ᵣ₁ Y ≤ star R ∘ᵣ₁ Y

A step in front of a run-then-Y is again a run-then-Y.

This is the absorption side condition that the aborting and diverging refinements both need in order to place an abort reached after n steps in the aborting set itself rather than in semⁿ ∘ᵣ₁ sem'. Stated at the closed form it is a theorem; at an arbitrary aborting semantics it has to be assumed, which is what Diverging.omega's and Diverging.star's abs binder is.

theorem Relation.star.le_lcomp₁ {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {Y : Set (α × ε)} : Y ≤ star R ∘ᵣ₁ Y

Y itself is a run-then-Y, the run being empty. The base case of the absorption above, and what lets an aborting refinement of Y be read as one of R* ∘ᵣ₁ Y.

theorem Relation.star.single {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} : R ≤ star R

One step is a run.

theorem Relation.star.trans {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {a b c : α} {e₁ e₂ : ε} (h₁ : (a, e₁, b) ∈ star R) (h₂ : (b, e₂, c) ∈ star R) : (a, e₁ * e₂, c) ∈ star R

Two runs end to end. Proved by peeling the first step of the left-hand run rather than by concatenating the two index-wise: Relation.star.head already knows how to put a step in front, so the induction only has to keep the trace's factors in the same order — which is Monoid.partialProd_succ'.

theorem Relation.star.star_eq {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} : star (star R) = star R

Runs of runs are runs. What lets a refinement whose source side already absorbs a whole run per target step be lifted to the whole iteration: instantiating StrongRefinement.Terminating.star at Relation.star R produces R** on the source, and this collapses it back.

theorem Relation.star.star_lcomp₁_absorb {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {Y : Set (α × ε)} : star R ∘ᵣ₁ star R ∘ᵣ₁ Y ≤ star R ∘ᵣ₁ Y

A whole run in front of a run-then-Y is again a run-then-Y. The absorption law at the shape a refinement whose source absorbs a run per target step produces (StrongRefinement.Terminating.starStutter): there the side condition arrives with Relation.star R where lcomp₁_absorb has R.

lcomp₁_absorb at R := Relation.star R, with star_eq collapsing the R** it leaves behind.