Tactic: add hoare split

[strub]

Introduce a new Hoare-only tactic hoare split that decomposes goals with conjunctive postconditions into independent Hoare goals.

It is intentionally restricted to Hoare logic, where this rule is sound.

[oskgo]

The hoare case can be done outside the TCB using conseq:

 require import AllCore.

   module M = {
     proc incr(x : int) : int = {
       var y : int;
       y <- x + 1;
       return y;
     }
   }.

   lemma L (n : int) : 0 <= n =>
     hoare [M.incr : x = n ==> n < res /\ 0 <= res].
   proof.
     move=> ge0_n; proc.

     (*$*) (* Split the conjunctive postcondition *)
     conseq (_: _ ==> n < y) (_: _ ==> 0 <= y); 1:done.

[fdupress]

There is still value in considering a high-level (non-TCB) tactic that infers the split postconditions and internally produces the conseq-based proof. But I tend to agree that this does not need to be TCB if we already have conseq in-TCB.

As an aside, I think we could generalize this to split all program-independent products that sit at the head of the postcondition (including universal quantification, and implications whose LHS does not use program variables).

[strub]

Ok. Will move it outside the TCB, I should have seen that.

But the tactic (that is going to have more complex inference mechanism) allows better proof edition.

[strub]

Done. As a side note, the internal API for conseq is a non-sense and has to be rewritten.

[oskgo]

The docs say that it should be splitting apart conjunctions recursively ("one for each conjunct"), but the implementation doesn't do that.

[strub]

The docs say that it should be splitting apart conjunctions recursively ("one for each conjunct"), but the implementation doesn't do that.

@oskgo Why do you think this sentence implies recursion?

[oskgo]

@strub Suppose the postcondition is a /\ b /\ c. I think most people when asked to list all the conjuncts are going to answer a, b and c rather than a and b /\ c.

If the intention is to just split apart one instance of the binary /\ operator this should be made clearer.

[strub]

@oskgo Ok. What about "top-level conjunction"?