Questions and exercises regarding inductive propositions:
Question (Henning): can you define sensible equality
on propositions that lives in Set as opposed to Prop?
Niels: Use Sigma-types?
Inductive lessThanTwo : nat -> Prop :=
| zero : lessThanTwo 0
| one : lessThanTwo 1.
Question (Guillaume):
We know that we can prove the proposition
[lessThanTwo n <-> n = 0 \/ n = 1].
In that statement, everything live in Prop.
Which of the following you can prove?
- forall n, lessThanTwo n -> {n = 0} + {n = 1}
- forall n, {n = 0} + {n = 1} -> lessThanTwo n