# 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))"
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 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
```
```
```
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```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.