Representing trees with functions (continued)
Consider the following inductive types for binary trees (with nodes
labeled by integers).
Require Import ZArith.
Inductive Z_btree : Set :=
Z_leaf : Z_btree |
Z_bnode : Z -> Z_btree -> Z_btree -> Z_btree.
Inductive Z_fbtree : Set :=
| Z_fleaf : Z_fbtree
| Z_fnode : Z -> (bool -> Z_fbtree) -> Z_fbtree.
Define functions :
f1 : Z_btree : Z_fbtree
f2 : Z_fbtree : Z_btree
that establish the most natural bijection between the two types.
Prove the following theorem:
Theorem f2_f1 : forall t: Z_btree, f2 (f1 t) = t.
What is missing to prove the following statement?
Theorem f1_f2 : forall t: Z_fbtree, f1 (f2 t) = t.