The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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},
    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.


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

Attachment: signature.asc
Description: OpenPGP digital signature