Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Injection on arguments of type Prop.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Injection on arguments of type Prop.


Chronological Thread 
  • From: Ryan Wisnesky <ryan AT cs.harvard.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Injection on arguments of type Prop.
  • Date: Thu, 27 Mar 2014 00:56:11 -0400

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.




Archive powered by MHonArc 2.6.18.

Top of Page