*To*: Wilmer RICCIOTTI <Wilmer.Ricciotti at irit.fr>*Subject*: Re: [isabelle] Unable to prove easy existential "directly"*From*: Makarius <makarius at sketis.net>*Date*: Fri, 19 Jul 2013 16:48:17 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <6c9a-51e80c80-1-5d76dd8@90856565>*References*: <6c9a-51e80c80-1-5d76dd8@90856565>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 18 Jul 2013, Wilmer RICCIOTTI wrote:

as a beginner in the use of Isabelle/Isar, I have every day numerousclashes with the Isar way of proving theorems. The strangest one to dateis related to proving an existentially quantified formula when you havethe same formula with an explicit witness as a hypothesis. That is tosay, 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 Ican slightly complicate the formula by means of a definition, and thisobvious 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

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.

lemma fixes g :: "'a ⇒ 'b" assumes "bijection g" obtains f :: "'a ⇒ 'b" where "bijection f" using assms .. Makarius

**Follow-Ups**:**Re: [isabelle] Unable to prove easy existential "directly"***From:*René Neumann

**Re: [isabelle] Unable to prove easy existential "directly"***From:*Brian Huffman

**References**:**[isabelle] Unable to prove easy existential "directly"***From:*Wilmer RICCIOTTI

- Previous by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Previous by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list