The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

I believe there is a small misunderstanding here: in Emilio's example,
the inductive type he defined is *not* in Prop, but in Type. It is the
constructor's *argument* has sort Prop, and, as he pointed out, his
example is provable with other tactics besides "injection". I'm not
sure this is the intended behavior, but it would be very strange if it
were!

2014-03-27 16:51 GMT+01:00 Eddy Westbrook 
<westbrook AT kestrel.edu>:
> Yeah, constructors in Prop are not, in general, injective.
>
> One way to explain this is Proof Irrelevance: if all constructors in Prop 
> were injective, then we would be able to disprove Proof Irrelevance, 
> because applying the same constructor in Prop to two unequal objects would 
> have to yield two unequal proofs.
>
> -Eddy
>
> On Mar 26, 2014, at 9:56 PM, Ryan Wisnesky 
> <ryan AT cs.harvard.edu>
>  wrote:
>
>> I can’t answer most of your questions, but constructors of impredicative 
>> types aren’t always injective.  See question 41 of the Coq FAQ: 
>> http://coq.inria.fr/faq
>>
>> On Mar 25, 2014, at 9:43 AM, Emilio Jesús Gallego Arias 
>> <emilioga AT cis.upenn.edu>
>>  wrote:
>>
>>> Dear coq-club,
>>>
>>> What is the reason why the injection tactic ignores arguments of type
>>> Prop?
>>>
>>> Aren't constructors always injective?
>>> Would it make sense allowing it again?
>>>
>>> For instance, this restriction makes the inversion tactic less useful if
>>> your definitions contain objects in Prop.
>>>
>>> Injection over Prop arguments can be enabled by adding back InProp at
>>> tactics/equality.ml:566, following the comment there.
>>>
>>> [Unfortunately the change is not fully backwards-compatible. Coq build
>>> broke at QCanon.v, but a one liner fix allowed it to finish?]
>>>
>>> Thanks!
>>> Emilio
>>>
>>> (* Example of injection failing on prop arguments *)
>>>
>>> Variable p : Prop.
>>>
>>> Inductive K : Type := K1 : p -> K.
>>>
>>> Lemma K1_inj (n n' : p) (H : K1 n = K1 n') : n = n'.
>>> injection H.
>>>
>>> (* fails with:
>>>
>>>    "Error: Nothing to do, it is an equality between convertible terms."
>>>
>>>    [The error msg seems bogus BTW]
>>>
>>>    It is easily provable:
>>>  *)
>>> congruence.
>>>
>>> (* f_equals also works *)
>>> Qed.
>>
>



-- 
Arthur Azevedo de Amorim