The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

> Le 16 oct. 2019 à 15:47, Sylvain Boulmé 
> <Sylvain.Boulme AT univ-grenoble-alpes.fr>
>  a écrit :
> 
> Hello Jeremy,
> 
> 
> Le 16/10/2019 à 15:35, Jeremy Dawson a écrit :
> > Given the earlier replies to my question, this doesn't seem to make sense
> 
> When you "Require Import Coq.Program.Equality",
> you implicitly import the "eq_rect_eq" axiom, of:
> 
> https://coq.inria.fr/library/Coq.Logic.Eqdep.html
> 
> whereas earlier replies explain how to avoid this axiom in some cases.
> 
> To my knowledge, there is no particular issue with this axiom, except that 
> it may not be consistent with other axioms, such as univalence.

There is always the issue that axioms are stuck terms. Equations [1] provides 
dependent elimination
tactics that avoid relying on it. For example, if you can provide an instance 
of the type class
`UIP A := forall (x y : A) (p q : x = y), p = q` (or `EqDec A` from which 
`UIP A` can be derived) 
then the tactics will simplify equalities of sigma-types with `A` as a domain 
without relying 
on an axiom but rather on the proof. It will also tell you if you try to 
implicitly use the
K/UIP/eq_rect_eq axiom while performing a dependent elimination (switch `Set 
Equations With UIP` 
to allow its use based on provided type class instances).

The Equations Reloaded paper provides an in-depth explanation of the issue 
and how Equations 
treats it.

[1] http://mattam82.github.io/Coq-Equations/

Best,
— Matthieu