The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/09/2016 07:18 PM, Clément Pit--Claudel wrote:
> I'm not sure I understand correctly:
>
> 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: Set},

The slight change here from {T1 T2 : Prop} to {T1 T2 : Set} makes the 
difference.

>      T1 = T2 -> T1 -> T2.
> Proof.
>    destruct 1; apply id.
> Qed.
>
> Lemma true_neq_false: not (@eq Set 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.

Got it:

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: Set},
    T1 = T2 -> T1 -> T2.
Proof.
  destruct 1; apply id.
Qed.

Lemma true_neq_false: not (@eq Set True False).
  intro Heq.
  destruct (@out_of_thin_air True False Heq I).
Qed.

Lemma alltrue : forall (x y : True), x = y.
intros.
destruct x, y.
reflexivity.
Qed.

Lemma true_neq_bool: not (@eq Set True bool).
  intro Heq.
  assert (true <> false) by discriminate.
  assert (true = false).
  pose alltrue.
  rewrite Heq in e.
  apply e.
  contradict H.
  assumption.
Qed.

Lemma false_neq_bool : not (@eq Set False bool).
  intro Heq.
  symmetry in Heq.
  pose (out_of_thin_air Heq) as f.
  apply f.
  exact true.
Qed.

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

So, this means universe reduction for arbitrary relations is not a good 
idea.  But, maybe just for eq...?

-- Jonathan

> On 2016-05-09 18:45, Jonathan Leivent wrote:
> > 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