The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

If you think of T_rect as the elimination rule of type T, as I've been doing, then every elimination rule depends on the -> and forall types. However, the dependence of e.g. False_rect on types -> and forall comes about as a result of discharging the asssumptions in the premisses of (False E), using the (-> I) and (forall I) rules, i.e. 

       [P : Type] [f : False]

---------------------------------------- (False E)

                 P

---------------------------------------- (-> I)

             False -> P

---------------------------------------- (forall I)

False_rect : forall P : Type, False -> P

The situation with (bool E), as with most others types, is different in that its premisses depend on other types, e.g. ->.

[P : bool -> Type] [f : P true] [f0 : P false] [b : bool]

--------------------------------------------------------- (bool E)

                            P b

As far as I'm aware, this state of affairs just reflects the fact that since a type system is constructed inductively, certain types (notably -> and forall) must be defined quite early on.

I'm actually very interested in understanding what's involved in building up a simple type system (with universes) from scratch. If anyone's got any information on how to do this, I'd be glad to receive it. Thanks.

Regards,

Jeff.

On 7 Aug 2014, at 10:16, Arnaud Spiwack wrote:

Well, technically [and_rect] and all other the [*_rect]-s are defined (using pattern-matching). You may want to [Print and_rect] to see what it looks like. You can, of course, define modus ponens like this:

Definition modus_ponens {P Q:Prop} (L:P->Q) (h:P) : Q := L h.

And, more generally, for forall (in Coq, [P->Q] is just a notation for [forall _:P,Q]):

Definition forall_rect {A:Type} {Q:A->Prop} (L:forall y, Q y) (x:A) : Q x := L x.

The fundamental rules of Coq (it's an arbitrary choice if you will, but it's technically motivated) are: "forall" is a type, inductive types are types, values of type "forall" are contructed with "fun" and eliminated with application, values of inductive types are constructed with constructors and eliminated with "match".

On 7 August 2014 07:25, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:

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.