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.

Solution

This file

Going home

Pierre Castéran