How to prove (n = n) = (m = m) in Coq?

Question

I am confused about the evidence and Prop etc. in Coq. How do we prove that (n = n) = (m = m)?

My intention is to show this is somehow True=True. But this is even correct formulation?

What I tried so far is:

Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.

But simpl. does nothing, and reflexivity neither. This is just an example, in general, I need to prove this for any type X if possible.

Have you considered to prove: (n = n) <-> (m = m)? Since <-> can be seen as equality between propositions, in Coq. — Rodrigo Ribeiro
@RodrigoRibeiro Thanks for the pointer. I'll try that. The example I showed is extracted from a larger proof. But I may have posed the assertion wrong. — tinlyx
Interesting question! I think this should fail because it need not be that n = m and so refl n <> refl m. I've spent the last hour trying to prove that (a=a)=(b=b) fails if a<>b but am still stuck. I've tried some interesting approaches and might post an "answer" later on detailing why the stuff I tried must fail. (But right now I just have a headache…) — nobody

Kristopher Micinski Kristopher Micinski · Accepted Answer · 2015-12-09T03:15:50

n = n and m = m are both propsitions, so they're of sort Prop rather than sort Set. This basically means that n = n is like a statement (that has to be proved) rather than something like true : boolean.

Instead, you could try proving something like: n-n = m-m, or, you could define a function nat_equal : nat -> bool that, given a natural, mapped it to bool, and then prove nat_equal n = nat_equal m.

If you really want to assert that the statements are equal, you'll need propositional extensionality.

How to prove (n = n) = (m = m) in Coq?

2 Answers