(**********************************************************************)
(*                Model checking under Coq : Test No 1                *)
(* 								      *)
(*                 Patrick Loiseleur, septembre 1997		      *)
(**********************************************************************)
(* Coq V6.3 *)

(* $Id: Btree.v,v 1.5 1999/06/29 07:49:02 loiseleu Exp $ *)

Require PolyList.
Require EqDecide.

Section binary_trees.

Implicit Arguments On.

Variable A : Set.

Inductive Set btree :=
  Empty_bt : btree
| Node_bt : A->btree->btree->btree.

Implicit Arguments Off.

Inductive bpath : Set :=
| Left_bp : bpath -> bpath
| Right_bp : bpath -> bpath
| End_bp : bpath.

Lemma bpath_eq_dec : (b1,b2:bpath){b1=b2}+{~b1=b2}.
Decide Equality.
Save.

Fixpoint bpath_eq [bp1, bp2:bpath] : bool := 
  Cases bp1 bp2 of
  | End_bp End_bp => true
  | (Right_bp bp3) (Right_bp bp4) => (bpath_eq bp3 bp4)
  | (Left_bp bp3) (Left_bp bp4) => (bpath_eq bp3 bp4)
  | _ _ => false
  end.

Inductive In_btree [x:A] : btree -> Prop :=
| In_end_bt : (t1,t2:btree) (In_btree x (Node_bt x t1 t2))
| In_left_bt : (t1,t2:btree) (In_btree x t1) 
    -> (In_btree x (Node_bt x t1 t2))
| In_right_bt : (t1,t2:btree) (In_btree x t2) 
    -> (In_btree x (Node_bt x t1 t2)).

Implicit Arguments On.


Fixpoint in_btree[x:A; t:btree] : Prop :=
  Cases t of
    Empty_bt => False
  | (Node_bt x1 t1 t2) => (x=x1)\/(in_btree x t1)\/(in_btree x t2)
  end.

Fixpoint flat_btree[t:btree] : (list A) :=
  Cases t of
    Empty_bt => (nil A)
  | (Node_bt x1 t1 t2) => 
      (cons x1 (app (flat_btree t1) (flat_btree t2)))
  end.

Fixpoint find_btree [p:bpath; t:btree] : (Exc A) :=
  Cases p t of
    End_bp (Node_bt x _ _) => (Value x)
  | (Right_bp p1) (Node_bt x t1 t2) => (find_btree p1 t2)
  | (Left_bp p1) (Node_bt x t1 t2) => (find_btree p1 t1)
  | _ _ => Error
  end.

Fixpoint valid_path[p: bpath; t:btree] : bool :=
  Cases p t of
    End_bp (Node_bt _ _ _) => true
  | (Right_bp p1) (Node_bt _ _ t2) => (valid_path p1 t2)
  | (Left_bp p1) (Node_bt _ t1 _) => (valid_path p1 t1)
  | _ _ => false
  end.

(* Lemma find_ok1 : *)



End binary_trees.

Implicit Arguments Off.


