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.