The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

eq is not special.  You can add an axiom, and it'd be nice to have axons with reduction rules, but it seems inelegant to add it to the kernel.  Do you have an idea for a general rule that would work for inductive type failures in general?

On Mon, May 9, 2016, 7:36 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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
>>>>>>
>>>>>>
>>