The Coq mailing list

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