This is a classical but interesting question:

Is nat equal to bool? Show and prove your answer.

Hints

• You probably guessed 'no'. If so you are correct.

• a = b means that any property a satisfies, b will also satisfy (Leibniz equality). Find a predicate P : Set -> Prop that:

  • Does not explicitly check what the type is (Coq will not let you)
  • Uses the given type to construct a property that successfully differentiates nat and bool (For P nat and P bool, one is true and the other is false)

• For this type:

  Inductive mybool := mytrue | myfalse.
  

  You will not be able to prove that bool <> mybool.