The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 11/08/2012 08:19 PM, Dmitry Grebeniuk wrote:
>    But there are no explanations about why the functional
> extensionality is not used by default (for "auto" tactic,
> for example; moveover, requires explicit Require Import).
> So, are there any cases when this axiom is undesirable?
> Can it break something?  I'd be glad to know about it (either
> in coq-club or from CPDT).
There are many reasons why such axioms are not used by tactics by default:

* Some axioms are inconsistent with each other. In particular, some are 
known to be inconsistent with -impredicative-set.

* Axioms (even those in Prop) may break computation. For example, 
uniqueness of identity proofs can be used to emulate complex dependent 
pattern matches. Unfortunately, such emulated pattern matches do not 
compute. They get stuck at something like

  match UIP x y p1 p2 with
  | eq_refl => ...
  end

  Since UIP is an axiom, it will not reduce to eq_refl, and thus this 
pattern match can never be contracted.

* It is unsure whether axioms remain consistent in future versions of 
Coq (e.g. Coq based on univalent foundations?).

* Last, but not least, many people prefer to keep their development 
clean of axioms for philosophical reasons, or just for elegance.

Besides, if you want functional extensionality or proof irrelevant 
without axioms, consider using a setoid equality instead of the standard 
Leibniz equality.

Best,

Robbert