Re: [isabelle] Unable to prove easy existential "directly"
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))"
assume ha : "P a"
thus "∃b.(P b)"..
First this basic example in canonical form:
lemma "P a ⟶ (∃b. P b)"
assume "P a"
then show "∃b. P b" ..
* 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
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)))"
assume hg : "bijection (g::'a ⇒ 'b)"
thus "∃f.(bijection f)"..
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)"
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
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
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
* 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:
fixes g :: "'a ⇒ 'b"
assumes "bijection g"
obtains f :: "'a ⇒ 'b" where "bijection f"
using assms ..
This archive was generated by a fusion of
Pipermail (Mailman edition) and