(* File: Regular_Avl.v  (last edited on 27/10/2000) (c) Klaus Weich  *)

(* An AVL tree of lists is called regular iff, for each entry l,   *)
(* we have l\not= nil                                             *)

Require Import List.
Require Import ML_Int.
Require Import AvlTrees.

Section Regular_Avl.

Variable A : Set.

Definition Regular (t : avl_tree (list A)) :=
  forall (k : Int) (d : list A), lookup (list A) k t d -> d = nil -> False.

Remark regular_nil : Regular (Avl_Nil (list A)).
(* Goal: Regular t' *)
unfold Regular in |- *.
(* Goal: forall (k : Int) (d : list A) (_ : lookup (list A) k t' d) (_ : @eq (list A) d (@nil A)), False *)
intros k d lookup eq_d.
(* Goal: False *)
inversion_clear lookup.
Qed.


Remark regular_equiv_del :
 forall (key : Int) (t t' : avl_tree (list A)),
 Regular t -> equiv_del (list A) key t t' -> Regular t'.
(* Goal: forall (key : Int) (t t' : avl_tree (list A)) (_ : Regular t) (_ : equiv_del (list A) key t t'), Regular t' *)
intros key t t' reg_t equiv_del.
(* Goal: Regular t' *)
unfold Regular in |- *.
(* Goal: forall (k : Int) (d : list A) (_ : lookup (list A) k t' d) (_ : @eq (list A) d (@nil A)), False *)
intros k d lookup eq_d.
(* Goal: False *)
elim (equal_dec k key).
(* Goal: forall _ : Equal k key, False *)
(* Goal: forall _ : not (Equal k key), False *)
intros eq_k.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
inversion_clear equiv_del.
(* Goal: False *)
(* Goal: forall _ : not (Equal k key), False *)
apply H with k d; assumption.
(* Goal: forall _ : not (Equal k key), False *)
intros not_eq_k.
(* Goal: False *)
apply reg_t with k d.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
inversion_clear equiv_del.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
apply H1; assumption.
(* Goal: @eq (list A) d (@nil A) *)
assumption.
Qed.



Remark regular_equiv_ins :
 forall (key : Int) (data : A) (t t' : avl_tree (list A)),
 is_avl (list A) t ->
 is_avl (list A) t' ->
 Regular t -> equiv_ins (list A) key (cons data) nil t t' -> Regular t'.
(* Goal: forall (key : Int) (data : A) (t t' : avl_tree (list A)) (_ : is_avl (list A) t) (_ : is_avl (list A) t') (_ : Regular t) (_ : equiv_ins (list A) key (@cons A data) (@nil A) t t'), Regular t' *)
intros key data t t' avl_t avl_t' reg_t equiv_ins.
(* Goal: Regular t' *)
unfold Regular in |- *.
(* Goal: forall (k : Int) (d : list A) (_ : lookup (list A) k t' d) (_ : @eq (list A) d (@nil A)), False *)
intros k d lookup eq_d.
(* Goal: False *)
elim (equal_dec k key).
(* Goal: forall _ : Equal k key, False *)
(* Goal: forall _ : not (Equal k key), False *)
intros eq_k.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
inversion_clear equiv_ins.
(* Goal: False *)
(* Goal: forall _ : not (Equal k key), False *)
clear H1 H2.
(* Goal: False *)
(* Goal: forall _ : not (Equal k key), False *)
elim (lookup_dec (list A) k t avl_t).
(* Goal: forall (d : list A) (_ : AvlTrees.lookup (list A) k t d), False *)
(* Goal: forall _ : forall d : list A, not (AvlTrees.lookup (list A) k t d), False *)
(* Goal: forall _ : not (Equal k key), False *)
intros d0 lookup0.
(* Goal: False *)
(* Goal: forall _ : forall d : list A, not (AvlTrees.lookup (list A) k t d), False *)
(* Goal: forall _ : not (Equal k key), False *)
cut (d = data :: d0).
(* Goal: forall _ : @eq (list A) d (@cons A data (@nil A)), False *)
(* Goal: @eq (list A) d (@cons A data (@nil A)) *)
(* Goal: forall _ : not (Equal k key), False *)
 rewrite eq_d.
intro x;  discriminate x.
(* Goal: @eq (list A) d (@cons A data (@nil A)) *)
(* Goal: forall _ : not (Equal k key), False *)
apply (lookup_avl_equal (list A) k k t').
(* Goal: @eq (list A) d (@nil A) *)
assumption.
(* Goal: @eq (list A) d (@nil A) *)
assumption.
(* Goal: @eq (list A) d (@nil A) *)
apply H; assumption.
(* Goal: Equal k k *)
(* Goal: forall _ : not (Equal k key), False *)
apply equal_refl.
(* Goal: forall _ : forall d : list A, not (AvlTrees.lookup (list A) k t d), False *)
(* Goal: forall _ : not (Equal k key), False *)
intros not_lookup0.
(* Goal: False *)
(* Goal: forall _ : not (Equal k key), False *)
cut (d = data :: nil).
(* Goal: forall _ : @eq (list A) d (@cons A data (@nil A)), False *)
(* Goal: @eq (list A) d (@cons A data (@nil A)) *)
(* Goal: forall _ : not (Equal k key), False *)
 rewrite eq_d.
intro x;  discriminate x.
(* Goal: @eq (list A) d (@cons A data (@nil A)) *)
(* Goal: forall _ : not (Equal k key), False *)
apply (lookup_avl_equal (list A) k k t').
(* Goal: @eq (list A) d (@nil A) *)
assumption.
(* Goal: @eq (list A) d (@nil A) *)
assumption.
(* Goal: @eq (list A) d (@nil A) *)
apply H0; assumption.
(* Goal: Equal k k *)
(* Goal: forall _ : not (Equal k key), False *)
apply equal_refl.

(* Goal: forall _ : not (Equal k key), False *)
intros not_equal_k.
(* Goal: False *)
apply reg_t with k d.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup (list A) k t d *)
(* Goal: @eq (list A) d (@nil A) *)
clear H H0.
(* Goal: @eq (list A) d (@nil A) *)
apply H2; assumption.
(* Goal: @eq (list A) d (@nil A) *)
assumption.
Qed.


(***********************************************************************)

Definition REGULAR (t : AVL (list A)) :=
  match t with
  | AVL_intro t _ => Regular t
  end.


Lemma regular_AVL_NIL : REGULAR (AVL_NIL (list A)).
(* Goal: forall (_ : REGULAR (AVL_intro (list A) t avl_t)) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) (AVL_intro (list A) t avl_t) (AVL_intro (list A) t' avl_t')), REGULAR (AVL_intro (list A) t' avl_t') *)
simpl in |- *.
(* Goal: Regular (Avl_Nil (list A)) *)
exact regular_nil.
Qed.


Lemma regular_EQUIV_DEL :
 forall (key : Int) (T T' : AVL (list A)),
 REGULAR T -> EQUIV_DEL (list A) key T T' -> REGULAR T'.
(* Goal: forall (key : Int) (T T' : AVL (list A)) (_ : REGULAR T) (_ : EQUIV_DEL (list A) key T T'), REGULAR T' *)
intros key T T'.
(* Goal: forall (_ : REGULAR T) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) T T'), REGULAR T' *)
elim T; clear T; intros t avl_t.
(* Goal: forall (_ : REGULAR (AVL_intro (list A) t avl_t)) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) (AVL_intro (list A) t avl_t) T'), REGULAR T' *)
elim T'; clear T'; intros t' avl_t'.
(* Goal: forall (_ : REGULAR (AVL_intro (list A) t avl_t)) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) (AVL_intro (list A) t avl_t) (AVL_intro (list A) t' avl_t')), REGULAR (AVL_intro (list A) t' avl_t') *)
simpl in |- *.
(* Goal: forall (_ : Regular t) (_ : equiv_del (list A) key t t'), Regular t' *)
intros reg_t equiv_del.
(* Goal: @eq (list A) d (@nil A) *)
apply regular_equiv_del with key t; assumption.
Qed.


Lemma regular_EQUIV_INS :
 forall (key : Int) (data : A) (T T' : AVL (list A)),
 REGULAR T -> EQUIV_INS (list A) key (cons data) nil T T' -> REGULAR T'.
(* Goal: forall (key : Int) (data : A) (T T' : AVL (list A)) (_ : REGULAR T) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) T T'), REGULAR T' *)
intros key data T T'.
(* Goal: forall (_ : REGULAR T) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) T T'), REGULAR T' *)
elim T; clear T; intros t avl_t.
(* Goal: forall (_ : REGULAR (AVL_intro (list A) t avl_t)) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) (AVL_intro (list A) t avl_t) T'), REGULAR T' *)
elim T'; clear T'; intros t' avl_t'.
(* Goal: forall (_ : REGULAR (AVL_intro (list A) t avl_t)) (_ : EQUIV_INS (list A) key (@cons A data) (@nil A) (AVL_intro (list A) t avl_t) (AVL_intro (list A) t' avl_t')), REGULAR (AVL_intro (list A) t' avl_t') *)
simpl in |- *.
(* Goal: forall (_ : Regular t) (_ : equiv_ins (list A) key (@cons A data) (@nil A) t t'), Regular t' *)
intros reg_t equiv_ins.
(* Goal: @eq (list A) d (@nil A) *)
apply regular_equiv_ins with key data t; assumption.
Qed.



End Regular_Avl.