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.