Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] dependent types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent types


chronological Thread 
  • From: Christine Paulin <Christine.Paulin AT lri.fr>
  • To: "Patricia Peratto" <pperatto AT hotmail.com>
  • Cc: <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] dependent types
  • Date: Sun, 23 Mar 2003 22:27:23 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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











Archive powered by MhonArc 2.6.16.

Top of Page