1. Write a function of type ∀ n m : nat, {n ≤ m} + {n > m}. That is, this function
decides whether one natural is less than another, and its dependent type guarantees
that its results are accurate.
2.(a) Define var, a type of propositional variables, as a synonym for nat.
(b) Define an inductive type prop of propositional logic formulas, consisting of
variables, negation, and binary conjunction and disjunction.
(c) Define a function propDenote from variable truth assignments and props to Prop,
based on the usual meanings of the connectives. Represent truth assignments as
functions from var to bool.
(d) Define a function bool true dec that checks whether a boolean is true, with a
maximally expressive dependent type. That is, the function should have type
∀ b, {b = true} + {b = true → False}.
(e) Define a function decide that determines whether a particular prop is true under
a particular truth assignment. That is, the function should have type
∀ (truth : var → bool) (p : prop), {propDenote truth p} + { ̃ propDenote truth p}.
This function is probably easiest to write in the usual tactical style, instead of
programming with refine. The function bool true dec may come in handy as a
hint.
(f) Define a function negate that returns a simplified version of the negation of a
prop. That is, the function should have type
∀ p : prop, {p’ : prop | ∀ truth, propDenote truth p ↔ ¬ propDenote truth p’ }
To simplify a variable, just
negate it. Simplify a negation by returning its argument. Simplify conjunctions
and disjunctions using De Morgan’s laws, negating the arguments recursively and
switching the kind of connective. Your decide function may be useful in some
of the proof obligations, even if you do not use it in the computational part of
negate’s definition. Lemmas like decide allow us to compensate for the lack of a
general Law of the Excluded Middle in CIC.