CODEWITHSUNDEEP
coqcoq-tactic
thor
thor

Reputation: 22460

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

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.

Upvotes: 3

Views: 320

Answers (2)

Kristopher Micinski
Kristopher Micinski

Reputation: 7672

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.

Upvotes: 2

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

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

Upvotes: 1

Related Questions