proof-workflows

Proof Workflows

Proof Strategy Decision Tree

What are you trying to prove?

1. Two games have the same distribution (g₁ ≡ₚ g₂): → by_equiv to enter relational mode, then use rvcstep / rvcgen → Add using ... when the current relational step needs an explicit witness

2. Advantage is bounded (advantage ≤ ε): → by_dist to enter TV distance reasoning → Use by_dist ε₂ when you want to pin the TV-distance contribution explicitly → For identical-until-bad: use tvDist_simulateQ_le_probEvent_bad

3. Probability equals a specific value (Pr[= x | oa] = ...): → Start with vcstep if the goal should lower or decompose automatically → Use vcstep? when you want the explicit script, binder names, rewrite form, or an explicit using / inv / with step surfaced → Otherwise use probOutput_bind_eq_tsum to decompose binds manually → Use simp with project simp lemmas → Use vcstep, vcstep rw, or vcstep rw congr' for probability equalities

4. Multi-hop security proof (g₁ ≡ₚ gₙ): → game_trans g₂ to split into two goals, repeat

5. Need to swap sampling order: → Use vcstep if the swap should close the goal → Use vcstep rw (or vcstep rw under n) if you need to continue after rewriting

Monadic Normalization with monad_norm

The canonical way to normalize monadic expressions in this codebase is Mathlib's monad_norm simp set (declared in Mathlib.Tactic.Attr.Register). It bundles pure_bind, bind_assoc, bind_pure, map_pure, pure_seq, seq_assoc, seq_eq_bind_map, and map_eq_bind_pure_comp, which between them push goals toward an associated bind-canonical form.

Prefer simp [monad_norm] (or simp […, monad_norm]) over hand-rolled lemma lists like simp [bind_assoc, pure_bind, …]. It documents intent, keeps proofs robust if Mathlib adds further rules, and reads more clearly. In simp only calls it is fine too — simp only [monad_norm] is just the closed set.