feat: variant for up-to-bad call/proc tactics

[loutr]

The premise:

∀O. is_lossless O => is_lossless A(O)         (1)

of the current up-to-bad tactics happens to be too restrictive in some cases. At first glance, it seems that it would be possible to allow another variant of the tactic that instead requires

is_lossless A(O_1) ∧ is_lossless A(O_2)       (2)

(possibly as two differents subgoals), which can be proved in some concrete instances of A, O_1, O_2, while (1) is not.

Simply introducing a variant of the tactic that replaces (1) with (2) is not satisfactory and is not ensured to be sound.

This is because commit 6534f3d (yes, some archeology was required) changed the premises of this tactic, which implicitly changes the proof of soundness of the tactic.

This PR provides a way to use a different set of premises, which restores the original conditions required for applying up-to-bad tactics, as well as changes condition (1) with (2) (which is the original goal).

Some issues still need to be addressed w.r.t. parsing. Introducing a variant syntax in the spirit of call @[weaker_pre] causes shift/reduce conflicts.

---

This is a duplicate of PR #1055 that was incorrectly targeting the main branch of my fork. This is an error on my side.

[strub]

@loutr

This is a duplicate of PR #1055 that was incorrectly targeting the main branch of my fork. This is an error on my side.

You can always change the target branch (when editing the title, the target branch can be changed)

[strub]

In order to have a sound variant of the tactic

I thought that the previous tactic was still sound. If not, this is not a variant that should be introduced. We should get rid of the previous one.

[fdupress]

The previous tactic is still sound as it is. But weakening only the equitermination goal does not yield a sound generalisation of the existing rule as implemented, because that one weakens the "preservation of bad" goals.

At the moment, we need to keep both. It also seems pretty clear (but not obvious) that all existing proofs could be adapted to work with this new rule, but it is not going to be a simple job. So we decided to keep both while we figure out how to use this one in general.

[strub]

The previous tactic is still sound

@loutr Could you fix the description?

[strub]

Take the opportunity to use a record.

[loutr]

@loutr

This is a duplicate of PR #1055 that was incorrectly targeting the main branch of my fork. This is an error on my side.

You can always change the target branch (when editing the title, the target branch can be changed)

Unfortunately no, upon editing the title of the PR it is only possible to change what GitHub calls the "base branch" of the PR, that is, the branch in this repo that should receive the changes. I wanted to change the "target branch" of the PR, which is a branch of my fork (loutr:1055-uptobad-variant) that was incorrectly set to loutr:main, which cannot be changed..

In order to have a sound variant of the tactic

Also, I changed the description. This sentence was in the original commit message because we had strong doubts with Benjamin that the tactic with its modified premises was sound at all. The pen-and-paper proof we found only dealt with the base tactic. We had to convince ourselves with a new proof. (But maybe there was a proof of this modified tactic somewhere, we just did not find it.)

[oskgo]

I wouldn't be surprised if existing proofs can be adapted to this new tactic, but as far as I understand it is not strictly stronger than the old tactic. The old tactic allows oracles that do not terminate as long as they are equiterminating before bad and terminating after. AFAIU the new rule requires strict termination before bad as well.

[loutr]

Exactly, neither the existing rule or this new variant imply the other, which is why it is being introduced as a variant that one can call with proc @[ll] .., instead of a replacing the existing rule.