The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Actually, it's more subtle than it may seem:

Check (prod:Prop->Prop->Prop).

Conjunction is actually a less polymorphic restriction of cartesian product. We can indeed define the following:

Definition and_rect' (A B : Prop) (P : A /\ B -> Type)
  (f : forall (a : A) (b : B), P (conj a b)) (p : A /\ B) :=
    let (x, x0) as p0 return (P p0) := p in
    f x x0
.

Check and_rect'.
(* and_rect'
     : forall (A B : Prop) (P : A /\ B -> Type),
       (forall (a : A) (b : B), P (conj a b)) -> forall p : A /\ B, P p *)

There is a convention of not using the dependent elimination of inductive types in Prop for their elimination principles, even when it would be available. But I don't know why this convention was established in the first place.


/Arnaud

On 24 July 2014 15:56, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi,

On 24/07/14 14:20, Michel Levy wrote:
> I examine the differences between the and_rect and prod_rect definition (with Print and_rect and Print prod_rect).
> In the and_rect definition, you have P:Type while in the prod_rect definition, you have P: prod A B -> Type.
> Why is the reason of this difference ?

Do you find the fact that "prod_rect" and "and_rect" have different types surprising?

Isn't that just a straightforward consequence of the fact that "prod" and "and" themselves have different types?
That is:

        and : Prop -> Prop -> Prop
        prod : Type -> Type -> Type