The Coq mailing list

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

Actually, I overlooked a much simpler proof:

Definition True_not_False : True <> False :=
  fun H => let 'eq_refl := H in I.

which you essentially get from

Goal True <> False.
  destruct 1; exact I.
Qed.

Clément.

On 2016-05-09 18:22, 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