module Functions.Cases where open import Sets.Enumerated using (Bool; true; false)
Representation of negation as a function from Bool to Bool:
not : Bool → Bool not true = false not false = true
We pattern match on the elements that appear in the Bool set — that is true and false — in order to define how the function works.
Now we have got elements of Bool like as follows:
not true : Boolnot (not (not false)) : Bool
Note that these are not new elements: their normal form is still either true or false. In the interactive environment, we can compute those normal forms by the C-c C-n key combination.
The reason is that functions have a certain computational content. For example, not defines not only a relation between Bool and Bool, but it also presents an algorithm on how to compute the negated value.
The logical conjunction could be defined with pattern matching on all the possible four alternatives (that is, as a table), but here is a shorter definition with only two alternatives and with variables:
_∧_ : Bool → Bool → Bool true ∧ x = x false ∧ _ = false infixr 6 _∧_
Note the following:
We can use variables as patterns.
We can use wildcards (underscores) as patterns. A wildcard pattern can also be considered as an unnamed variable.
Similarly to data sets:
Underscores in names — such as _∧_ — denote the space for the operands.
The infixr keyword gives the associativity and precedence.
Define the logical disjunction as a function.
infixr 5 _∨_
_∨_ : Bool → Bool → Bool
Redefine the logical disjunction in a single line, with the help of not and _∧_ functions.
Define a set named Answer with three elements: yes, no, and maybe. Define the logical conjunction and disjunction operations on Answer.
Define a set named Quarter with four elements: east, west, north, and south. Define the turnLeft function with the following type:
turnLeft : Quarter → Quarter
For the previous exercise, define the turnBack and turnRight functions with the help of turnLeft.
turnRight : Quarter → Quarter
turnBack : Quarter → Quarter
(This can be done with either pattern matching or defining the function composition (_∘_) and using it.)
infixr 5 _∨_ _∨_ : Bool → Bool → Bool true ∨ _ = true -- false ∨ x = x --