Email Gateway (Aug 22 2022 at 17:53): Email Gateway (Aug 22 2022 at 17:53):From: John Matthews <john_matthews@apple.com>
We've noticed some unintuitive Isar behavior when we have an identity proof step within a chain of “also have” calculations.
For example, the proof below succeeds that has the identity proof step commented out:
lemma "(1::nat)+2+3 = 6"
proof -
have "(1::nat)+2+3 = 3+3" by arith
(* also have "... = 3+3" .. -- "identity proof step" *)
also have "... = 6" by arith
finally show "(1::nat)+2+3 = 6" .
qed
However with that line enabled then the "finally show” proof step fails two lines later. We were expecting either for the "finally show" proof step to succeed or else for Isar to report an error at the identity proof step itself. Note that identity proof steps may not be obvious to the user in the presence of complex term abbreviations.
Thanks,
John
Email Gateway (Aug 22 2022 at 17:53):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Also mysterious to the uninitiated are situations in which the chain of terms
contains a nontrivial loop; i.e. the repeated term occurs not in the immediate
next step, but in a later one. In that case, an "also" in the proof can loop
(visually, turns purple and stays that way). I don't know if this always happens;
it seems that sometimes there is no visual indication of the problem. With a
visual indication, it is usually more clear that something is wrong, but when
I first encountered this behavior I had no idea what was happening. An explicit
check for loops in the calculation, with an error report to the user, would be
very helpful.
Email Gateway (Aug 22 2022 at 17:53):From: Dominique Unruh <unruh@ut.ee>
Dear John,
the also-finally mechanism works as follows (in the example including the
identity proof step):
- There is a variable "calculation" that contains the intermediate
conclusion of the chain of the equations. Initially, this variable is empty.
- The first "also" sets calculation := "1+2+3=3+3", because it was empty
before, and the last proven fact was "1+2+3=3+3"
- The second "also" takes the current content of calculation (1+2+3=3+3)
and the last proven fact (3+3=3+3) and tries to apply some transitivity
rule to it.
The obvious choice would, of course, be the rule "a=b ==> b=c ==> a=c",
and that would give us calculation := 1+2+3=3+3.
- However, in this special case, there are other transitivity rules that
also match (you get the full list with print_trans_rules):
For example, there is the rule "a = b ⟹ P b ⟹ P a". This rule matches
the current situation, instantiated with a:=1+2+3, b:=3+3, and P:="λx. x=x".
The conclusion of the rule is then 1+2+3=1+2+3. This is then stored in
calculation (you can check this in jEdit by clicking on the work also and
looking at the output panel). (So here is where things went wrong.)
- The finally command applies the same mechanism as also (except that it
does not store the result in calculation but makes it available to the show
command as a fact).
But in the present case, we have "1+2+3=1+2+3" and "3+3=6", there is no
rule that can combine those. Thus "finally" fails (not show!).
I don't know if there is a way to solve this. (The only way I see would be
to have priorities on trans-rules, so that the "a=b ==> b=c ==> a=c" rule
is always tried first but that sounds like a bigger chance in the
mechanism.)
Best wishes,
Dominique.
Last updated: Apr 27 2024 at 01:05 UTC