CEGIW in Lean 4

A formalisation of Counterexample-Guided Interval Weakening (CEGIW), by Andrew, Dennis, Fisher and Farrell, in Lean 4. It covers the metric temporal logic (MTL) definitions of §2, the weakening algorithm of §3, the correctness and optimality results, and the O(|π|^td(φ)) complexity bound. Lean 4.33.1 against Mathlib, 19 modules, about 4,080 lines, zero sorry.

Building

lake build

Cegiw/Audit.lean is built last and prints the axiom dependencies of every headline result. No listing contains anything beyond propext, Classical.choice and Quot.sound, and several manage with fewer. If sorryAx ever appears there, a proof has gone soft.

Module map

Module	Paper
Cegiw/Interval.lean	intervals [a, b] with a : ℕ, b : ℕ∞; right-bound extension and contraction (Def. 4)
Cegiw/Syntax.lean	MTL formulae, contexts, context substitution (Def. 1)
Cegiw/Semantics.lean	pointwise semantics over ℕ; shift congruence
Cegiw/Weakening.lean	the weakening order ⊑ (Def. 2); Theorem 3; Lemmas 5–8
Cegiw/Lasso.lean	lasso traces, endIdx (the paper's end_π), covering intervals; Lemma 11
Cegiw/Algorithm.lean	Lasso.weaken (Alg. 1), uDirect (Alg. 2), uLeftLoop (Alg. 3), the appendix's unnumbered WeakenRDirect (rDirect), WeakenURight (uRightLoop), WeakenRLeft (rLeftLoop) and WeakenRRight (rRightLoop), and the ∧/∨ cases the paper elides
Cegiw/Correctness/*.lean	Lemmas 13–18 and Theorem 19, one module per context shape
Cegiw/Counterexample.lean	machine-checked counterexamples to WeakenRLeft
Cegiw/Complexity.lean	instrumented loops, Context.holeDepth and Context.size, the `O(
Cegiw/Audit.lean	#print axioms for the results below

The named results, all in the Formula namespace:

Lean	Paper
Context.subst_weakens	Theorem 3
until_weaken_hi / release_weaken_hi	Lemmas 5 / 6
extension_weakening_order / contraction_weakening_order	Lemmas 7 / 8
Lasso.coverage	Lemma 11, offset form (deviation 2); Lasso.coverage_abs is the paper's statement
Problem.weaken_sound	soundness, every context
Problem.weaken_spec, Problem.weaken_correct	Theorem 19, for contexts satisfying both Context.NoReleaseL and Context.WellFormed
Problem.rRightLoop_complete	completeness of the WeakenRRight scan, where Context.WellFormed is consumed
Formula.release_eq_neg_until	the paper's remark φ ℛ_I ψ ≡ ¬(¬φ 𝒰_I ¬ψ), proved — a check that the corrected release orientation of deviation 1 is the right one
Problem.sound_releaseL	soundness for the release-left case
Problem.complete_optimal_releaseL_of_break	completeness and optimality for release-left, under hbreak
ReleaseLeftGap.not_complete, ReleaseLeftGap.not_optimal	the counterexamples
Lasso.weakenI_fst	the instrumented algorithm returns what Lasso.weaken returns, for every context
Lasso.weakenI_cost	`cost ≤ C.size * (
Lasso.weaken_cost_le	the `O(
Lasso.weakenI_cost_hole_eq	a hole scan that runs to completion costs exactly steps Iorig.lo (end_π(Iorig.lo))
Lasso.uLeftLoopI_cost_eq	a temporal context multiplies its subcontext's cost by its own scan length

Problem.Sound, Problem.Complete, Problem.Optimal and Problem.Spec are in Cegiw/Correctness/Defs.lean; Optimal is Definition 12.

WeakenRLeft is incomplete and non-optimal

Weakenℛ Left, the unnumbered algorithm of the appendix, is wrong on the context shape C ℛ_J φ, where the hole sits in the left operand — the releaser. It is neither complete nor optimal, and the same behaviour is in _aux_release_left in src/weaken.py of the Python implementation.

Release has a vacuous first disjunct. The clause ∀ i ∈ J, π ⊨[t+i] φ satisfies C[ψ △_I ψ'] ℛ_J φ for every interval I, whatever the recursive calls report about the hole. When φ happens to hold throughout the covering interval, I_orig is therefore always a valid weakening, and since nothing weaker is needed it is also the strongest one.

Weakenℛ Left does not see this. It collects the intervals returned by the recursive calls and returns None when that collection is empty, so it reports that no weakening exists in exactly the situation where I_orig works. When the collection is non-empty it returns an interval strictly weaker than I_orig, which breaks optimality by the same argument.

Both failures are machine-checked in Cegiw/Counterexample.lean over two small lassos, each with the context [-] ℛ_{[0,0]} ⊤. ReleaseLeftGap.not_complete uses a trace on which no proposition ever holds and the problem ⊥ 𝒰_{[0,0]} ⊥, which no extension can satisfy. The algorithm returns None, and P₀_holds shows I_orig satisfies the context by the vacuous disjunct. ReleaseLeftGap.not_optimal uses a trace where the single proposition holds exactly at time 1 and the problem ⊤ 𝒰_{[0,0]} p, so the recursive call returns [0, 1], which P₁_dualStrict shows is strictly weaker than I_orig.

The fix is one line of pseudocode. If the loop of Weakenℛ Left runs to completion without φ ever failing, return I_orig rather than None.

The other three temporal cases are fine. Weaken𝒰Left has the if i = a escape, and until has no vacuous disjunct to begin with; Weakenℛ Right puts the hole in the obligation, which every disjunct constrains. This is why Problem.weaken_spec carries the hypothesis Context.NoReleaseL and the release-left case is split in two: sound_releaseL holds unconditionally, and complete_optimal_releaseL_of_break assumes hbreak, that φ fails somewhere in the covering interval. That hypothesis is exactly the case the pseudocode's break was written for.

Weakenℛ Right needs a ≤ b

The MTL syntax rule of §2 requires every interval [a, b] to satisfy a ≤ b, and that restriction is load-bearing for Weakenℛ Right.

On an empty context interval J, a release holds vacuously through its first disjunct for every interval at the hole, which is the same vacuity that breaks Weakenℛ Left. Meanwhile Lasso.steps J.lo (covHi J) is zero, so the scan runs no iterations and reports None. Unlike the Weakenℛ Left case this is ruled out by the grammar: well-formed syntax admits no empty interval.

It shows up in the formalisation as the hypothesis hJne : (J.lo : ℕ∞) ≤ J.hi on Problem.rRightLoop_complete and Problem.spec_releaseR, and as the predicate Context.WellFormed, which asserts a ≤ b at every temporal node of a context. Only the release-right case consumes it.

None of this rescues Weakenℛ Left. The counterexamples above use the interval [0, 0], which is well formed.

Off-by-a in _aux_release_right

The Python implementation tests self.markings.get(c.left, trace_idx + i + a) in _aux_release_right (src/weaken.py), where every other site, including Weakenℛ Right in the paper, uses trace_idx + i. Since i already ranges over [a, right_idx], the left bound is added twice, and the discrepancy is only visible when a > 0. The formalisation follows the paper here.

The O(|π|^td(φ)) bound

Lasso.weaken is noncomputable and returns an Option Interval, so it carries no notion of running time. Cegiw/Complexity.lean supplies one by pairing it with an instrumented twin, Lasso.weakenI, which returns Option Interval × ℕ, the result alongside a step count. Every loop in Algorithm.lean gets an instrumented twin, and the twins branch on the same scrutinees as the originals. The twins are proved to agree. Formula.Lasso.weakenI_fst shows (L.weakenI …).1 = L.weaken … for every context. The instrumented run therefore takes the path the real one takes, and its count is a statement about the algorithm.

One unit of cost is charged per loop iteration. Each iteration performs a bounded number of satisfaction tests, which in the reference Python implementation are lookups in a precomputed marking table. Unit-per-iteration is faithful up to a constant that depends on the formula alone and is constant in the trace.

Two structural measures on contexts drive the bound. Context.holeDepth counts the temporal operators on the path to the hole, and Context.size counts the nodes on that path. Formula.Lasso.weakenI_cost proves cost ≤ C.size * (|π| + 1) ^ (C.holeDepth + 1), and Context.holeDepth_succ_le_temporalDepth proves C.holeDepth + 1 ≤ td(C[φ]) whenever td(φ) ≥ 1. Composing the two gives Formula.Lasso.weaken_cost_le, which reads cost ≤ C.size * (|π| + 1) ^ td(C[ψ △_I ψ']). C.size is the constant hidden by the O. It depends on the formula alone and is constant in the trace, which is what makes this the paper's O(|π|^td(φ)).

The + 1 in |π| + 1 is real. A loop over the covering interval of [a, b] runs end_π(a) + 1 - a iterations, and when a = 0 and a < |π_pre| that is exactly |π| + 1; Formula.Lasso.steps_covHi_le bounds any single loop's iteration count by |π| + 1. Cegiw/Audit.lean prints the axiom dependencies of all four results, and each lists only the usual three, with holeDepth_succ_le_temporalDepth needing just propext and Quot.sound.

An upper bound on a cost model leaves open whether the model charges anything at all, so two further lemmas pin it down from below. Formula.Lasso.weakenI_cost_hole_eq shows that when ψr never holds and ψl always does, so nothing stops the scan early, the hole case costs exactly steps Iorig.lo (end_π(Iorig.lo)), its full iteration count. Formula.Lasso.uLeftLoopI_cost_eq shows that when the guard φ never holds and every recursive call returns an interval at cost c, one temporal context costs exactly n * (c + 1). Each temporal constructor on the path therefore multiplies the cost below it by its own scan length. The exponent is the hole depth and the base is the scan length. The bound is attained.

Deviations from the paper

All of these are recorded in the relevant module docstring as well.

1. Release semantics. The typeset definition in §2 reads π,t ⊨ φ₁ ℛ_I φ₂ iff (∀ i ∈ I. π,t+i ⊨ φ₁) ∨ ∃ j ∈ I. (π,t+j ⊨ φ₂ ∧ ∀ i ∈ [0,i] ∩ I. π,t+i ⊨ φ₁), which swaps the two operands relative to the rest of the paper: it makes the first operand the obligation and the second the releaser. The proof of Lemma 6, the proof of the ℛ base case, Weakenℛ Direct and the Python implementation all make the first operand the releaser and the second the obligation. That is the standard convention. Weakenℛ Direct follows it, breaking when ψ_r fails and returning when ψ_l holds. A second slip: the inner bound variable shadows the witness, so [0,i] should be [0,j]. Formalised in the form the proofs use.
2. Lemma 11 in offset time. The paper states coverage in absolute time, but every application is at offset time. The algorithm evaluates π ⊨[t+i] φ for arbitrary base t, with endIdx applied to the offset a rather than to t+a. Those coincide only at t = 0. The offset form is true and is proved directly as Lasso.coverage; the paper's statement is the t = 0 instance, Lasso.coverage_abs.
3. Right-bound contraction. [a, b−i] with i ≤ b−a is ill-defined at b = ∞, since truncated subtraction gives ∞ − i = ∞, which contracts nothing. Replaced by a relational definition Interval.RightContr, which agrees with the arithmetic one for finite b (rightContr_coe_iff) and behaves correctly at ∞.
4. Primitive ∨. Disjunction is a constructor of the syntax, because the context grammar includes C ∨ φ and no negation may sit on the path to the hole.
5. Accumulators instead of max/min. The pseudocode's "interval with maximal (minimal) absolute difference to I_orig" is implemented as a running weakest (strongest) accumulator. All candidates share I_orig's left bound, so they are ordered by right bound alone, and maximal absolute difference means weakest in the order of Lemmas 7 and 8. This also drops the sign hack that _interval_abs_diff needs when I_orig = [a, ∞].
6. The if i = a branch of Algorithm 3 is decided on the accumulator being empty. That is equivalent and total, whereas max of an empty list is not.
7. Noncomputable definitions. Satisfaction of an MTL formula on an infinite trace is undecidable, so the semantics use classical case analysis. The implementation recovers computability by evaluating on the finite lasso representation.
8. Notation. The paper's π, t ⊨ φ is written π ⊨[t] φ, because a comma in the notation collides with Lean's ∀ x ∈ s, binder parser.
9. Until semantics. The paper requires the left operand of 𝒰 only on [0,i) ∩ I, where pointwise MTL usually requires it on all of [0,i). Formalised as written. Nothing here depends on the choice, and the De Morgan duality φ ℛ_I ψ ≡ ¬(¬φ 𝒰_I ¬ψ) still holds under it, proved as Formula.release_eq_neg_until.

Not covered

Soundness holds for every context: Problem.weaken_sound. Completeness and optimality hold for every well-formed context whose hole is not in the left operand of a release, which is Context.WellFormed together with Context.NoReleaseL. For that one shape both are false, and hold only under hbreak.

The iterative outer loop of §3.1 is not formalised. It needs a model checker as an oracle, and its correctness follows from Theorem 19 directly.

Formalising the four temporal cases uniformly is what surfaced the missing branch in Weakenℛ Left: three of them justify their early return and the fourth cannot. The case it gets wrong is the one where the release obligation is never tested, which is easy to leave out of a test suite because nothing in it ever fails.