Global Set Asymmetric Patterns.
Require Export Peano_dec.


Inductive nat_tree : Set :=
  | NIL : nat_tree
  | bin : nat → nat_tree → nat_tree → nat_tree.




Inductive binp : nat_tree → Prop :=
    binp_intro : ∀ (n : nat) (t1 t2 : nat_tree), binp (bin n t1 t2).

Hint Resolve binp_intro: searchtrees.

Lemma NIL_not_bin : ¬ binp NIL.
Proof.
 unfold not in |- *; intros H.
 inversion_clear H.
 Qed.
Hint Resolve NIL_not_bin: searchtrees.

Lemma diff_nil_bin : ∀ (n : nat) (t1 t2 : nat_tree), bin n t1 t2 ≠ NIL.
Proof.
 intros; discriminate.
Qed.

Hint Resolve diff_nil_bin: searchtrees.


Inductive occ : nat_tree → nat → Prop :=
  | occ_root : ∀ (n : nat) (t1 t2 : nat_tree), occ (bin n t1 t2) n
  | occ_l :
      ∀ (n p : nat) (t1 t2 : nat_tree), occ t1 p → occ (bin n t1 t2) p
  | occ_r :
      ∀ (n p : nat) (t1 t2 : nat_tree), occ t2 p → occ (bin n t1 t2) p.

Hint Resolve occ_root occ_l occ_r: searchtrees.

Definition member (n : nat) (t : nat_tree) := occ t n.

Derive Inversion_clear OCC_INV with
 (∀ (n p : nat) (t1 t2 : nat_tree), occ (bin n t1 t2) p).


Lemma occ_inv :
 ∀ (n p : nat) (t1 t2 : nat_tree),
 occ (bin n t1 t2) p → n = p ∨ occ t1 p ∨ occ t2 p.
Proof.
intros.
inversion H using OCC_INV; auto with searchtrees v62.
Qed.

Hint Resolve occ_inv: searchtrees.

Lemma not_occ_nil : ∀ p : nat, ¬ occ NIL p.
Proof.
unfold not in |- *; intros p H.
inversion_clear H.
Qed.

Hint Resolve not_occ_nil: searchtrees.