The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Oops...

Inductive foo (A : Type) (x : A) : A -> Type :=
Build_foo (y z : A) : x <> y -> x <> z -> y <> z -> foo A x x.

Lemma out_of_thin_air : forall {T1 T2: Prop},
    T1 = T2 -> T1 -> T2.
Proof.
  destruct 1; apply id.
Qed.

Lemma true_neq_false: True <> False.
  intro Heq.
  destruct (@out_of_thin_air True False Heq I).
Qed.

Goal foo Set True True.
eapply (Build_foo Set _ False bool).
apply true_neq_false.

the apply fails with Error: Unable to unify "not (@eq Prop True False)" 
with "not (@eq Set True False)".

I guess I misunderstood Jason as saying that [foo Set True True] is 
already inhabited, but maybe he was instead saying that it would be 
inhabited if this kind of eq level reduction occurred?

-- Jonathan

On 05/09/2016 06:22 PM, Clément Pit--Claudel wrote:
> Does this work?
>
> Lemma out_of_thin_air : forall {T1 T2: Prop},
>      T1 = T2 -> T1 -> T2.
> Proof.
>    destruct 1; apply id.
> Qed.
>
> Goal True <> False.
>    intro Heq.
>    destruct (@out_of_thin_air True False Heq I).
> Qed.
>
>
> On 2016-05-09 18:03, Jonathan Leivent wrote:
> > Are you sure that thing is inhabited as you say?  I can't prove it - I end up with subgoals 
> > like "True <> False", which I don't think can be proven.
> >
> > Even if it were, can't such a collapsing reduction be only about equalities, 
> > in much the same way that axiom K is only about equalities?
> >
> > -- Jonathan
> >
> >
> > On 05/09/2016 05:12 PM, Jason Gross wrote:
> > > You're playing with fire here.  Consider the inductive type
> > > Inductive foo (A : Type) (x : A) : A -> Type := Build_foo (y z : A) : x <>
> > > y -> x <> z -> y <> z -> foo A x x.
> > >
> > > Then [foo Set True True] is inhabited (let y be False and z be bool), but
> > > [foo Prop True True] contradicts prop_extensionality+LEM and so cannot be
> > > inhabited.
> > >
> > > What rule for universes of inductive types can you formulate that permits
> > > what you want for equality but forbids collapsing [foo Set True True] is to
> > > [foo Prop True True]?
> > >
> > > On Mon, May 9, 2016, 4:01 PM Jonathan Leivent 
> > > <jonikelee AT gmail.com>
> > >  wrote:
> > >
> > > > On 05/09/2016 03:48 PM, Stefan Monnier wrote:
> > > > > > Note that [@eq Type@{i} A B -> @eq Type@{j} A B] does not hold for [i
> > > > > j],
> > > > > Hmm.. which part of Coq's typing rules cause this?
> > > > >
> > > > >
> > > > >            Stefan
> > > > I'd just like to make it go away.  Specifically, I'd like [@eq Type@{i}
> > > > A B] to reduce to [@eq Type@{j} A B] where j is the minimum permissible
> > > > level considering A and B.
> > > >
> > > > I guess one could have a type theory where some things are provably
> > > > equal at higher levels but not at lower ones.  But, such a thing seems
> > > > quite bizarre.
> > > >
> > > > -- Jonathan