feat: variant for up-to-bad call/proc tactics#1060
Conversation
loutr
force-pushed
the
1055-uptobad-variant
branch
from
c6c0467 to
1bdb190
Compare
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. |
|
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. |
@loutr Could you fix the description? |
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.
In order to have a sound variant 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).
strub
force-pushed
the
1055-uptobad-variant
branch
from
1bdb190 to
43ba638
Compare
|
|
||
| and pspattern = unit | ||
|
|
||
| type fun_upto_info = bool option * pformula * pformula * pformula option |
There was a problem hiding this comment.
Take the opportunity to use a record.
3 participants
The premise:
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
(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.
In order to have a sound variant 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.