The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

Thank you for the informative answers.

I am thinking about this because I am reading http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-159876 that has been mentioned here in the quotient discussion.  He defines subset inclusion on PERs of the same type, then extends it trivially to a relation between PERs of different types, which I formalized like R and R' below as I was reading along.  He then proves that it's a partial order using an argument that starts with "the only interesting case is when the arguments are the same type".  But at this point I'm thinking this metatheory argument may not be formalizable in Coq without axioms.

Proving it for an arbitrary partial order compatible with an arbitrary equivalence relation seems not possible without axioms, since a necessary step of proving antisymmetry can be shown equivalent to JMEq_eq using a variation of Alexandre's argument.  (Attached .v file).

And if there's a special property of PERs that makes it work, it's not obvious to me at this point.  (Not that it should be, since I'm unfamiliar with PERs and how they are used in type theory, but an alternative to Setoid seems interesting.)

Attachment: MixParamPartialOrderJMeq.v
Description: Binary data

On Nov 18, 2011, at 9:07 AM, AUGER Cedric wrote:

You can also assume unicity of proof irrelevance:

Set Implicit Arguments.

Variable M: Type -> Type.
Variable R : forall A, M A -> M A -> Prop.

Inductive R' : forall A B, M A -> M B -> Prop :=
| CR' : forall A (x y : M A), R x y -> R' x y.

Definition cast A B (H:A=B) (a:A): B :=
match H in _=A' return A' with eq_refl => a end.

Axiom UIP : forall A (a:A) (K:a=a), K = (eq_refl a).

Theorem R'inv : forall A (x y : M A), R' x y -> R x y.
Proof.
 intros A.
 assert (forall B (H: M B = M A) (x : M A) (y : M B),
          R' x y -> R x (cast H y)).
  intros.
  destruct H0.
  rewrite (UIP H).
  simpl.
  assumption.
 intros x y K; exact (H _ (eq_refl _) x y K).
Qed.

But I guess that this is not as good as Alexandre answer,
since I don't think that JMeq_eq implies UIP.

Le Thu, 17 Nov 2011 23:31:40 +0100,
Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> a écrit :

On Thu, Nov 17, 2011 at 11:07 PM, Gregory Bush <gbush AT mysck.com>

wrote:

(* This may be trivial, but is the following provable in Coq

without using JMeq_eq or other axioms? *)

I think it is equivalent to JMeq_eq, so you will need some axioms to

prove it:

Set Implicit Arguments.

Section blah.

Variable M : Type -> Type.

Variable R : forall A, M A -> M A -> Prop.

Inductive R' : forall A B, M A -> M B -> Prop :=

| CR' : forall A (x y : M A), R x y -> R' x y.

Theorem R'inv : forall A (x y : M A), R' x y -> R x y.

Admitted.

End blah.

Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=

   JMeq_refl : JMeq x x.

Lemma JMeq_R': forall A (a:A) B (b:B), JMeq a b -> R' (fun T:Type =>

T) (@eq) A B a b.

Proof.

 intros. inversion H. constructor. reflexivity.

Qed.

Theorem JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.

Proof.

 intros. apply R'inv. apply JMeq_R'. assumption.

Qed.