coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Injection on arguments of type Prop., Emilio Jesús Gallego Arias, 03/25/2014
- Re: [Coq-Club] Injection on arguments of type Prop., Ryan Wisnesky, 03/27/2014
- Re: [Coq-Club] Injection on arguments of type Prop., Eddy Westbrook, 03/27/2014
- Re: [Coq-Club] Injection on arguments of type Prop., Arthur Azevedo de Amorim, 03/27/2014
- Re: [Coq-Club] Injection on arguments of type Prop., Eddy Westbrook, 03/27/2014
- Re: [Coq-Club] Injection on arguments of type Prop., Ryan Wisnesky, 03/27/2014
Archive powered by MHonArc 2.6.18.