Email Gateway (Aug 18 2022 at 15:07): Email Gateway (Aug 18 2022 at 15:07):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Just out of curiosity:
1) Why does the method assumption restrict the given facts to 0 or 1?
2) Why does 'by this' seem to do the same thing? Example: Since I am
using exclusively Isar for proves, I accustomed myself to state lemmas as
lemma
assumes "A" and "B" shows "C"
rather than as
lemma "A ==> B ==> C"
Now, e.g.,
lemma "A ==> B ==> A" .
lemma "A ==> B ==> A" by assumption
both works. When 'Isarfying' the lemma a bit more, like
lemma assumes "A" shows "B ==> A"
using assms .
lemma ssumes "A" shows "B ==> A"
using assms by assumption
it is still working. But with
lemma assumes "A" and "B" shows "A"
it doesn't work any longer. Wouldn't it be nice, to have a short way of
proving such simple statements (where one of the current facts solves
the goal). E.g.,
lemma assumes "A" and "B" shows "A' using assms .
And indeed, isn't that, what the documentation claims? In isar-ref.pdf
on page 88, I read "this applies all of the current facts directly as
rules."
cheers
chris
Email Gateway (Aug 18 2022 at 15:08):From: Brian Huffman <brianh@cs.pdx.edu>
I think the documentation means to say that "." can use multiple facts
to prove multiple goals. Here's an example:
lemma
assumes "A" and "B"
shows "B" and "A"
proof -
from assms show "A" and "B" .
qed
By the way, you can get a fairly short proof using "rule", like this:
lemma assumes "A" and "B" shows "A" by (rule assms)
Of course, this relies on having a named set of facts. To use the
chained facts in this way you would need something like
have "A" and "B" by ...
note foo = this
show "A" by (rule foo)
which isn't quite as nice. I agree that a proof method with the
semantics you described would be useful. It probably wouldn't take too
much code to implement; why don't you try writing one?
Email Gateway (Aug 18 2022 at 15:08):From: Makarius <makarius@sketis.net>
The above gives you a goal A and rules A and B which are all applied
as rules (in the order of the text). After the first rule application,
there are no goals left, so the attempt to apply B fails. Example
situations where several rules actually can be applied: multiple goals, or
single goals with facts that have premises.
The general idea of proper Isar proof methods (as opposed to
semi-automated tools like "simp", or old tactic emulations like
"rule_tac") is to try to take the given structure of the problem
seriously. The aim is to get a text that faithfully represents the
reasoning, not to accept as much as possible.
For example
from A and B have A by this
reads to me like both A and B somehow contribute to the result, not that
the second one is silently ignored. In practice there are many corner
causes of proof methods, and often one could define certain fine points
one way or the other, such as "this" vs. "assumption". On the spot, I do
not recall all the details that lead up all details in basic Isar methods
-- it always takes several rounds of in-depth studies of various
mechanisms to make things fit together in the end.
Anyway, using "assumption" like methods for trivial proofs is slightly
old-style since the "fact" method has come up some years ago. E.g. this
works:
lemma assumes "A" and "B" shows "A' by fact
Here the implicit scope for trivial facts is the whole of the visible
proof text. You can also use (fact my_facts) to limit the scope
explicitly.
Makarius
Last updated: Apr 18 2024 at 16:19 UTC