Email Gateway (Aug 22 2022 at 19:09): Email Gateway (Aug 22 2022 at 19:09):From: Gidon Ernst <gidon.ernst@unimelb.edu.au>
Hi all,
I have feedback wrt. documentation and a question (I guess a feature request).
Sorry if these points have been raised before.
I really like obtains in lemmas with the ability to specify multiple cases.
It helped to streamline my Isar proofs a lot and I think it should be advertised more in the documentation.
The documentation could be more explicit about the fact(s) "that" which you can use to prove such lemmas (e.g. in Sec 2.2.2), as I found out about it accidentally via sledgehammer only (it is mentioned in fact somewhere at the very end of the manual, but hard to spot).
Also, I'd note that "that" in an inductive lemma
assumes A obtains B using A proof (induction ...)
refers to the outer context, not the properly generalized one, and is therefore useless. Could this be fixed somehow?
Secondly, how about a similar construct for introduction rules?
Applying an introduction lemma for C
assumes a: "!!x. A ==> B" shows C
could generate a structure comparable to a cases rule that does the "fix x assume a: A show B" for you, possibly extending to multiple assumptions.
Is there a mechanism for this? It would amount to multiple "case ..." with different conclusions, which I understand does not work currently.
Thanks a lot and best regards,
Gidon
Email Gateway (Aug 22 2022 at 19:11):From: Makarius <makarius@sketis.net>
On 13/02/2019 10:12, Gidon Ernst wrote:
I really like obtains in lemmas with the ability to specify multiple cases.
Note that in a proof body you have a few more such structuring
principles for statements: "have C if A for x", "consider A | B | C",
and then "obtain x where A" as a special case.
The "that" fact shows up here as well: historically 'obtains' was first,
but I have retrofitted it into this general setup a few years ago.
Also, I'd note that "that" in an inductive lemma
assumes A obtains B using A proof (induction ...)
refers to the outer context, not the properly generalized one, and is therefore useless. Could this be fixed somehow?
A proof method mainly operates on the goal state, but local facts are
not part of that. The "cases" / "induct" family of proof methods make an
exception in providing named cases as small local proof contexts to be
activated later. This is a concession to the requirements of complex
induction schemes.
Secondly, how about a similar construct for introduction rules?
Applying an introduction lemma for C
assumes a: "!!x. A ==> B" shows C
could generate a structure comparable to a cases rule that does the "fix x assume a: A show B" for you, possibly extending to multiple assumptions.
Is there a mechanism for this? It would amount to multiple "case ..." with different conclusions, which I understand does not work currently.
Some decades ago, I was thinking about that but dismissed it.
The next time when I will revisit this question there will be some
Prover IDE support to copy-paste parts of the goal state into the source
document.
Makarius
Email Gateway (Aug 22 2022 at 19:11):From: Gidon Ernst <gidon.ernst@unimelb.edu.au>
Hi Makarius,
On 2/18/19 1:54 AM, Makarius wrote:> On 13/02/2019 10:12, Gidon Ernst wrote:
I really like obtains in lemmas with the ability to specify multiple
cases.Note that in a proof body you have a few more such structuring
principles for statements: "have C if A for x", "consider A | B | C",
and then "obtain x where A" as a special case.
Thanks for the pointer. I've seen obtain and used it occasionally, and
it permits one to name facts as in "obtain x where a: A".
Is there a similar mechanism for "obtains" in lemma definitions?
I've noted that you can in fact write "shows a: A", but I haven't
figured out where the "a" comes into play...
Having names for conclusions of lemmas that "shows a: A B" that get
imported into a proof state could be a cool feature for maintenance:
there is no need to spell out "A" or refer to it by position "a(1)" when
you use it -> proofs remain intact even if "A" changes or more
conclusions get added to a lemma.
Secondly, how about a similar construct for introduction rules?
Applying an introduction lemma for C
assumes a: "!!x. A ==> B" shows C
could generate a structure comparable to a cases rule that does the>> "fix x assume a: A show B" for you, possibly extending to multiple
assumptions.
Is there a mechanism for this? It would amount to multiple "case ..."
with different conclusions, which I understand does not work
currently.Some decades ago, I was thinking about that but dismissed it.
The next time when I will revisit this question there will be some
Prover IDE support to copy-paste parts of the goal state into the source
document.
That would be great! (Do you still remember why you dismissed that
Idea?). Same argument about naming would apply here, though.
That said, I've been using Isabelle for ~6 month now and I quite enjoy it.
Best,
Gidon
Email Gateway (Aug 22 2022 at 19:11):From: Makarius <makarius@sketis.net>
On 18.02.19 02:16, Gidon Ernst wrote:
Thanks for the pointer. I've seen obtain and used it occasionally, and
it permits one to name facts as in "obtain x where a: A".
Is there a similar mechanism for "obtains" in lemma definitions?
"lemma obtains" corresponds to "consider" within a proof body: it states
an elimination (possible) with case split. "obtain" is for a one-arm
case split where the rule is used on the spot to augment the local
context, and later dispose the assumptions again thanks to the proven rule.
I've noted that you can in fact write "shows a: A", but I haven't
figured out where the "a" comes into play...
"lemma shows" is merely a syntactic device of the long form of rule
statements "fixes-assumes-shows". The name attached there is the name of
the overall conclusion of the lemma.
Secondly, how about a similar construct for introduction rules?
Applying an introduction lemma for C
assumes a: "!!x. A ==> B" shows C
could generate a structure comparable to a cases rule that does the>> "fix x assume a: A show B" for you, possibly extending to multiple
assumptions.
Is there a mechanism for this? It would amount to multiple "case ..."
with different conclusions, which I understand does not work
currently.Some decades ago, I was thinking about that but dismissed it.
The next time when I will revisit this question there will be some
Prover IDE support to copy-paste parts of the goal state into the source
document.That would be great! (Do you still remember why you dismissed that
Idea?). Same argument about naming would apply here, though.
The generic problem is to find just the right amount of explicitness in
proofs that they become readable and maintainable. Being too implicit
can destroy this delicate balance (e.g. via automatic name bindings for
obscure goal artifacts); the same can happen by being too explicit (e.g.
big generated goal statements copied into the text, without symbolic
abbreviations for certain sub-terms).
Existing Isar (the current version from 2016) already spans a broad
range of possibilities: it is often just a matter of style how to use it
in applications. The language also tolerates "improper" elements like
"apply" or "supply" and semi-proper ones like "subgoal" and "goal_cases"
(see the index of the isar-ref manual).
In particular, the last two might help in your applications, but it is
hard to tell without looking at the applications concretely.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC