Re: [isabelle] Eliminating two quantifiers in structural proof
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Eliminating two quantifiers in structural proof
- From: Edward Schwartz <edmcman at cmu.edu>
- Date: Sat, 15 Sep 2012 17:51:10 -0400
- In-reply-to: <17766_1347740206_q8FKGjuS027503_CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>
- References: <17766_1347740206_q8FKGjuS027503_CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>
- Sender: edmcman at gmail.com
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"
assume A: "\<forall>x. P x"
from A show "P c" ..
And here is the two variable example:
lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
assume H: "\<forall>x y. P x y"
fix a b
from H have "\<forall>y. P a y" ..
thus "P a b" ..
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?
On Sat, Sep 15, 2012 at 4:15 PM, Edward Schwartz <edmcman at cmu.edu> wrote:
> 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
> 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
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and