Re: [isabelle] Eliminating two quantifiers in structural proof



Try to use the meta-quantifier !! instead of \<forall> whenever you can, and in
your examples you can. Now if you have an assumption A: "!!x y. P x y" you can
instantiate the quantifiers very easily: just write A[of "t1" "t2"]. Then it is
hardly more verbose than Coq. Note that the instantiation order is not the order
of quantification but the order in which x and y occur in P (from left to
right). In fact, if you inspect A in the proof (eg via command thm) you see that
the !! have disappeared and x/y became ?x/?y.

Unfortunately the "of" operator only works for !!, and !! can only occur at the
"outermost" level, ie not inside HOL formulas. But in many situations that suffices.

Tobias

Am 15/09/2012 22:15, schrieb Edward Schwartz:
> 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.