The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

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