Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Elimination Rules

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Elimination Rules


Chronological Thread 
  • From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
  • To: "<coq-club AT inria.fr>" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Elimination Rules
  • Date: Thu, 7 Aug 2014 05:25:31 +0000
  • Accept-language: en-GB, en-US
  • Authentication-results: spf=none (sender IP is ) smtp.mailfrom=jeffrey.terrell AT kcl.ac.uk;

In some texts, -> is treated in the same way as any other connective; and given that e.g. /\ has an elimination rule, i.e. and_rect, I was wondering whether -> has an elimination rule too. The same applies to forall x : A, P.

It's clear that there's something fundamental about type P -> Q, because attempting to define it in the normal way is problematic.

Inductive imply (P Q : Prop) : Prop :=
   imp : (P -> Q) -> imply P Q.

Regarding forall x : A, P, I'm aware that you can build a proof f a of P[a/x], but what is it that says you can?

Regards,
Jeff.

On 6 Aug 2014, at 22:09, Maxime Dénès wrote:

Well, given a proof a of A and a proof f of forall x : A, P, you can build the proof f a of P[a/x].

Not sure if this answer your question, though.

Are you familiar with the Curry-Howard isomorphism? If not, I would advise to read about it.

Best,

Maxime.

On 08/06/2014 04:59 PM, Terrell, Jeffrey wrote:
From a proof of A and a proof of A -> B, we can infer B. This is the -> elimination rule.

Similarly, from a proof a of A and a proof of forall x : A, P, we can infer P[a/x]. This is the forall elimination rule.

How are these elimination rules manifest in Coq?

Regards,
Jeff.





Archive powered by MHonArc 2.6.18.

Top of Page