CODEWITHSUNDEEP
coq
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Under what circumstances is equality of equalities decidable?

Consider the following goals:

Goal forall (x y: I = I), x = y.
Proof.
Abort.

Goal forall (x y: tt = tt), x = y.
Proof.
Abort.

Both I and tt are members of singleton types. The former lives in Prop, the latter in Set. These are very uncomplicated types, so I wouldn't expect them to support rich equality types in any setting. Are these goals provable in Coq without resorting to the Uniqueness of Identity Proofs axiom?

Upvotes: 1

Views: 72

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

A common sufficient condition is for the type to have decidable equality; see also this FAQ: https://github.com/coq/coq/wiki/The-Logic-of-Coq#i-have-two-proofs-of-an-equality-statement-can-i-prove-they-are-equal

Upvotes: 5

Related Questions