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 propertya
satisfies,b
will also satisfy (Leibniz equality). Find a predicateP : 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
andbool
(ForP nat
andP 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:
Stats:
Created | Jan 2, 2020 |
Published | Jan 2, 2020 |
Warriors Trained | 320 |
Total Skips | 22 |
Total Code Submissions | 160 |
Total Times Completed | 97 |
Coq Completions | 68 |
Agda Completions | 18 |
Lean Completions | 17 |
Total Stars | 6 |
% of votes with a positive feedback rating | 100% of 16 |
Total "Very Satisfied" Votes | 16 |
Total "Somewhat Satisfied" Votes | 0 |
Total "Not Satisfied" Votes | 0 |
Total Rank Assessments | 3 |
Average Assessed Rank | 6 kyu |
Highest Assessed Rank | 6 kyu |
Lowest Assessed Rank | 6 kyu |