Rozwiązanie każdego ćwiczenia warto zacząć od:
Require Import CpdtTactics.
Set Implicit Arguments.
5. Define mutually inductive types of even and odd natural numbers,
such that any natural number is isomorphic to a value of one of the
two types. (This problem does not ask you to prove that
correspondence, though some interpretations of the task may be
interesting exercises.) Write a function that computes the sum of two
even numbers, such that the function type guarantees that the output
is even as well. Prove that this function is commutative.
6. Using a reflexive inductive definition, define a type nat tree of
infinitary trees, with natural numbers at their leaves and a countable
infinity of new trees branching out of each internal node. Define a
function increment that increments the number in every leaf of a nat
tree. Define a function leapfrog over a natural i and a tree nt.
leapfrog should recurse into the i th child of nt, the i+1st child of
that node, the i+2nd child of the next node, and so on, until
reaching a leaf, in which case leapfrog should return the number at
that leaf. Prove that the result of any call to leapfrog is
incremented by one by calling increment on the tree.
7. Define a type of trees of trees of trees of (repeat to infinity).
That is, define an inductive type trexp, whose members are either base
cases containing natural numbers or binary trees of trexps. Base your
definition on a parameterized binary tree type btree that you will
also define, so that trexp is defined as a nested inductive type.
Define a function total that sums all of the naturals at the leaves of
a trexp. Define a function increment that increments every leaf of a
trexp by one. Prove that, for all tr, total (increment tr ) >= total tr.
On the way to finishing this proof, you will probably want to prove a
lemma and add it as a hint using the syntax
Hint Resolve name_of_lemma.
8. Prove discrimination and injectivity theorems for the nat btree
type defined earlier in this chapter. In particular, without using the
tactics discriminate, injection, or congruence, prove that no leaf
equals any node, and prove that two equal nodes carry the same natural
number.
Inductive nat_btree : Set :=
| NLeaf : nat_btree
| NNode : nat_btree -> nat -> nat_btree -> nat_btree.