The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This proof will still go through when the inconsistency with prop_ext is fixed.  The inconsistency with prop_ext relies on using it to bypass the guard condition for fixpoints to create an infinite loop.  This proof does not use recursion, and so the fix to the guard condition will not affect this proof.

-Jason

On Tue, Jan 28, 2014 at 5:17 PM, Cody Roux <cody.roux AT andrew.cmu.edu> wrote:

Of course, prop_ext in inconsistent with the current version of Coq, so this proof shouldn't come as a surprise... :)

On 01/28/2014 04:51 PM, Jason Gross wrote:

You don't even need bracket types if you have prop_ext:

Axiom prop_ext: forall (p q : Prop), (p <-> q) -> p = q.

Goal forall (a b : Prop), @eq Type a b -> @eq Prop a b.

Proof.

  intros a b H.

  apply prop_ext.

  split; destruct H; apply id.

Defined.

On Tue, Jan 28, 2014 at 4:45 PM, Jeremy Avigad <avigad AT cmu.edu> wrote:

It should be possible to do using the "bracket type" projection Type -> Prop  but I am not sure how exactly it works in Coq since I do not use Prop.

V.

Good point. Here is how to do it using propositional extensionality.

(Sorry for the lousy proof scripts. I have been away from Coq for a while.)

Best wishes,

Jeremy

**********************

Axiom prop_ext: forall (p q : Prop), (p <-> q) -> p = q.

Section Test.

Variables a b : Prop.
Variable p : @eq Type a b.

Definition bracket (A : Type) : Prop := forall (P : Prop), (A -> P) -> P.

Lemma bracket_eq (x : Prop): bracket x = x.
  apply prop_ext.
  split.
  intro H.
    apply (H x).
    intro H1. apply H1.
  intros H P H1.
  apply (H1 H).
Qed.
 
Lemma coerce: @eq Prop a b.
  transitivity (bracket a).
    symmetry. apply bracket_eq.
  transitivity (bracket b).
    rewrite p. reflexivity.
  apply bracket_eq.
Qed.

End Test.

On 01/28/2014 03:50 PM, Vladimir Voevodsky wrote:

It should be possible to do using the "bracket type" projection Type -> Prop  but I am not sure how exactly it works in Coq since I do not use Prop.

V.

On Jan 28, 2014, at 2:30 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

There is no way without axioms.  Going the other way is straightforwad: "match (H : @eq Prop x y) in (_ = y') return (@eq Type x y') with eq_refl => eq_refl end".  It does not work going the other way because y' would be a Type, and you'd be trying to make it a Prop.  If you think about this homotopy-theoretically (google homotopy type theory), there is no guarantee that every point along a path @eq Type_i (x : Type_j) (y : Type_j) will be small enough to fit into a Type_j.  You could do it with Axiom K, I believe.

-Jason

On Jan 28, 2014 1:06 PM, "Leonardo de Moura" <leonardo AT microsoft.com> wrote:

Hi,

 

Given (x y : Prop), I’m wondering about how to coerce an equality proof for (@eq Type x y) to (@eq Prop x y).

Is this possible?

 

Thanks,

Leo