New high-level tactic: 2-sided rcond/match

[fdupress]

When reasoning about equivalences of control-flow-heavy pWhile programs, it is often the case that one wants to simultaneously prove that two conditionals have equivalent conditions AND that those conditions are both true. Currently, the best proof pattern that allows me to do this without simply repeating the proof that the condition reduces to a specific value is:

• sp i j to immediately before the condition to be reduced;
• if then discharge the (first) condition (on equivalence of the condition expression); and
• exfalso on the dead proof branch.

This pattern could be supported at top-level as a high-level tactic implemented out of TCB.

This might be a good first issue to get in to the high-level code base.

[fdupress]

The description given above is very wrong: this reduces both conditions with a single proof, but it also eats the prefix.

Ideally, we'd like a tactic that, given a proof of (EQ) {P} c1 ~ c2 {={b}} and a proof of (L) forall &2, {P} c1 {b} (perhaps given as a single goal?) reduces proving {P} c1; if b then c1_t else c1_e; c1_f ~ c2; if b then c2_t else c2_e; c2_f {Q} to proving {P} c1; c1_t; c1_f ~ c2; c2_t; c2_f {Q}.

This is not something that can be implemented at as high a level as the one described above, as far as I can see—in the sense that I cannot come up with a valid template to produce an externally valid EasyCrypt proof from those components. (In particular, there is no externally usable tactic that allows one to conclude forall &1, {P} c2 {b} from (EQ) and (L). But maybe there is an easily usable internal tactic for this?)