Email Gateway (Aug 19 2022 at 11:33): Email Gateway (Aug 19 2022 at 11:33):From: Wilmer RICCIOTTI <Wilmer.Ricciotti@irit.fr>
Hi all,
as a beginner in the use of Isabelle/Isar, I have every day numerous clashes with the Isar way of proving theorems. The strangest one to date is related to proving an existentially quantified formula when you have the same formula with an explicit witness as a hypothesis. That is to say, something similar to this lemma:
lemma fie : "P a ⟶ (∃b.(P b))"
proof
assume ha : "P a"
thus "∃b.(P b)"..
qed
Unsurprisingly, this proof doesn't pose any challenge at all. However I can slightly complicate the formula by means of a definition, and this obvious proof technique won't work any more. Specifically, I define
definition bijection :: "('a ⇒ 'b) ⇒ bool" where
"bijection f = (∀y::'b.∃!x::'a. y = f x)"
and then the same proof as before, with bijection in place of a generic P, fails:
lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
proof
assume hg : "bijection (g::'a ⇒ 'b)"
thus "∃f.(bijection f)"..
qed
replacing the implicit ".." with an explicit "proof (rule exI)" fails similarly, leaving me quite puzzled.
(Un)Interestingly, since "foo" is an instance of "fie", we can easily prove it using "by (rule fie)" and nothing else. However this feels more like a trick to make things work than a solution.
What am I doing wrong?
Best,
Email Gateway (Aug 19 2022 at 11:33):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
the behaviour of "rule" in the presence of premises is something that I
have not and will probably never understand.
You can replace the ".." with a "by (rule_tac exI)" or a "by (intro
exI)" and that works fine. Personally, I usually prefer the good old "by
blast" in these cases. Another thing that would work is "from exI[OF
this] show "∃b.(P b)" ."
As for the reason that rule fails here but rule_tac works, that is
something from the depths of the internals of Isabelle that are far
outside my area of expertise.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:33):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Wilmer,
I often run into the same problem ;) which is that things are too
polymorphic.
lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
proof
assume hg : "bijection (g::'a ⇒ 'b)"
thus "∃f.(bijection f)"..
In this line, check the type of "f" (e.g., Ctrl+hover in jEdit) which
outputs:
bound "f"
bound variable
:: 'c ⇒ 'd
i.e., the types of "f" and "g" do not match. (Try to give f an explicit
type in the binder.)
hope this helps,
chris
Email Gateway (Aug 19 2022 at 11:33):From: Manuel Eberl <eberlm@in.tum.de>
Hallo Christian,
Are you quite sure about this? On my system, all occurences of "f" and
"g" are displayed as having type "'a ⇒ 'b". I don't see how it could be
any other way, seeing as bijection is a free variable and the assertion
forces "bijection" to have the type "('a ⇒ 'b) ⇒ bool", which in turn
forces the bound f in the "thus statement" to be of type "'a ⇒ 'b" as well.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:33):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Manuel,
as far as I see "bijjection" is not a free variable, it was defined by
Wilmer. But you are write that my suggestion does not solve to problem.
Rather he would have to combine our two mails ;)
cheers
chris
Email Gateway (Aug 19 2022 at 11:33):From: Manuel Eberl <eberlm@in.tum.de>
Oh my, I must have missed that. Yes, in these cases, it is best to
annotate variables in binders. If one does not know where the problem
comes from in these cases, it can also be a good idea to enable the
unification trace, which shows exactly why a role could not be applied;
in this case, probably a clash between the free type variables.
But be that as it may, even when one does annotate the bound variable,
".." still does not work, which then brings us back to what I said in my
first reply. :)
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:33):From: Christian Sternagel <c.sternagel@gmail.com>
Yes. That's what I wanted to say with "combine our two mails". -cheers chris
For the record: I also find this behavior of ".."/"rule"/... vs.
"rule_tac"/"blast"/... strange.
Email Gateway (Aug 19 2022 at 11:33):From: Stephan Merz <Stephan.Merz@loria.fr>
In order to answer Wilmer's original question explicitly: your second lemma can be proved using baby-steps as follows.
lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
proof
assume hg : "bijection (g::'a ⇒ 'b)"
thus "∃(f::'a ⇒ 'b).(bijection f)"
apply (intro exI)
apply assumption
done
qed
Observe that you also have to type-constrain the bound variable in "thus", and that (as noted by Christian and Manuel) ".." (or equivalently "apply (rule exI)"), which applies the rule in elim-resolution mode fail due to somewhat inscrutable issues of type resolution.
Of course, you'd typically apply automatic proof methods such as auto or blast that do the job.
Stephan
Email Gateway (Aug 19 2022 at 11:34):From: Manuel Eberl <eberlm@in.tum.de>
I looked through the relevant parts of the Isabelle source code just now
and all I could find was something called "Pattern.trace_unify_fail".
This option seems to be exposed in Proof General through the menu, but
in jEdit, nothing like that seems to exist. There doesn't seem to be a
configuration attribute either, so that one could do something like
"declare [[trace_unify]]".
However, as a workaround, you can do this in jEdit:
ML {* Pattern.trace_unify_fail := true *}
If you then try an "apply (rule exI)", you get the following error message:
The following types do not unify:
('a ⇒ 'b) ⇒ bool
('c ⇒ 'd) ⇒ bool
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:34):From: Makarius <makarius@sketis.net>
On Thu, 18 Jul 2013, Wilmer RICCIOTTI wrote:
as a beginner in the use of Isabelle/Isar, I have every day numerous
clashes with the Isar way of proving theorems. The strangest one to date
is related to proving an existentially quantified formula when you have
the same formula with an explicit witness as a hypothesis. That is to
say, something similar to this lemma:lemma fie : "P a ⟶ (∃b.(P b))"
proof
assume ha : "P a"
thus "∃b.(P b)"..
qed
First this basic example in canonical form:
lemma "P a ⟶ (∃b. P b)"
proof
assume "P a"
then show "∃b. P b" ..
qed
Notes:
* No need to invent funny names for things that are never refered by
name. The empty name is fine by default. (If you do need names for
intermediate facts, you can use , , , or 1, 2, 3, until you get
better ideas. There is no need for Ha, Hb, Hc seen in other provers.
* 'thus' is an an old-fahsioned abbreviation, for people who like typing
more than necessary (paradoxically). It is better to use explicit
"then show" to make clear to yourself and the reader of the proof that
something is happening here: forward chaining of facts towards a goal.
Thus the subsequent "rule" step will first consume the facts, reducing
the rule by applying it to a prefix of its premises, and then apply
the remaining rule to the goal.
* "." and ".." are full proofs in their own right, just like "by
method". So you should put a space there, and not imitate terminators
seen in other provers.
* Placing parentheses within the term language correctly requires a bit
of experience with the syntax. It is fine to put redundant
parentheses there as a start, but I've made it precise in the example
to avoid obscuring the situation for people who are versed in the
syntax.
Unsurprisingly, this proof doesn't pose any challenge at all. However I
can slightly complicate the formula by means of a definition, and this
obvious proof technique won't work any more. Specifically, I definedefinition bijection :: "('a ⇒ 'b) ⇒ bool" where
"bijection f = (∀y::'b.∃!x::'a. y = f x)"and then the same proof as before, with bijection in place of a generic P, fails:
lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
proof
assume hg : "bijection (g::'a ⇒ 'b)"
thus "∃f.(bijection f)"..
qed
Here you try to make an existential introduction of a thing of function
type. Due to the way Larry implemented HO unification some decades ago,
this does not work in the compositional manner required by Isar. So here
is my slightly awkward proof (again in somewhat standard form):
definition bijection :: "('a ⇒ 'b) ⇒ bool"
where "bijection f ⟷ (∀y. ∃!x. y = f x)"
lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
qed
Note that there are two snags:
* The inner "show" needs to be precise about the types, because there is
no syntactic connection to the surrounding context: bound variable "f"
and global constant "bijection" are not constrained in any way by what
the proof text contains so far, so they would get a surprisingly
general type due to Milner type-inference, if the constraint on f is
omitted.
As a rule of thumb, when something should unify but doesn't, types
are too general. Isabelle/jEdit makes it relatively easy these days
to inspect the situation via the usual hovering. (I still need to
work out a color scheme to hilight such situations directly in the
Prover IDE.)
* Actual HO unification imcompleteness, which is a relevatively rare
incident. It is a tiny imperfection of Isabelle/Pure for the use of
structured proof checking in Isabelle/Isar. I've tried to convince
Larry to address that in 1998 already, but it is unrealistic to touch
this delicate part of Isabelle again.
To keep this thread interesting, and about actual Isar, here is another
version of the example to be considered:
lemma
fixes g :: "'a ⇒ 'b"
assumes "bijection g"
obtains f :: "'a ⇒ 'b" where "bijection f"
using assms ..
Makarius
Email Gateway (Aug 19 2022 at 11:34):From: René Neumann <rene.neumann@in.tum.de>
Am 19.07.2013 18:48, schrieb Makarius:
* 'thus' is an an old-fahsioned abbreviation,
When did this become 'old-fashioned'?
for people who like typing more than necessary (paradoxically).
|'th<TAB><space>sh<TAB>'| = 7
|'thus'| = 4
Not counting the time it takes to wait before autocompletion mechanisms
can be used (ie small delay before each <TAB>)
Email Gateway (Aug 19 2022 at 11:34):From: Makarius <makarius@sketis.net>
On Fri, 19 Jul 2013, René Neumann wrote:
Am 19.07.2013 18:48, schrieb Makarius:
* 'thus' is an an old-fahsioned abbreviation,
When did this become 'old-fashioned'?
Many years ago. It goes back to an old draft of Isar, which was derived
from Mizar and the Mizar mode for HOL, before 'then' was introduced as a
standalone Isar primitive.
Did you ever wonder why there is no conflation of "then obtain"?
for people who like typing more than necessary (paradoxically).
|'th<TAB><space>sh<TAB>'| = 7
|'thus'| = 4Not counting the time it takes to wait before autocompletion mechanisms
can be used (ie small delay before each <TAB>)
The extra typing happens when you change your structured goal
specfications back and forth several times, e.g.
then have
from blah have
with blah have
The form with 'then' saves typing for experts and is more easy to
understand for readers of the text. Isar is very compositional by design,
more than Mizar in that respect.
Makarius
Email Gateway (Aug 19 2022 at 11:34):From: Tobias Nipkow <nipkow@in.tum.de>
Don't worry, it is alive and kicking.
Tobias
Email Gateway (Aug 19 2022 at 11:34):From: Brian Huffman <huffman.brian.c@gmail.com>
Hi Wilmer,
Makarius has precisely identified the problem: Unification has trouble
when proving the existence of something with a function type. I have
come across this exact problem several times before; below is the
workaround that I have used.
lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI)
qed
The "-" method serves to turn "bijection g" from a chained fact into
an ordinary assumption in the proof goal; this then affects how the
"rule" method does unification. (Writing "by - rule" will also work.)
Grep the Isabelle sources for "by - (rule exI)" to see all the places
I've had to use this trick: Some examples involve proving countability
of types, showing goals of the form "∃f::'a ⇒ nat. inj f". Other
examples occur in HOLCF when proving instances of class "bifinite",
which asserts the existence of a function with certain properties.
The same trick used to be necessary for proving things of the form
"∃A::'a set. P A", during the period when "'a set" was an abbreviation
for "'a => bool". This is no longer the case, but you can still find
one or two leftover examples of "by - (rule exI)" in
Multivariate_Analysis.
Email Gateway (Aug 19 2022 at 11:34):From: Makarius <makarius@sketis.net>
According to canonical jargon on this mailing list, "old fashioned" means
it is not even "legacy" yet. It just means old-fashioned.
Nonetheless, there is no reason to encumber new learners of Isar with old
habits drawn from Mizar. The latter cannot even use "then obtain ..." or
"obtain ... then". I also want to do Mizar justice in avoiding confusion
of its "hence" and "thus" that have a quite different meaning there.
Makarius
Email Gateway (Aug 19 2022 at 11:34):From: Makarius <makarius@sketis.net>
On Fri, 19 Jul 2013, Brian Huffman wrote:
lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
qedlemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI)
qedThe "-" method serves to turn "bijection g" from a chained fact into
an ordinary assumption in the proof goal; this then affects how the
"rule" method does unification. (Writing "by - rule" will also work.)
For practical purposes, the "by - rule" form is indeed better. My more
ugly variant above stays formally within structured rule application of
Isar, but its need of instantiation is not nice.
BTW, the 'by' command has these two slots: initial method and terminal
method. There is a difference in handling of chained facts, so
by method1 method2
is conceptionally (and operationally) different from
by (method1, method2) -- improper
Normally one should only show the good examples to imitate, but
"by (cases, auto)" is seen a bit too often in examples, where "by cases auto"
was meant by the writer of the text.
The same trick used to be necessary for proving things of the form
"∃A::'a set. P A", during the period when "'a set" was an abbreviation
for "'a => bool".
Gladly that episode is history. It was known beforehand that such issues
would follow from that experiment, because Larry or Tobias had introduced
the explicit 'a set type exactly to prevent HO unification problems,
although it was before recorded history.
Makarius
Last updated: Apr 19 2024 at 12:27 UTC