The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I'm trying to generalize some of the standard library constructs to permit the use of [Type] rather than [Prop] (in particular, the structures that are behind the scenes of [reflexivity], [transitivity], [symmetry], [Add Parametric Relation], [Add Parametric Morphism], and [rewrite]/[setoid_rewrite]).  Because universe polymorphism is hard, there are some bits that I want to leave in [Prop], which I don't plan on using.  (I also don't want to lose any existing functionality.)  In order to do this, I would like to condition some definitions on whether the inputs are in [Prop] or in [Type].  I have achieved this with [relation] (below), which acts as both [fun A : Type => A -> A -> Type], and [fun A : Prop => A -> A -> Prop].  I would like to do a similar thing with [inverse] (also below), but am having trouble figuring out how to do this.  Can anyone help me make this work?  Thanks.

Local Notation typeOf A := ((fun T (_ : T) => T) _ A).

Notation relation A := (A -> A -> typeOf A%type).

Local Notation relationTypeOf R := ((fun A (_ : relation A) => A) _ R).

Notation inverse R := (flip (R%type : relation (relationTypeOf R)) : relation (relationTypeOf R)).

Set Printing All.

Eval compute in forall (A : Prop) (R : relation A), inverse R = inverse R.

(*

     = forall (A : Prop) (R : A -> A -> Prop),

       @eq (A -> A -> Type) (fun x y : A => R y x) (fun x y : A => R y x)

     : Prop

*)

(* I want

     = forall (A : Prop) (R : A -> A -> Prop),

       @eq (A -> A -> Prop) (fun x y : A => R y x) (fun x y : A => R y x)

     : Prop

*)

Alternatively to the last line, I want

  Eval compute in fun (A : Prop) (R : relation A) => inverse R : A -> A -> Prop.

to type-check.

In the standard library, [inverse] is defined as

  Notation inverse R := (flip (R : relation _) : relation _).

However, keeping this definition results in Coq failing to infer types in the following (which is a loss of functionality as compared with the standard library)

  Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.

  Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).

(I am somewhat confused about why this fails to type-check, so explanation of this would also be appreciated.)

-Jason