The Coq mailing list

[Benjamin Werner <werner AT pauillac.inria.fr>]

Just to add my two cents:

On the other hand, most of the time there should be no need for having
a computational Set type depend upon a non-computational proof of
A\/B.

Mybye you can say a few words about why you want this ?

Cheers,

Benjamin



> 
> No you are right, it is not possible to do an elimination on o:A\/B 
> in order to build a proof of (P o):Set.
> 
> The distinction between Prop and Set is that the computation 
> of objects in Set does not need information on object in sort Prop.
> In your rule you will have 
> 
> o:A\/B    f1:(x:A)(P (or_introl x)) f2:(y:B)(P (or_intror y))
> ------------------------------------------------------------------------
>   Case o of (or_introl x) => (f1 x) | (or_intror x) => (f2 y) end :(P o)
> 
> Because (P o):Set one needs to be able to compute 
>  Case o of (or_introl x) => (f1 x) | (or_intror x) => (f2 y) end
> but without knowing the proof of A\/B which has type Prop, it is not
>  possible to choose between f1 or f2
> 
> C. Paulin
> 
> Patricia Peratto writes:
>  > Than you very much.
>  > But I want to define dependent elimination over Sort
>  > Set. I couldn't. Is not allowed?
>  > 
>  > Patricia Peratto
>  > 
>  > ----- Original Message -----
>  > From: "Christine Paulin" 
>Â <Christine.Paulin AT lri.fr>
>  > To: "Patricia Peratto" 
>Â <pperatto AT hotmail.com>
>  > Cc: 
>Â <coq-club AT pauillac.inria.fr>
>  > Sent: Sunday, March 23, 2003 1:48 PM
>  > Subject: Re: [Coq-Club] dependent types
>  > 
>  > 
>  > >
>  > > You may use the following declaration
>  > > Coq < Scheme or_elim := Induction for or Sort Prop.
>  > > or_elim is recursively defined
>  > >
>  > > Coq < Check or_elim.
>  > > or_elim
>  > >      : (A,B:Prop; P:(A\/B ->Prop))
>  > >         ((a:A)(P (or_introl A B a))) ->
>  > >         ((b:B)(P (or_intror A B b))) ->(o:(A\/B))(P o)
>  > >
>  > > In order to use it, when p has type (A\/B)
>  > > there is the tactic
>  > > Elim p using or_elim.
>  > >
>  > > C. Paulin
>  > >
>  > > Patricia Peratto writes:
>  > >  > I'm trying to define a rule for or_elim with dependent types
>  > >  > as follows:
>  > >  >
>  > >  > (A,B:Prop; P:(A\/B->Set))
>  > >  >  ((a:A)(P (or_introl A B a)))
>  > >  >  ->((b:B)(P (or_intror A B b)))->(p:(A\/B))(P p)
>  > >  >
>  > >  > with cases, but does not recognize p as formed
>  > >  > by constructors and asks type (P p) for the conclusion.
>  > >  >
>  > >  > Is it not possible to define this rule in Coq?
>  > >  >
>  > >  > Regards
>  > >  >
>  > >  > Patricia Peratto
>  > >
>  > > --
>  > >   Christine Paulin-Mohring             mailto : 
>Â Christine.Paulin AT lri.fr
>  > >   LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY 
> Cedex
>  > >   LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
>  > >
>  > >
>  > >
>  > >
>  > >
>  > >
>  > >
>  > >
> 
> -- 
>   Christine Paulin-Mohring             mailto : 
>Â Christine.Paulin AT lri.fr
>   LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
>   LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
> 
> 
> 
> 
> 
> 
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>