Re: [isabelle] Eliminating two quantifiers in structural proof



Forgot this one:

theorem th11d:
   "∀x. ∀y. P x y ==> P a b"
     proof -
       assume  "∀x. ∀y. P x y"
       from this have "∀y. P a y" by (rule spec[where x =a])
       from this show  "P a b" by (rule spec[where x=b])
     qed

On Sun, Sep 16, 2012 at 8:04 AM, Alfio Martini <alfio.martini at acm.org>wrote:

> 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
>
>


-- 
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.