3

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.

thor
  • 21,418
  • 31
  • 87
  • 173
  • Have you considered to prove: `(n = n) <-> (m = m)`? Since `<->` can be seen as equality between propositions, in Coq. – Rodrigo Ribeiro Dec 08 '15 at 16:11
  • @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. – thor Dec 08 '15 at 16:15
  • 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 Dec 08 '15 at 18:12

2 Answers2

2

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.

Kristopher Micinski
  • 7,572
  • 3
  • 29
  • 34
1

It is not possible to prove what you are asking for without assuming additional axioms; cf. this answer.

Community
  • 1
  • 1
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39