Email Gateway (Aug 18 2022 at 17:29): Email Gateway (Aug 18 2022 at 17:29):From: Makarius <makarius@sketis.net>
The treatment of chained facts by "rule" is inherent in the way how Isar
really works. Part of the confusion stems from the very liberal language
design which also admits many "improper" elements in the same language.
If you really want to understand structure Isar proofs, not proof scripts,
you need to become acquainted with Isar rule composition.
Makarius
Email Gateway (Aug 18 2022 at 17:29):From: Makarius <makarius@sketis.net>
On Sun, 3 Apr 2011, Jun Inoue wrote:
I was trying "by (-, rule foo)", but now I see why that was no good.
:)For the record, if anyone reads this in the archives: "by - (rule foo)"
performs two separate method calls, a no-op and (rule foo), which
automatically induces a "stick assumptions into the premises" step in
between, whereas "by (-, rule foo)" performs one call to a single,
composite method which does nothing special in between the no-op and
(rule foo).
Yes, the initial proof method of 'by' is just one big expressen, where
every participant receives the same facts. You often see this mistake in
the sources:
by (method1, method2)
where it really should be
by method1 method2
e.g.
by cases auto
It is also a bit inconvenient that there is no single method that has
the "insert chained facts, then apply a rule" behavior; but at least
there is an easy workaround with "-" followed by "rule".
Isar is about structure, but here it would get lost in the dark goal
state. You can use rule_tac as workaround, but then you are really
stepping outside proper Isar.
but if the authors of the Isabelle Tutorial ever see this, please
consider making a little note of this behavior of "rule" in Section 5.7
(or maybe in the "Structured Proofs in Isar/HOL" document). Clearly
pointing out the general difference between assumptions and premises
could be even better...
The manuals are not really up to date. I hope to be able to work again on
a proper Isar tutorial for structured proofs.
I did not understand what you mean by "general difference between
assumptions and premises".
Probably there is again a confusion by taking the printed goal state too
seriously -- which is very confusion indeed.
Makarius
Email Gateway (Aug 18 2022 at 17:29):From: Makarius <makarius@sketis.net>
"by blast" and "by - blast" should be always the same.
Since blast is a "simple method" it first uses "insert" to dump the facts
into the goal state and then tries its luck on the result.
Makarius
Email Gateway (Aug 18 2022 at 17:30):From: Makarius <makarius@sketis.net>
Actually you can have a difference if the goal state has > 1 subgoals,
e.g. like this:
notepad
begin
assume B
then have "A --> A" and B by - blast
end
Here the "dumping" of facts is only weakly structured: all subgoals are
augmented uniformly. The "blast" then solves the first, while the other
is implicitly closed as trivial in the end.
The defaults of the Isar language attempt to maximize proof structure,
e.g. one should not attempt to escape from that without good reasons.
Makarius
Email Gateway (Aug 18 2022 at 17:30):From: Brian Huffman <brianh@cs.pdx.edu>
On Mon, Apr 4, 2011 at 1:27 AM, Makarius <makarius@sketis.net> wrote:
On Sun, 3 Apr 2011, Jun Inoue wrote:
I was trying "by (-, rule foo)", but now I see why that was no good. :)
For the record, if anyone reads this in the archives: "by - (rule foo)"
performs two separate method calls, a no-op and (rule foo), which
automatically induces a "stick assumptions into the premises" step in
between, whereas "by (-, rule foo)" performs one call to a single, composite
method which does nothing special in between the no-op and (rule foo).Yes, the initial proof method of 'by' is just one big expressen, where every
participant receives the same facts.
By anyone's standard, I would be considered an "expert" Isabelle
user... and in my years of experience with Isar I never knew this! How
did that happen?
You often see this mistake in the
sources:by (method1, method2)
where it really should be
by method1 method2
Now that I think about it, I can remember many situations where I had
written something like
by (method1, rule foo, method 2)
and it failed for some reason that I didn't understand. Now it makes sense.
Unfortunately, my usual first reaction was to rewrite this as
apply - by (method1, rule foo, method 2)
making it less structured, instead of as
by method1 (rule foo, method 2)
which I suppose would be considered more "proper".
How are average users expected to learn these things?
Email Gateway (Aug 18 2022 at 17:30):From: Makarius <makarius@sketis.net>
On Mon, 4 Apr 2011, Brian Huffman wrote:
By anyone's standard, I would be considered an "expert" Isabelle user...
and in my years of experience with Isar I never knew this! How did that
happen?
There is no problem with that. In general there are many very delicate
points in Isar, but it is partly successful since it can be used without
going to the bottom of every detail. Instead, the usual way is to imitate
"best-style" proofs. Unfortunately, not all examples in the libraries are
good ones.
How are average users expected to learn these things?
By being lucky in the selection of manuals or chosing the teacher. This
very issue of "initial method" vs. "terminal method" should also have been
mentioned quite often on the mailing list.
Since a couple of years, my tendency is to make the system guide users
more explicitly (e.g. in the Prover IDE), although I can also foresee lots
of complaints about such tutelage ...
Makarius
Email Gateway (Aug 18 2022 at 17:31):From: Jun Inoue <jun.lambda@gmail.com>
Hi, I'm having trouble understanding how the rule/erule method interacts
with the subtle difference between `this' and ==>. Given an
introduction rule
P
-
Q
and a goal state with a chained fact
(* call this state 1 *)
using this:
R
goal:
Q
the tutorial says the rule method unifies only the Q's, but it appears
to be matching P to R as well, failing if they don't match. But if the
goal state were
(* call this state 2 *)
(`this' is empty)
goal:
R ==> Q
then no matching seems to happen between P and R, and the method
succeeds. I'm including a minimal concrete example below. A similar,
but opposite, thing seems to happen with erule, which appears to
(sometimes? always?) neglect chained facts when it searches for
formulas to consume.
So exactly which combinations of formulas do rule and erule unify?
Where could I have found this information?
When I have state 1, how do I massage it into state 2 so that I can
invoke rule without unifying the rule's premises to anything, or erule
with unification to `this'? Why wouldn't Isabelle do this massaging for
me?
(* Example: P = "n \<le> 1", Q = "n \<noteq> 2", and R = "n = 0". *)
lemma the_rule_assm:
fixes n :: int
assumes "n \<le> 1"
shows "n \<noteq> 2"
using assms by arith
(* The way the rule is declared makes no difference, as expected. *)
lemma the_rule_imp:
fixes n :: int
shows "n \<le> 1 \<Longrightarrow> n \<noteq> 2"
by arith
(* The way the theorem to prove with the rule is declared does make
a difference, as is highly unexpected. *)
theorem test_assm:
fixes n :: int
assumes "n = 0"
shows "n \<noteq> 2"
using assms
(* Unification fails using either of the rules defined above,
apparently trying to match n \<le> 1 with n = 0". *)
(apply (rule the_rule_assm) ( Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
(* apply (rule the_rule_imp) (* Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
oops
(* The same rules work, apparently without trying to
unify n \<le> 1 with n = 0, if the lemmas are stated
this way. *)
theorem test_imp:
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_assm) (* works *)
oops
theorem test'':
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_imp) (* works *)
oops
Email Gateway (Aug 18 2022 at 17:32):From: Brian Huffman <brianh@cs.pdx.edu>
On Fri, Apr 1, 2011 at 10:09 AM, Jun Inoue <jun.lambda@gmail.com> wrote:
(* call this state 1 *)
using this:
R
goal:
Q
[...]
(* call this state 2 *)
(this' is empty) goal: R ==> Q [...] When I have state 1, how do I massage it into state 2 so that I can invoke rule without unifying the rule's premises to anything, or erule with unification tothis'?
Hi Jun,
This particular question, at least, has an easy answer: just use
"apply -", i.e. use the method whose name is just a single hyphen. Its
only effect is to add any chained facts to the goal as ordinary
assumptions. It is often used in structured proofs with "proof -",
where it is usually a no-op. Another pattern that you can find in the
sources is "by - (rule foo, simp)" or similar. I have also used "by -
(rule exI)" in several places in HOLCF where "by (rule exI)" fails for
some reason.
It is a bit confusing how "rule" treats chained facts in a special
way, when nearly all other methods start by adding any chained facts
into the goal as premises before continuing with their normal
behavior. It is also a bit inconvenient that there is no single method
that has the "insert chained facts, then apply a rule" behavior; but
at least there is an easy workaround with "-" followed by "rule".
(* The way the theorem to prove with the rule is declared does make
a difference, as is highly unexpected. *)
theorem test_assm:
fixes n :: int
assumes "n = 0"
shows "n \<noteq> 2"
using assms
(* Unification fails using either of the rules defined above,
apparently trying to match n \<le> 1 with n = 0". *)
(apply (rule the_rule_assm) ( Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
(* apply (rule the_rule_imp) (* Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
oops(* The same rules work, apparently without trying to
unify n \<le> 1 with n = 0, if the lemmas are stated
this way. *)
theorem test_imp:
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_assm) (* works *)
oopstheorem test'':
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_imp) (* works *)
oops
The theorem list "assms" only includes propositions listed in
"assumes" clauses. Since there are no "assumes" clauses in either of
the last two theorems, "assms" is actually empty, so there are no
chained facts, and "rule" doesn't try to unify with any assumptions.
Email Gateway (Aug 18 2022 at 17:35):From: Jun Inoue <jun.lambda@gmail.com>
Brian Huffman <brianh@cs.pdx.edu> writes:
On Fri, Apr 1, 2011 at 10:09 AM, Jun Inoue <jun.lambda@gmail.com> wrote:
(* call this state 1 *)
using this:
R
goal:
Q
[...]
(* call this state 2 *)
(this' is empty) goal: R ==> Q [...] When I have state 1, how do I massage it into state 2 so that I can invoke rule without unifying the rule's premises to anything, or erule with unification tothis'?Hi Jun,
This particular question, at least, has an easy answer: just use
"apply -", i.e. use the method whose name is just a single hyphen. Its
only effect is to add any chained facts to the goal as ordinary
assumptions. It is often used in structured proofs with "proof -",
where it is usually a no-op. Another pattern that you can find in the
sources is "by - (rule foo, simp)" or similar. I have also used "by -
(rule exI)" in several places in HOLCF where "by (rule exI)" fails for
some reason.
Hi Brian, thanks for the tip! I was trying "by (-, rule foo)", but now
I see why that was no good. :)
For the record, if anyone reads this in the archives: "by - (rule foo)"
performs two separate method calls, a no-op and (rule foo), which
automatically induces a "stick assumptions into the premises" step in
between, whereas "by (-, rule foo)" performs one call to a single,
composite method which does nothing special in between the no-op and
(rule foo).
It is a bit confusing how "rule" treats chained facts in a special
way, when nearly all other methods start by adding any chained facts
into the goal as premises before continuing with their normal
behavior. It is also a bit inconvenient that there is no single method
that has the "insert chained facts, then apply a rule" behavior; but
at least there is an easy workaround with "-" followed by "rule".
I tripped over this separation between assumptions before, when I found
that "show" doesn't unify exported premises with any pending goal's
premises but only assumptions with goals' premises. Why does Isar have
this (IMHO idiosyncratic) distinction between assumptions and premises?
I suppose it's there for a reason, but to me it seems like Isar would be
more streamlined and novice-friendly if the two notions are identified,
or always automatically bridged.
PS. Not to be too nosy here, but if the authors of the Isabelle
Tutorial ever see this, please consider making a little note of this
behavior of "rule" in Section 5.7 (or maybe in the "Structured Proofs in
Isar/HOL" document). Clearly pointing out the general difference
between assumptions and premises could be even better...
(* The way the theorem to prove with the rule is declared does make
a difference, as is highly unexpected. *)
theorem test_assm:
fixes n :: int
assumes "n = 0"
shows "n \<noteq> 2"
using assms
(* Unification fails using either of the rules defined above,
apparently trying to match n \<le> 1 with n = 0". *)
(apply (rule the_rule_assm) ( Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
(* apply (rule the_rule_imp) (* Clash: HOL.eq =/= Orderings.ord_class.less_eq ))
oops(* The same rules work, apparently without trying to
unify n \<le> 1 with n = 0, if the lemmas are stated
this way. *)
theorem test_imp:
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_assm) (* works *)
oopstheorem test'':
fixes n :: int
shows "n = 0 \<Longrightarrow> n \<noteq> 2"
using assms
apply (rule the_rule_imp) (* works *)
oopsThe theorem list "assms" only includes propositions listed in
"assumes" clauses. Since there are no "assumes" clauses in either of
the last two theorems, "assms" is actually empty, so there are no
chained facts, and "rule" doesn't try to unify with any assumptions.
- Brian
Email Gateway (Aug 18 2022 at 17:36):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
I agree. At the very least, this is non-obvious. I still get caught by
this occasionally. I've trained myself that rule/erule/drule and
assumption require the use of - first, while auto and (clar)simp do not.
I still remain surprised whenever I have to replace "by blast" with "by
While I suppose I could just go around using auto and metis everywhere,
I don't think that's necessarily a good idea, as it miscommunicates to
the reader/maintainer how involved the proof step is. I will use
assumption when that's all that's needed, blast when there's no
simplification needed, and prefer simp over auto.
Anyway, my proposal would be to add an implicit "-" to blast and any
official tactic that can finish a proof, and document in the tutorial
and reference the fact that rule/erule/drule (and whatever else) don't
do this, like Jun suggested.
Sincerely,
Rafal Kolanski.
Last updated: Nov 21 2024 at 12:39 UTC