Tactic coupling, a more general rnd tactic

[namasikanam]

This PR introduces a coupling tactic, which works on pRHL goal where the last statements on the two sides are both sampling statements.

{phi} c1; x <$ g1 ~ c2; y <$ g2 {psi}

It has two forms.

1. One-sided form accepts one argument, which is a function from the specified side to the other side. This is a little generalization for rnd in the sense that the function is not restricted to be bijective.

This form of tactic will generate one of two goals:

left: {phi} c1 ~ c2 {dmap d1 g = d2 /\ forall u, u \in supp(d1) => psi[x -> u, y -> g(u)]}
right: {phi} c1 ~ c2 {d1 = dmap d2 g /\ forall v, v \in supp(d2) => psi[x -> g(v), y -> v]}

2. Two-sided form accepts one argument, which is a coupling of the two (see [RAND] in POPL'17 Coupling Proofs Are Probabilistic Product Programs).

This form of tactic will generate a goal as follows:

{phi} c1 ~ c2 {iscoupling g muL muR /\ (forall u v, (u, v) \in supp(g) => psi[x -> u, y -> v])}

See tests/coupling-rnd.ec for the usage.

Remark: The original rnd tactic contains some post-processing simplification containing short-circuiting conjunctions. There's no post-processing for this coupling tactic.

Update: instead of generating forall a b, a \in supp(d1) => b = g(a) => psi[x -> a, y -> b], I choose to generate forall a, a \in supp(d1) => psi[x -> a, y -> g(a)] directly. The reason for this change is as follows: I found that the default substitution API will automatically use let-binding if at least twice substitutions are needed for one pattern, which already satisfies the readability target for this unnecessary b = g(a).

[fdupress]

forall a b, b = g(a) => psi[x -> a, y -> b]

Why not forall a, psi[x -> a, y -> g(a)]?

[namasikanam]

forall a b, b = g(a) => psi[x -> a, y -> b]

Why not forall a, psi[x -> a, y -> g(a)]?

Because the former is more readable and easier to understand. This is Manuel's suggestion, and I think it makes sense. Do you agree @fdupress ?

[fdupress]

I think this is a pretty Quixotic quest.

Proofs where this will make a difference to the actual readability of the actual post are likely to be small enough that a reasonable user will remember "oh yeah, I used the tactic that says that the sampling on the left is coupled with the result of applying g to the sampling on the right."

For proofs that are complex enough that the user loses track of the fact they did that, this little drop of readability is likely to get lost in an ocean of symbols that gets mooshed by move=> /> before anyone ever attempts to read it.

But maybe it's worth giving the user a chance, knowing that /> will do the work of cleaning up the extra reasoning step for us. Check with @strub tomorrow?

[Copilot]

Pull Request Overview

This PR introduces a new coupling tactic for proving pRHL (probabilistic Relational Hoare Logic) goals involving sampling statements. The tactic generalizes the existing rnd tactic by allowing non-bijective functions and direct coupling specifications.

Key changes:

• Adds support for one-sided coupling (using a function from one distribution to another)
• Adds support for two-sided coupling (using an explicit coupling distribution)
• Includes two supporting lemmas (iscpl_dmap1 and iscpl_dmap2) for the one-sided case

Reviewed Changes

Copilot reviewed 8 out of 9 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
theories/distributions/Distr.ec	Adds two lemmas establishing coupling properties for mapped distributions
tests/coupling-rnd.ec	Provides comprehensive test cases demonstrating all forms of the coupling tactic
src/phl/ecPhlRnd.mli	Exports the new process_coupling function
src/phl/ecPhlRnd.ml	Implements the core coupling tactic logic with goal generation
src/ecParsetree.ml	Adds the Pcoupling parse tree constructor
src/ecParser.mly	Adds grammar rule for parsing the coupling tactic
src/ecLexer.mll	Registers "coupling" as a keyword token
src/ecHiTacticals.ml	Wires the coupling tactic into the tactical processor

---

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

[namasikanam]

I updated the generated goal from forall a b, a \in supp(d1) => b = g(a) => psi[x -> a, y -> b] to forall a, a \in supp(d1) => psi[x -> a, y -> g(a)]. The reason for this change is as follows: I found that the default substitution API automatically uses let-binding when at least two substitutions are needed for the same pattern, which already satisfies the readability target for this unnecessary b = g(a).

[oskgo]

Apparently there's a github bug where a change request sticks around if you make changes before resolving them.

Reviewers with write access should feel free to dismiss mine now.

Change made before it was requested.