Proof irrelevance in COQ

0
votes

I am thinking about proof irrelevance in COQ. One provable statement says:

If equality of a type is decidable then there can be only one proof for the equality statement, namely reflexivity.

I wonder if its possible to construct types with more than one equality proof in COQ. Therefore I ask if the following construct is consistent?

(*it is known that f=g is undecidable in COQ *)    
Definition f(n:nat) := n.
Definition g(n:nat) := n+0.

Axiom p1: f=g.
Axiom p2: f=g.

Axiom nonirrelevance:p1<>p2.

What me puzzles here is the fact that by introducing p1 I made the equality f=g decidable and therefore it should only have one proof! What is my error in reasoning here?

Is that all a pure COQ behaviour or is it similar in HOTT?

1
coq
Related, I think: cstheory.stackexchange.com/questions/5158/… – augurar
I think your error in reasoning is that p1 does not make equality over the type nat -> nat decidable, so proof irrelevance is not implied. – augurar

1 Answers

1
votes

I think you're confusing several things.

The provable statement you are speaking of can be found in https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html and is

Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) : 
    forall (y:A) (p1 p2:x = y), p1 = p2.

Now what is quite interesting is the type of eq_dec. First of all, it doesn't even really ask for equality to be decidable, it just asks for it to be true or false which is way less stronger than {x = y} + {x <> y}

Then notice that it doesn't ask this just for the x and y to prove the equality irrevelance of, it ask this property for all functions.

So you would need to prove your contradiction that forall (f g : nat -> nat), f = g \/ f <> g which you cannot. p1 is just a proof that f = g \/ f <> g for your specific f and g. Notice though that if you could, it would just mean that there is no way to build a system in which you can compare functions and yet have multiple ways which are provably different to check them.

Finally, for P to be undecidable only means that there is no constructible functions over {P} + {~P} yet, it doesn't mean that adding one as an axiom leads to a contradiction. Just adding that in case it wasn't clear.