Peter Lammich
2018-08-02 15:50:31 UTC
Hi List,
is there any particular reason why the ";" method combinator and the
more low-level THEN_ALL_NEW tactical process the new goals in a
backward fashion (except that implementing the backwards direction is
slightly more convenient).
This backwards-direction tends to get counter-intuitive quite often in
my use-case of VCG-rules. There, it is often important in which order
the new subgoals are solved, and forward-direction is much more
intuitive. For example, consider a rule with frame-inference from
separation logic:
C |- array l a * F i < length l
--------------------------------------
{ C } a[i] := x { array (l[i:=x]) a * F }
When applying this rule, the two subgoals will contain some schematic
variables ?l and ?F. When, e.g., inside Eisbach, I now use ; to solve
the produced goals, it will try to solve "i < length ?l" first. This is
not possible, or might even result in silently instantiating ?l
wrongly.
This is just a simple example, and when rules get more complex, writing
them down with reversed assumptions can really obfuscate what is going
on, as one starts to think of the rules in a "computational" way, where
each preconditions "computes" the values of a schematic variable. A
basic example for this is the seq-comp rule
{ P } a { Q } { Q } b { R }
--------------------------------
{ P } a;b { R }
in a forward-style VCG, the assumptions of this rule need to be
reversed in order to use ";".
So what are the deeper reasons that we have a backward ";" rather than
a forward ";", or why not simply have both?
--
Peter
p.s.
implementing THEN_ALL_NEW_FWD and REPEAT_ALL_NEW_FWD tacticals is
straightforward, but the Isar method combinator syntax is hardwired,
such that I cannot simply define a new one, say "method1;; method2" or
"method1;\<^sub>f method2"
The only thing that works is a long name, e.g.,
then_all_new_fwd <method1> <method2>
which is inconvenient and makes Eisbach style method definitions
unreadable, e.g. (a;b;c) vs
then_all_new_fwd <a> <then_all_new_fwd <b> <c>>
pps.
another workaround might be a reverse_assumptions attribute, that
reverses the assumptions of a theorem, and is applied to any rule
before resolving with it, e.g.
(rule vcg_rules[reverse_assumptions]; solve_preconds)
is there any particular reason why the ";" method combinator and the
more low-level THEN_ALL_NEW tactical process the new goals in a
backward fashion (except that implementing the backwards direction is
slightly more convenient).
This backwards-direction tends to get counter-intuitive quite often in
my use-case of VCG-rules. There, it is often important in which order
the new subgoals are solved, and forward-direction is much more
intuitive. For example, consider a rule with frame-inference from
separation logic:
C |- array l a * F i < length l
--------------------------------------
{ C } a[i] := x { array (l[i:=x]) a * F }
When applying this rule, the two subgoals will contain some schematic
variables ?l and ?F. When, e.g., inside Eisbach, I now use ; to solve
the produced goals, it will try to solve "i < length ?l" first. This is
not possible, or might even result in silently instantiating ?l
wrongly.
This is just a simple example, and when rules get more complex, writing
them down with reversed assumptions can really obfuscate what is going
on, as one starts to think of the rules in a "computational" way, where
each preconditions "computes" the values of a schematic variable. A
basic example for this is the seq-comp rule
{ P } a { Q } { Q } b { R }
--------------------------------
{ P } a;b { R }
in a forward-style VCG, the assumptions of this rule need to be
reversed in order to use ";".
So what are the deeper reasons that we have a backward ";" rather than
a forward ";", or why not simply have both?
--
Peter
p.s.
implementing THEN_ALL_NEW_FWD and REPEAT_ALL_NEW_FWD tacticals is
straightforward, but the Isar method combinator syntax is hardwired,
such that I cannot simply define a new one, say "method1;; method2" or
"method1;\<^sub>f method2"
The only thing that works is a long name, e.g.,
then_all_new_fwd <method1> <method2>
which is inconvenient and makes Eisbach style method definitions
unreadable, e.g. (a;b;c) vs
then_all_new_fwd <a> <then_all_new_fwd <b> <c>>
pps.
another workaround might be a reverse_assumptions attribute, that
reverses the assumptions of a theorem, and is applied to any rule
before resolving with it, e.g.
(rule vcg_rules[reverse_assumptions]; solve_preconds)