Skip to content

Commit 92d4199

Browse files
gaetanserregaetanserre
committed
WIP terminates
1 parent d591a17 commit 92d4199

5 files changed

Lines changed: 259 additions & 44 deletions

File tree

‎RandomDo.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,4 +27,5 @@ public import RandomDo.Tactic.IsMarkov.Elab
2727
public import RandomDo.Tactic.IsMarkov.ForInStep
2828
public import RandomDo.Tactic.IsMarkov.Lemmas
2929
public import RandomDo.Tactic.IsMarkov.While.LoopInvariant
30+
public import RandomDo.Tactic.IsMarkov.While.Tactic
3031
public import RandomDo.Tactic.IsMarkov.While.Termination

‎RandomDo/Tactic/IsMarkov/While/LoopInvariant.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,6 @@ namespace LoopInvariant
4545
instance : CoeFun (LoopInvariant f) fun _ ↦ ForInStep σ → Prop where
4646
coe I t := ForInStep.casesOn t I.stopped I.running
4747

48-
/-- The invariant that always holds. -/
49-
instance : Top (LoopInvariant f) where
50-
top := { running := fun _ ↦ True, step := fun _ _ ↦ .of_forall fun t ↦ by cases t <;> trivial }
51-
5248
end LoopInvariant
5349

5450
end MeasurableSpaceMonadWhile

‎RandomDo/Tactic/IsMarkov/While/Tactic.lean‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
/-
2+
Copyright (c) 2026 Gaëtan Serré. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Gaëtan Serré
5+
-/
6+
module
7+
8+
public import RandomDo.Tactic.IsMarkov.While.Termination
9+
10+
/-!
11+
# A tactic for the termination of `while` loops
12+
13+
`terminates` proves the goal `Terminates f b` that `is_markov` hands back for a `while` loop, from
14+
an invariant, a variant and a probability given on the states of the loop. It applies a rule of
15+
`RandomDo.Tactic.IsMarkov.While.Termination`, unfolds the step of the loop on its successors, and
16+
leaves the remaining conditions as goals about the states only.
17+
18+
## Main declarations
19+
20+
* `loop_step`: simplifies a goal about one step of a loop into conditions on its successors.
21+
* `terminates`: proves the termination of a loop by one of the rules.
22+
-/
23+
24+
public meta section
25+
26+
open Lean
27+
28+
/-- `loop_step [h₁, …]` simplifies a goal about one step of a loop: a property that almost every
29+
successor of a state satisfies, the probability of a set of successors, or an arithmetic condition.
30+
It evaluates the step on its successors, with the additional simp lemmas `h₁, …` for the
31+
definitions of the program, splits on the conditions of the program, and tries to close the
32+
resulting goals, which only mention the state. -/
33+
syntax (name := loopStep) "loop_step" (" [" term,* "]")? : tactic
34+
35+
macro_rules
36+
| `(tactic| loop_step $[[$ls,*]]?) => do
37+
let ls : Array Term := (ls.map (·.getElems)).getD #[]
38+
`(tactic| (
39+
try intro $(mkIdent `s) $(mkIdent `hs)
40+
try simp only at *
41+
try simp only [MeasureTheory.ae_iff]
42+
try split_ifs
43+
all_goals try norm_num [MeasureTheory.Measure.dirac_apply, Set.indicator_apply,
44+
ENNReal.toReal_add, ENNReal.toReal_ofReal', ENNReal.mul_eq_top, $[$ls:term],*] at *
45+
-- A measure followed by a deterministic successor is its image, and the probability of a set
46+
-- under the image is at least the probability of its preimage.
47+
all_goals try rw [MeasureTheory.Measure.bind_dirac_eq_map]
48+
all_goals try refine le_trans ?_ (ENNReal.toReal_mono (MeasureTheory.measure_ne_top _ _)
49+
(MeasureTheory.Measure.le_map_apply ?_ _))
50+
all_goals try fun_prop
51+
all_goals try simp only [Set.preimage_ofPred_eq] at *
52+
all_goals try split_ifs
53+
all_goals try norm_num [ENNReal.toReal_add, ENNReal.toReal_ofReal', ENNReal.mul_eq_top] at *
54+
all_goals repeat' apply And.intro
55+
all_goals try first | done | trivial | assumption | omega | linarith | positivity))
56+
57+
/-- The invariant of `terminates`: the given property of the running states, whose stability is left
58+
as the goal `step`, or the property that always holds. -/
59+
def invariant (P? : Option Term) : MacroM Term :=
60+
match P? with
61+
| some P => `(({ running := $P, step := ?step } : MeasurableSpaceMonadWhile.LoopInvariant _))
62+
| none => `(({ running := fun _ ↦ True
63+
step := fun _ _ ↦ Filter.Eventually.of_forall fun t ↦ by cases t <;> trivial } :
64+
MeasurableSpaceMonadWhile.LoopInvariant _))
65+
66+
/-- `terminates` proves the termination of a `while` loop, the goal `Terminates f b` that
67+
`is_markov` hands back (after `intro` of the parameters the loop depends on).
68+
69+
* `terminates (prob := ε)` applies `Terminates.mcIverMorgan_immediateEscape`: every step stops with
70+
probability at least `ε > 0`.
71+
* `terminates (variant := U) (bound := N) (prob := ε)` applies
72+
`Terminates.majumdarSathiyanarayana_variantRule`, with a variant `U : σ → ℕ` on the states, at
73+
most `N`, decreased with probability at least `ε > 0` by every step that does not stop. Stopping
74+
counts as decreasing `U`.
75+
* `(invariant := P)`, before the other arguments, restricts both to the states satisfying
76+
`P : σ → Prop`, which almost every step keeps.
77+
* `[h₁, …]`, after the other arguments, are simp lemmas for the definitions of the program.
78+
79+
The variant rule takes a variant `U'` on the states `ForInStep σ` of the transition system, with
80+
`Lo ≤ U' < Hi`, and a probability `> ε` of decreasing it. `terminates` applies it to
81+
`U' (done s) = 0` and `U' (yield s) = U s + 1`, between `Lo = 0` and `Hi = N + 2`, with `ε / 2`:
82+
* A step from `yield s` that stops goes to some `done s'`, and counts as decreasing `U'` only if
83+
`U' (done s') < U' (yield s)`. As `U` can be `0` on a running state (when the loop is about to
84+
stop, as `countdown` at `0`), the terminal states need a value below all the values of `U`:
85+
hence the shift of `U` by `1` on the running states, the terminal states taking `0`. A step to
86+
`yield s'` still decreases `U'` exactly when it decreases `U`.
87+
* On the invariant, `U s ≤ N`, so `0 ≤ U' ≤ N + 1`, and the strict upper bound of the rule is
88+
`N + 2`: one for the shift, one for passing from `≤` to `<`.
89+
* `(prob := ε)` asks for a probability at least `ε`, while the rule asks for one greater than its
90+
constant: a probability `≥ ε` is `> ε / 2`.
91+
92+
The conditions it cannot prove are left as goals about the states only. -/
93+
syntax (name := terminatesTac) "terminates" (atomic(" (" &"invariant") " := " term ")")?
94+
(atomic(" (" &"variant") " := " term ")")? (atomic(" (" &"bound") " := " term ")")?
95+
" (" &"prob" " := " term ")" (" [" term,* "]")? : tactic
96+
97+
macro_rules
98+
| `(tactic| terminates $[(invariant := $P?)]? (prob := $ε) $[[$ls,*]]?) => do
99+
let ls : Array Term := (ls.map (·.getElems)).getD #[]
100+
let I ← invariant P?
101+
`(tactic| (
102+
intros
103+
refine MeasurableSpaceMonadWhile.Terminates.mcIverMorgan_immediateEscape $I $ε ?pos
104+
?init ?stop
105+
all_goals try loop_step [$[$ls:term],*]))
106+
| `(tactic| terminates $[(invariant := $P?)]? (variant := $U) (bound := $N) (prob := $ε)
107+
$[[$ls,*]]?) => do
108+
let ls : Array Term := (ls.map (·.getElems)).getD #[]
109+
let I ← invariant P?
110+
let P ← P?.getDM `(fun _ ↦ True)
111+
`(tactic| (
112+
intros
113+
-- `U` shifted by `1` on the running states, below which the terminal states are `0`: see the
114+
-- docstring for the bounds `0` and `N + 2` and for `ε / 2`.
115+
refine MeasurableSpaceMonadWhile.Terminates.majumdarSathiyanarayana_variantRule $I
116+
(fun t ↦ ForInStep.casesOn (motive := fun _ ↦ ℤ) t (fun _ ↦ 0) fun s ↦ (($U s : ℕ) : ℤ) + 1)
117+
0 ((($N : ℕ) : ℤ) + 2) ($ε / 2) (half_pos ?pos) ?init ?bounds
118+
(fun $(mkIdent `s) $(mkIdent `hs) ↦ (half_lt_self ?pos).trans_le ?progress) ?measurable
119+
-- The bound of the lifted variant, from the bound `U ≤ N` on the states of the invariant.
120+
case' bounds =>
121+
intro t $(mkIdent `hs)
122+
cases t with
123+
| done _ => dsimp only; omega
124+
| yield $(mkIdent `s) =>
125+
replace $(mkIdent `hs) : ($P) $(mkIdent `s) := $(mkIdent `hs)
126+
try dsimp only at $(mkIdent `hs):ident ⊢
127+
refine (fun h : ($U) $(mkIdent `s) ≤ ($N) ↦ by (try simp only [] at h); omega) ?_
128+
try loop_step [$[$ls:term],*]
129+
-- The measurability of the lifted variant, from the measurability of `U`.
130+
case' measurable => first
131+
| exact Measurable.of_discrete
132+
| (refine MeasurableSpaceMonadWhile.measurable_casesOn measurable_const
133+
(((Measurable.of_discrete (f := fun n : ℕ ↦ (n : ℤ))).comp ?_).add_const 1)
134+
first | fun_prop | measurability | skip)
135+
try case' step => try loop_step [$[$ls:term],*]
136+
try case' init => try loop_step [$[$ls:term],*]
137+
try case' pos => try loop_step [$[$ls:term],*]
138+
try case' progress => try loop_step [$[$ls:term],*]))
139+
| `(tactic| terminates $[(invariant := $_)]? (variant := $_) (prob := $_) $[[$_,*]]?) =>
140+
Macro.throwError "terminates: a variant needs a bound, given by `(bound := N)`"
141+
| `(tactic| terminates $[(invariant := $_)]? (bound := $_) (prob := $_) $[[$_,*]]?) =>
142+
Macro.throwError "terminates: a bound needs a variant, given by `(variant := U)`"
143+
144+
end

‎RandomDo/Tactic/IsMarkov/While/Termination.lean‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,9 @@ hypotheses of its paper.
2222
* `Terminates.majumdarSathiyanarayana_variantRule`: the variant rule of McIver and Morgan, as
2323
presented by Majumdar and Sathiyanarayana (POPL 2025, Proof Rule 3.1), derived from the zero-one
2424
law as McIver and Morgan derive their variant rule (2005, Lemma 2.7.1).
25+
* `Terminates.mcIverMorgan_immediateEscape`: termination when every step stops with probability at
26+
least some fixed `ε > 0`, the stronger condition McIver and Morgan remark after their zero-one law
27+
(2005, p. 54).
2528
2629
## Implementation notes
2730
@@ -191,6 +194,27 @@ theorem majumdarSathiyanarayana_variantRule (I : LoopInvariant f) (U : ForInStep
191194
← ENNReal.ofReal_pow hε.le] at hlim
192195
exact (ENNReal.ofReal_le_iff_le_toReal (ne_top_of_le_ne_top ENNReal.one_ne_top hloop)).1 hlim
193196

197+
/-- **Immediate escape** (McIver and Morgan 2005, p. 54: the stronger condition they remark after
198+
the zero-one law, Lemma 2.6.1).
199+
200+
If, from every non-terminal state of the invariant `I`, one step stops with probability at least
201+
some fixed `ε > 0`, then the program terminates almost surely from `yield b`. This is the condition
202+
of a rejection sampling loop, which stops as soon as its sample satisfies a property of probability
203+
at least `ε`. It is the variant rule with the variant `1` on the non-terminal states and `0` on the
204+
terminal ones. -/
205+
theorem mcIverMorgan_immediateEscape (I : LoopInvariant f) (ε : ℝ) (hε : 0 < ε) (hb : I.running b)
206+
(hstop : ∀ s, I.running s → ε ≤ (f s {t | t.isDone}).toReal)
207+
(hf : IsMarkov f := by is_markov) : Terminates f b := by
208+
refine majumdarSathiyanarayana_variantRule I (fun t ↦ if t.isDone then 0 else 1) 0 2 (ε / 2)
209+
(half_pos hε) hb (fun t _ ↦ by split_ifs <;> simp) (fun s hs ↦ ?_)
210+
(Measurable.ite (ForInStep.measurable_isDone (measurableSet_singleton true))
211+
measurable_const measurable_const) hf
212+
-- The successors that decrease the variant are the terminal ones.
213+
refine (half_lt_self hε).trans_le ((hstop s hs).trans_eq ?_)
214+
congr 2
215+
ext t
216+
cases t <;> simp
217+
194218
end Terminates
195219

196220
end MeasurableSpaceMonadWhile

‎Test/IsMarkov.lean‎

Lines changed: 90 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ node. There is one test here per construct it recognises.
1212
-/
1313

1414
open scoped ENNReal
15-
open MeasureTheory ProbabilityTheory MeasurableSpacePure MeasurableSpaceMonadWhile
15+
open MeasureTheory ProbabilityTheory MeasurableSpacePure
1616

1717
@[expose] public section
1818

@@ -97,8 +97,8 @@ example : IsMarkov overList := by is_markov
9797
/-! ## `while`, whose termination is handed back
9898
9999
`is_markov` proves that a `while` loop is Markovian up to its termination, which it hands back as a
100-
goal `Terminates`. Each test closes it with a proof rule of the literature, from
101-
`RandomDo.Tactic.IsMarkov.While.Termination`. -/
100+
goal `Terminates`. Each test closes it with `terminates`, which applies a proof rule of the
101+
literature from `RandomDo.Tactic.IsMarkov.While.Termination`. -/
102102

103103
noncomputable def untilHeads : Measure ℕ := rdo
104104
let mut n := 0
@@ -109,14 +109,10 @@ noncomputable def untilHeads : Measure ℕ := rdo
109109
break
110110
return n
111111

112-
/-- The variant rule of McIver and Morgan, as stated by Majumdar and Sathiyanarayana: with the
113-
invariant that always holds, the variant is `1` while the loop runs, `0` once it has stopped. -/
112+
/-- Immediate escape: every step stops with probability `1 / 2`. -/
114113
example : IsProbabilityMeasure untilHeads := by
115114
is_markov
116-
refine fun _ ↦ .majumdarSathiyanarayana_variantRule ⊤ (fun t ↦ if t.isDone then 0 else 1) 0 2
117-
(1 / 4) (by norm_num) trivial (fun t _ ↦ by split_ifs <;> simp)
118-
fun n _ ↦ ?_
119-
norm_num [fairCoin]
115+
terminates (prob := 1 / 2) [fairCoin]
120116

121117
/-- A `while` loop whose condition reads the parameter. -/
122118
noncomputable def climbFrom (k : ℕ) : Measure ℕ := rdo
@@ -127,19 +123,13 @@ noncomputable def climbFrom (k : ℕ) : Measure ℕ := rdo
127123
n := n + 1
128124
return n
129125

130-
/-- The variant rule of McIver and Morgan, as stated by Majumdar and Sathiyanarayana: below the
131-
invariant bound `k + 3`, the variant is `k + 4 - n` while the loop runs. -/
126+
/-- The variant rule: below the invariant bound `k + 3`, the variant `k + 3 - n` decreases with
127+
probability `1 / 2`. -/
132128
example : IsMarkov climbFrom := by
133129
is_markov
134-
refine fun k ↦ .majumdarSathiyanarayana_variantRule
135-
{ running := (· ≤ k + 3), step := fun n (hn : n ≤ k + 3) ↦ ?_ }
136-
(fun t ↦ if t.isDone then 0 else (k : ℤ) + 4 - t.run) 0 (k + 5) (1 / 4) (by norm_num)
137-
(Nat.le_add_right k 3) (fun t ht ↦ by cases t <;> simp at ht ⊢ <;> omega)
138-
(fun n (hn : n ≤ k + 3) ↦ ?_)
139-
· rw [ae_iff]
140-
by_cases h : n < k + 3 <;> simp [h, hn.not_gt, fairCoin]
141-
omega
142-
· by_cases h : n < k + 3 <;> norm_num [h, fairCoin, show (n : ℤ) < k + 4 by omega]
130+
intro k
131+
terminates (invariant := (· ≤ k + 3)) (variant := (k + 3 - ·)) (bound := k + 3) (prob := 1 / 2)
132+
[fairCoin]
143133

144134
/-- A deterministic countdown, whose counter is bounded only by its initial value. -/
145135
noncomputable def countdown (k : ℕ) : Measure ℕ := rdo
@@ -148,18 +138,11 @@ noncomputable def countdown (k : ℕ) : Measure ℕ := rdo
148138
i := i - 1
149139
return i
150140

151-
/-- The variant rule of McIver and Morgan, as stated by Majumdar and Sathiyanarayana: below the
152-
invariant bound `k`, the variant is the counter plus one while the loop runs. -/
141+
/-- The variant rule: below the invariant bound `k`, the counter decreases at every step. -/
153142
example : IsMarkov countdown := by
154143
is_markov
155-
refine fun k ↦ .majumdarSathiyanarayana_variantRule
156-
{ running := (· ≤ k), step := fun i (hi : i ≤ k) ↦ ?_ }
157-
(fun t ↦ if t.isDone then 0 else (t.run : ℤ) + 1) 0 (k + 2) (1 / 2) (by norm_num) le_rfl
158-
(fun t ht ↦ by cases t <;> simp at ht ⊢ <;> omega)
159-
(fun i _ ↦ by by_cases h : 0 < i <;> norm_num [h])
160-
rw [ae_iff]
161-
by_cases h : 0 < i <;> simp [h]
162-
omega
144+
intro k
145+
terminates (invariant := (· ≤ k)) (variant := id) (bound := k) (prob := 1)
163146

164147
/-- A `while` loop over two mutable variables: the flips until two heads. -/
165148
noncomputable def untilTwoHeads : Measure ℕ := rdo
@@ -172,18 +155,85 @@ noncomputable def untilTwoHeads : Measure ℕ := rdo
172155
heads := heads + 1
173156
return flips
174157

175-
/-- The variant rule of McIver and Morgan, as stated by Majumdar and Sathiyanarayana: below the
176-
invariant bound `2` on the heads, the variant is `3 - heads` while the loop runs. -/
158+
/-- The variant rule, on the pairs `(heads, flips)`: below the invariant bound `2` on the heads, the
159+
variant `2 - heads` decreases with probability `1 / 2`. -/
177160
example : IsProbabilityMeasure untilTwoHeads := by
178161
is_markov
179-
refine fun _ ↦ .majumdarSathiyanarayana_variantRule
180-
{ running := fun p ↦ p.1 ≤ 2, step := fun p (hp : p.1 ≤ 2) ↦ ?_ }
181-
(fun t ↦ if t.isDone then 0 else 3 - (t.run.1 : ℤ)) 0 4 (1 / 4) (by norm_num) (by simp)
182-
(fun t ht ↦ by cases t <;> simp at ht ⊢; omega)
183-
(fun p (hp : p.1 ≤ 2) ↦ ?_)
184-
· rw [ae_iff]
185-
by_cases h : p.1 < 2 <;> simp [h, hp.not_gt, fairCoin]
186-
· by_cases h : p.1 < 2 <;> norm_num [h, fairCoin, show p.1 < 3 by omega]
162+
terminates (invariant := fun p ↦ p.1 ≤ 2) (variant := fun p ↦ 2 - p.1) (bound := 2)
163+
(prob := 1 / 2) [fairCoin]
164+
165+
/-- The flips of a coin of bias `p` until heads. -/
166+
noncomputable def geometric (p : unitInterval) : Measure ℕ := rdo
167+
let mut n := 0
168+
while true rdo
169+
let b ← bernoulliMeasure true false p
170+
n := n + 1
171+
if b then
172+
break
173+
return n
174+
175+
/-- Immediate escape, with a symbolic probability. -/
176+
example (p : unitInterval) (hp : 0 < (p : ℝ)) : IsProbabilityMeasure (geometric p) := by
177+
is_markov
178+
terminates (prob := p)
179+
180+
/-- The gambler's ruin: a fair random walk stopped at `0` and at `N`. -/
181+
noncomputable def ruin (N x : ℕ) : Measure ℕ := rdo
182+
let mut y := x
183+
while 0 < y ∧ y < N rdo
184+
let b ← fairCoin
185+
if b then
186+
y := y + 1
187+
else
188+
y := y - 1
189+
return y
190+
191+
/-- The variant rule, with the distance to the nearest barrier as the variant. -/
192+
example (N : ℕ) : IsMarkov (ruin N) := by
193+
is_markov
194+
terminates (variant := fun y ↦ min y (N - y)) (bound := N) (prob := 1 / 2) [fairCoin]
195+
196+
/-- A die by rejection: three flips give a number below `8`, kept if it is below `6`. -/
197+
noncomputable def die : Measure ℕ := rdo
198+
let mut r := 6
199+
while 6 ≤ r rdo
200+
let a ← fairCoin
201+
let b ← fairCoin
202+
let c ← fairCoin
203+
r := (if a then 4 else 0) + (if b then 2 else 0) + (if c then 1 else 0)
204+
return r
205+
206+
/-- The variant rule, with the variant `1` on the rejected numbers: a step keeps the number it draws
207+
with probability `3 / 4`. -/
208+
example : IsProbabilityMeasure die := by
209+
is_markov
210+
terminates (variant := fun r ↦ if 6 ≤ r then 1 else 0) (bound := 1) (prob := 3 / 4) [fairCoin]
211+
212+
/-- A Gaussian random walk, stopped once it leaves `(-1, 1)`. -/
213+
noncomputable def gaussianWalk (x : ℝ) : Measure ℝ := rdo
214+
let mut y := x
215+
while |y| < 1 rdo
216+
let z ← gaussianReal 0 1
217+
y := y + z
218+
return y
219+
220+
/-- The variant rule, with the variant `1` inside `(-1, 1)`: a step leaves it with probability at
221+
least `P(Z ≥ 2)`. The goals left are about the Gaussian distribution only. -/
222+
example : IsMarkov gaussianWalk := by
223+
is_markov
224+
intro x
225+
terminates (variant := fun y ↦ if |y| < 1 then 1 else 0) (bound := 1)
226+
(prob := (gaussianReal 0 1 (Set.Ici 2)).toReal)
227+
· -- From `|s| < 1`, a step of at least `2` leaves `(-1, 1)`.
228+
rename_i h
229+
refine measure_mono fun a (ha : 2 ≤ a) ↦ ?_
230+
have := (abs_lt.1 h).1
231+
simp [show ¬|s + a| < 1 from fun h' ↦ by linarith [(abs_lt.1 h').2]]
232+
· exact ENNReal.toReal_le_of_le_ofReal zero_le_one (by simp [prob_le_one])
233+
· refine ENNReal.toReal_pos (fun h ↦ ?_) (measure_ne_top _ _)
234+
simpa using gaussianReal_absolutelyContinuous' 0 one_ne_zero h
235+
· exact Measurable.ite (measurableSet_lt (by fun_prop) measurable_const) measurable_const
236+
measurable_const
187237

188238
/-! ## Looking through definitions, and the `fuel` argument -/
189239

0 commit comments

Comments
 (0)