CPDT Exercise 5

gistfile1.txt

Section CPDT_Exercise_5.

Section Tree.

Variable A : Set.

CoInductive tree :=
 | Node : A -> tree -> tree -> tree.

CoInductive tree_eq : tree -> tree -> Prop :=
 | Tree_eq : forall v t1 t2 t3 t4,
   tree_eq t1 t2 -> tree_eq t3 t4 -> tree_eq (Node v t1 t3) (Node v t2 t4).

End Tree.

CoFixpoint everywhere {A : Set} (n : A) :=
 Node A n (everywhere n) (everywhere n).

CoFixpoint map {A B : Set} (f : A -> A -> B) (t1 t2 : tree A) :=
 match (t1, t2) with
 | (Node v1 x1 y1, Node v2 x2 y2) =>
   Node B (f v1 v2) (map f x1 x2) (map f y1 y2) end.

CoFixpoint falses :=
 Node bool false falses falses.

CoFixpoint true_false_aux (v : bool) (f : bool -> bool) :=
 Node bool v (true_false_aux (f v) f) (true_false_aux (f v) f).

CoFixpoint true_false :=
 true_false_aux true negb.

Require Import Bool.

Goal tree_eq true_false (map orb true_false falses).
Proof.
Abort.

End CPDT_Exercise_5.