Email Gateway (Aug 19 2022 at 14:55): Email Gateway (Aug 19 2022 at 14:55):From: Vadim Zaliva <vzaliva@cmu.edu>
I am learning Isar and have another naive question on the syntax:
I am trying to do something like this in Isar:
1: lemma
2: shows "not something"
3: proof(rule ccontr)
4: assume "something"
5: thus False proof cases
6: ...
7: qed
8: qed
and get "*** Failed to refine any pending goal" error around line 5
Why this does not work? Something like this works instead:
lemma
shows "not something"
proof
assume "something"
hence False proof cases
...
qed
thus False by simp
qed
But last statement (thus False by simp) seems to be unnecessary, as it is proving
False from False!
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 14:55):From: Timothy Bourke <tim@tbrk.org>
You want rather
lemma "¬ something"
proof (rule notI)
assume "something"
thus False
sorry
qed
Typing "find_theorems intro" after line 2 gives a list of applicable
rules. But, in fact, in this case Isar finds the right rule by itself:
lemma "¬ something"
proof
assume "something"
thus False
sorry
qed
Tim.
signature.asc
Email Gateway (Aug 19 2022 at 14:55):From: Lars Noschinski <noschinl@in.tum.de>
On 17.07.2014 00:00, Vadim Zaliva wrote:
I am learning Isar and have another naive question on the syntax:
I am trying to do something like this in Isar:1: lemma
2: shows "not something"
3: proof(rule ccontr)
4: assume "something"
5: thus False proof cases
6: ...
7: qed
8: qed
Have a look ath the proof state after "proof (rule ccontr)". The
precondition is "~~ something". Your assumption "something" does not
unify with this, so you get an error message as soon as you try to
discharge a proof obligation with show (or thus).
(Actually, it would be nice if the system would actually warn you about
this probable error at the assume statement).
You can either assume "~~something", or -- which is nicer -- do not use
the rule "ccontr" here. You just need "notI" (which is actually the
default rule, so changing line 3 to just "proof" should make everything
go through).
and get "*** Failed to refine any pending goal" error around line 5
Why this does not work? Something like this works instead:
lemma
shows "not something"
proof
assume "something"
hence False proof cases
...
qed
thus False by simp
qed
The important difference is not the split into hence/thus (which is
indeed entirely unnecessary), but "proof (rule ccontr)" vs just "proof"
(which is equivalent here to "proof (rule notI)".
Have a look at both rules by doing "print_statement ccontr notI".
Best regards, Lars
Email Gateway (Aug 19 2022 at 14:55):From: Vadim Zaliva <vzaliva@cmu.edu>
Thanks! That helps. The reason I used "something" instead of "~~something"
in the assumption is to be able to use simpler cases syntax as my "something"
is inductive definition:
inductive something :: .... where
C1: ... |
C2: ...
If I am proving "something" I can write "proof cases". If I proving ~~something
I have to write proof (cases something).
I do not know what is involved implementation-wiser but it would be nice if Isabelle could deal with
trivial double negation during unification.
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 14:55):From: Tobias Nipkow <nipkow@in.tum.de>
I have often toyed with the idea of unification modulo certain equations but
implementation-wise it is subtle and means modifying an already convoluted part
of the core. Don't hold your breath.
Tobias
Email Gateway (Aug 19 2022 at 14:55):From: Joachim Breitner <breitner@kit.edu>
Hi,
it would be very helpful, especially for beginners, but often also for
me, if a "proof" would tell us what rule it applied – similar to how
"also" tells us what the current calculation is.
(And while are are at it: "also" could also tell us what rule it
used...)
Such features give great insight into the system and give the users more
confidence in using it.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:56):From: Lars Noschinski <noschinl@in.tum.de>
I agree. If I remember correctly, a crude form of that is provided by the rule_trace option.
Joachim Breitner <breitner@kit.edu> schrieb:
Email Gateway (Aug 19 2022 at 14:56):From: Lars Noschinski <noschinl@in.tum.de>
As a side remark, if you are doing "unstructured" case analysis (i.e.,
there is not directly a rule matching your goal/assumptions and the
desired analysis), one way to write this is the following:
{ assume P1
have Q ... }
moreover
{ assume P2
have Q ...}
moreover
{ assume P3
have Q ...}
ultimately
have Q ...
Usually, blast or metis is then a good method to discharge the final
obligation.
Email Gateway (Aug 19 2022 at 15:04):From: Makarius <makarius@sketis.net>
The rules (and their instances) that are actually used are not immediately
tracable, due to the way the traditional lazy enumeration of potential
results works.
I have often reconsidered that, but the only reform that went through in
recent years was better error reporting in the absence of results --
instead of just "empty result sequence". Thus users merely need to look
at the error message of some failed "by ..." command or calculational
step. Funnily, seasoned users stick to older habits to ignore the error
and turn a failed "by" into "apply" and then watch the Output window.
There is now also a tiny reform in the printing of 'also' / 'finally'
for Isabelle2014 -- to discontinue some old workarounds for TTY
interaction.
Makarius
Email Gateway (Aug 19 2022 at 15:04):From: Joachim Breitner <breitner@kit.edu>
Hi,
I try to use the "by" output, but I fail because
a) it sometimes shows up below “have ..” and below “proof”. Before I
reach for the mouse (repeatedly, as I change my proof), I rather change
the by to apply.
b) the red background is unpleasant to read. It makes me nervous. It
should be reserved for proper alerting. I need to be alerted once that
it’s broken, but I don’t need to be continuously alerted while working
on it.
The second point is a bit of a psychological one and might not affect
other users. OTOH, UI is nothing but psychology, so it seems to be
relevant here.
With best regards,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:04):From: Makarius <makarius@sketis.net>
On Fri, 25 Jul 2014, Joachim Breitner wrote:
a) it sometimes shows up below “have ..” and below “proof”. Before I
reach for the mouse (repeatedly, as I change my proof), I rather change
the by to apply.
I will take a second look. That non-determinsm is probably just an
accidental side-effect of generally reworked asynchronous printing in
Isabelle2014-RC0.
b) the red background is unpleasant to read. It makes me nervous. It
should be reserved for proper alerting. I need to be alerted once that
it’s broken, but I don’t need to be continuously alerted while working
on it.
So why not change the color in Plugin Options / Isabelle / Rendering?
You should keep it somehow visible, though, otherwise the following
incident might happen:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-May/msg00037.html
Makarius
Email Gateway (Aug 19 2022 at 15:05):From: Lars Noschinski <noschinl@in.tum.de>
Because I want to see the bad color in the edit window, but not (as
strong) in the output window.
Last updated: Nov 21 2024 at 12:39 UTC