The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I know that if [A : Type] has decidable equality (that is, [∀ x y : A, x = y ∨ x ≠ y]) than [eq_proofs_unicity] (in the standard library) tells me that [∀ (x y : A) (p1 p2 : x = y), p1 = p2].  Does this extend to other relations?

In particular, say I have an inductive relation [Inductive R : A → A → Prop], for each pair of distinct constructors [c1], [c2], and some elements [x y : A], I have a proof that if there are some arguments which can be passed to [c1] to construct [R x y], and also some arguments which can be passed to [c2] to construct [R x y], then one can derive absurdity.  For example, [le] fits this model, because it has two constructors, but they can't both apply at the same time.

If this is the case, is there a decision procedure for generating a proof of [∀ (x y : A) (p1 p2 : R x y), p1 = p2]?

Thanks,

Jason