The Coq mailing list

[emilioga AT cis.upenn.edu (Emilio Jesús Gallego Arias)]

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.