The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/09/2016 03:15 AM, Alan Schmitt wrote:
> ...
> I’m wondering about the converse: are there types for which equality is not
> decidable, but that have canonical equality proofs hence UIP?

Alan,

I have a class of types that have UIP but not eqdec ({a=b}+{a<>b}).  
They have instead excluded middle of equality (a=b \/ a<>b), which I 
call eqem.  I had also played with the proofs in Eqdep_dec, and found 
that the requirement on eqdec there could be relaxed to eqem.

For most uses in Coq, eqem is probably not very useful.  However, I am 
often working in a development that has proof relevance - a single Prop 
that has an injection axiom on it.  The reasons have to do with getting 
better erasability on extractions than I can otherwise get in Coq.  
Having this one Prop with injection allows me to get discrimination on 
all other inductive Props, which allows me to then get eqem on many of 
them, and hence UIP.  Unfortunately, having a proof relevance axiom 
means I can't use any axioms for proof irrelevance, so I need to prove 
useful varieties, such as UIP or "irrelevant sibling" (for given prop P, 
prove the existence of Q <-> P where Q is irrelevant - which I can do if 
P has eqem).

I have been trying to find various ways to automate proofs of eqdec, 
eqem, and UIP.   I will look closely at your proof to see if I can use 
it, so thanks for posting it!   Also, I didn't yet get a change to 
examine Dominique Larchey-Wendling's proof of UIP of sigma, but thanks 
to Dominique for that as well!

Most recently, I have found a very promising way to automate proofs of 
eqdec or eqem for dependent types - potentially more stable and 
certainly easier to automate than what I was working on previously at 
https://github.com/jonleivent/deptacs.  It involves proving eqdec (or 
eqem) on a sigma equality over the dependent type first.

I have wondered if it may be the case in Coq - without any axioms - that 
every purely inductive non-Prop type has eqdec and hence UIP. By purely 
and non-Prop, I mean not having Prop or functional typed fields, 
parameters, or indices.  Then, in the case of my proof relevance axiom, 
this extends to eqem in any purely inductive type, even Props and with 
Prop components - hence can potentially get UIP for all of them.

-- Jonathan