Re: [isabelle] Eliminating two quantifiers in structural proof



Hi all,

I made a few breakthroughs in understand Isar:

1. "proof" is not the same thing as "proof -".  In particular, proof
looks for a classical logic introduction rule that matches the current
goal.  It will not work with goals like "A ==> B" as I had.  "proof -"
works on these.  This is really confusing, and if any Isabelle devs
read this, please consider changing it!

2. Here are the modified proofs of my examples:

The first example can be rewritten where the assumption is more general:

lemma single_proof : "(\<forall>x. P x) \<Longrightarrow> P a"
proof -
  assume A: "\<forall>x. P x"
  fix c
  from A show "P c" ..
qed

And here is the two variable example:

lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
proof -
  assume H: "\<forall>x y. P x y"
  fix a b
  from H have "\<forall>y. P a y" ..
  thus "P a b" ..
qed

This is a big improvement over my previous attempts, but still seems
overly verbose for just instantiating bound variables.  Is there a
quicker way that works on multiple bound variables at the same time?

Thanks again,

Ed

On Sat, Sep 15, 2012 at 4:15 PM, Edward Schwartz <edmcman at cmu.edu> wrote:
> Hi,
>
> I am new to Isabelle, and am stuck on a fairly trivial part of my
> proof.  I have an assumption "\forall x y. P x y".  I'd simply like to
> show (P a b) for two terms I have (a and b).  Surprisingly, I am
> having trouble doing this in a structural way.
>
> With one quantified variable, there is no problem:
>
> lemma single_proof : "(\<forall>x. P x) \<Longrightarrow> P a"
> proof (erule allE)
>   fix c
>   assume A: "P c"
>   from A show "P c" by assumption
> qed
>
> My understanding of what is happening is that allE removes the
> quantifier, and so we really just prove /\ c. P c ==> P c.  It seems
> like a better proof would be of /\ c. P ?c ==> P c.  Is there any way
> to do this instead?
>
> lemma double : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
> apply (erule allE, erule allE)
> apply assumption
> done
>
> Here is a way to do the proof with tactics.  Unfortunately, in my
> larger proof, the erule commands do not find the correct assumption,
> and so I must specify P manually, which is *very* ugly.
>
> lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
> proof (erule allE)
>   fix c
>   assume "\<forall>y. P c y"
>   have "P c b"
>   proof (erule allE) (* error: proof command failed *)
>
> Finally, I try to do a structural proof, eliminating one quantifier at
> a time, and fail.  I've tried many variations, but can't seem to
> understand how to do this.  If someone could show how to finish this
> proof, and explain why it works, I would greatly appreciate it.
>
> Overall, Isabelle/HOL seems to make it very difficult to instantiate
> free variables in foralls.  In Coq, this is very easy, since \forall
> x. P x is actually a function that accepts a variable v and returns
> proof that (P v).  What am I missing?
>
> Thanks,
>
> Ed
>





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