General Trees

(* GENERAL TREES         *)
(* by Venanzio Capretta  *)
(* Coq version 6.2.3     *)

(* Implementation of a type of general trees similar to the one defined in *)
(* Chapter 16 of Programming in Martin-Lof's Type Theory                   *)
(*               by Nordstrom, Petersson and Smith.                        *)
(* See also  A Set Constructor fo Inductive Sets in Martin-Lof's           *)
(*           Type Theory                                                   *)
(*           by Petersson and Synek.                                       *)

(* General Trees are a generalization of Martin-Lof's W-types,    *)
(* in which a family of types can be defined by mutual induction. *)

Require Export Setoids.

Implicit Arguments On.

Section General_Inductive_Trees.

Variable A : Set. (* sorts, index for the defined family. *)
Variable B : Set. (* constructors, or labels for the nodes of the trees. *)

Variable C : B -> Set.
(* For every constructor b : B, (C b) is the set of its arguments,     *)
(* or the set indexing the branches of a tree with a node labelled b.  *)

Variable f : B -> A.
(* For every constructor we specify to which elements of the defined  *)
(* family the elements constructed will belong.                       *)

Variable g : (b:B)(C b) -> A.
(* For ever argument c : (C b), (g b c) specifies to which element  *)
(* of the family the argument must belong.                          *)

Inductive General_Tree : A -> Set :=
  g_tree : (b : B)((x : (C b))(General_Tree (g x))) -> (General_Tree (f b)).

(* If b is a constructor (i. e. an element of B) and we have already    constucted, for each element x : (C b) a tree (h x) that belongs    to the element of the family of index (g b x), then we can    construct the new tree (tree a h) which has a node labelled by a    and has as subtrees all the (h x)'s. *)

Local T := General_Tree.

(* Extraction of the node and subtrees of a tree. *)

Definition g_node : (a:A)(T a) -> B :=
[a:A][t : (T a)]
Cases t of
  (g_tree b h) => b
end.

Definition g_sub_trees :
  (a:A)(t : (T a))(x : (C (g_node t)))(T (g x)) :=
[a][t]
<[a:A][t : (T a)](x : (C (g_node t)))(T (g x))>
Cases t of
  (g_tree b h) => h
end.

(* In general trees that have equal nodes and equal subtrees are    not equal: (tree b h1) and (tree b h2) do not need to be equal even    if (h1 x)=(h2 x) for all x:(C b). To have this kind of equality    we need to consider extensional equality for functions.    So the following notion of equality for trees is needed. *)

Inductive tree_eq : (a:A)(T a) -> (T a) -> Prop :=
    tree_eq_intro : (b:B)(h1, h2 : (x:(C b))(T (g x)))
                    ((x:(C b))(tree_eq (h1 x) (h2 x)))
                    -> (tree_eq (g_tree h1) (g_tree h2))
  | tree_eq_trans : (a:A)(t1, t2, t3 : (T a))
                    (tree_eq t1 t2) -> (tree_eq t2 t3)
                    -> (tree_eq t1 t3).

(* Transitivity must be required. It is provable only if we assume    uniqueness of proofs of equality. *)

(* tree_eq_dep is a dependent equivalence relation. *)

Lemma tree_eq_reflexive :
  (a:A)(Reflexive (!tree_eq a)).

Lemma tree_eq_symmetric :
  (a:A)(Symmetric (!tree_eq a)).

Lemma tree_eq_transitive : (a:A)(Transitive (!tree_eq a)).

Lemma tree_eq_equivalence : (a:A)(Equiv (!tree_eq a)).

(* Therefore general trees with the estensional equality  *)
(* tree_eq form a setoid.                                 *)

Definition General_Tree_Setoid : A -> Setoid :=
  [a](setoid (tree_eq_equivalence a)).

(* Two equal trees must have the same root. *)
Lemma equal_trees_same_node :
  (a : A)(t1, t2 : (General_Tree a))(tree_eq t1 t2) ->
  (g_node t1) = (g_node t2).

End General_Inductive_Trees.

Implicit Arguments Off.

25/02/99, 14:36