6 kyu

Is nat equal to bool?

68 of 97dramforever

Description:

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.

Theorem Proving
Logic
Fundamentals

Similar Kata:

More By Author:

Check out these other kata created by dramforever

Stats:

CreatedJan 2, 2020
PublishedJan 2, 2020
Warriors Trained320
Total Skips22
Total Code Submissions160
Total Times Completed97
Coq Completions68
Agda Completions18
Lean Completions17
Total Stars6
% of votes with a positive feedback rating100% of 16
Total "Very Satisfied" Votes16
Total "Somewhat Satisfied" Votes0
Total "Not Satisfied" Votes0
Total Rank Assessments3
Average Assessed Rank
6 kyu
Highest Assessed Rank
6 kyu
Lowest Assessed Rank
6 kyu
Ad
Contributors
  • dramforever Avatar
  • donaldsebleung Avatar
  • monadius Avatar
  • eric-wieser Avatar
Ad