Re: [isabelle] Eliminating two quantifiers in structural proof



Hi Edward,

I am not sure if this is what you what, but in Isar is fairly natural to do
such proofs. I use it to teach natural deduction to students.
Here goes three proofs of this conjecture:

theorem th11a:
   assumes prem: "∀x. ∀y. P x y"
   shows "P a b"
     proof -
       from prem have "∀y. P a y" by (rule spec)
       thus "P a b" by (rule spec)
     qed

theorem th11b:
   assumes prem: "∀x. ∀y. P x y"
   shows "P a b"
     proof -
       from prem have "∀y. P a y" by (rule allE)
       thus "P a b" by (rule allE)
     qed

theorem th11c:
   assumes prem: "∀x. ∀y. P x y"
   shows "P a b"
     proof -
       from prem have "∀y. P a y" by (rule spec[where x =a])
       from this show  "P a b" by (rule spec[where x=b])
     qed

I assume you hardly have to use the qualifieres (e(limination),
d(estruction)) when
working in Isar. I use this style only when I am playing with linear
scripts.

All the Best!

On Sat, Sep 15, 2012 at 5: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
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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