# Library Coq.rtauto.Bintree

Require Export List.
Require Export BinPos.
Open Scope positive_scope.
Ltac clean := try (simpl; congruence).
Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
Lemma Gt_Eq_Gt : forall p q cmp,
(p ?= q) Eq = Gt -> (p ?= q) cmp = Gt.
Lemma Gt_Lt_Gt : forall p q cmp,
(p ?= q) Lt = Gt -> (p ?= q) cmp = Gt.
Lemma Gt_Psucc_Eq: forall p q,
(p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt.
Lemma Eq_Psucc_Gt: forall p q,
(p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt.
Lemma Gt_Psucc_Gt : forall n p cmp cmp0,
(n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt.
Lemma Gt_Psucc: forall p q,
(p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt.
Lemma Psucc_Gt : forall p,
(Psucc p ?= p) Eq = Gt.
Fixpoint pos_eq (m n:positive) {struct m} :bool :=
match m, n with
xI mm, xI nn => pos_eq mm nn
| xO mm, xO nn => pos_eq mm nn
| xH, xH => true
| _, _ => false
end.
Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
Theorem refl_pos_eq : forall m, pos_eq m m = true.
Definition pos_eq_dec : forall (m n:positive), {m=n}+{m<>n} .
Defined.
Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m).
Theorem pos_eq_dec_ex : forall m n,
pos_eq m n =true -> exists h:m=n,
pos_eq_dec m n = left _ h.
Fixpoint nat_eq (m n:nat) {struct m}: bool:=
match m, n with
O,O => true
| S mm,S nn => nat_eq mm nn
| _,_ => false
end.
Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n.
Theorem refl_nat_eq : forall n, nat_eq n n = true.
Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A :=
match l with nil => None
| x::q =>
match n with O => Some x
| S m => Lget A m q
end end .
Implicit Arguments Lget [A].
Lemma map_app : forall (A B:Set) (f:A -> B) l m,
List.map f (l ++ m) = List.map f l ++ List.map f m.
Lemma length_map : forall (A B:Set) (f:A -> B) l,
length (List.map f l) = length l.
Lemma Lget_map : forall (A B:Set) (f:A -> B) i l,
Lget i (List.map f l) =
match Lget i l with Some a =>
Some (f a) | None => None end.
Lemma Lget_app : forall (A:Set) (a:A) l i,
Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l.
Lemma Lget_app_Some : forall (A:Set) l delta i (a: A),
Lget i l = Some a ->
Lget i (l ++ delta) = Some a.
Section Store.
Variable A:Type.
Inductive Poption : Type:=
PSome : A -> Poption
| PNone : Poption.
Inductive Tree : Type :=
Tempty : Tree
| Branch0 : Tree -> Tree -> Tree
| Branch1 : A -> Tree -> Tree -> Tree.
Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption :=
match T with
Tempty => PNone
| Branch0 T1 T2 =>
match p with
xI pp => Tget pp T2
| xO pp => Tget pp T1
| xH => PNone
end
| Branch1 a T1 T2 =>
match p with
xI pp => Tget pp T2
| xO pp => Tget pp T1
| xH => PSome a
end
end.
Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree :=
match T with
| Tempty =>
match p with
| xI pp => Branch0 Tempty (Tadd pp a Tempty)
| xO pp => Branch0 (Tadd pp a Tempty) Tempty
| xH => Branch1 a Tempty Tempty
end
| Branch0 T1 T2 =>
match p with
| xI pp => Branch0 T1 (Tadd pp a T2)
| xO pp => Branch0 (Tadd pp a T1) T2
| xH => Branch1 a T1 T2
end
| Branch1 b T1 T2 =>
match p with
| xI pp => Branch1 b T1 (Tadd pp a T2)
| xO pp => Branch1 b (Tadd pp a T1) T2
| xH => Branch1 a T1 T2
end
end.
Definition mkBranch0 (T1 T2:Tree) :=
match T1,T2 with
Tempty ,Tempty => Tempty
| _,_ => Branch0 T1 T2
end.
Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree :=
match T with
| Tempty => Tempty
| Branch0 T1 T2 =>
match p with
| xI pp => mkBranch0 T1 (Tremove pp T2)
| xO pp => mkBranch0 (Tremove pp T1) T2
| xH => T
end
| Branch1 b T1 T2 =>
match p with
| xI pp => Branch1 b T1 (Tremove pp T2)
| xO pp => Branch1 b (Tremove pp T1) T2
| xH => mkBranch0 T1 T2
end
end.
Theorem Tget_Tempty: forall (p : positive), Tget p (Tempty) = PNone.
Theorem Tget_Tadd: forall i j a T,
Tget i (Tadd j a T) =
match (i ?= j) Eq with
Eq => PSome a
| Lt => Tget i T
| Gt => Tget i T
end.
Record Store : Type :=
mkStore {index:positive;contents:Tree}.
Definition empty := mkStore xH Tempty.
Definition push a S :=
mkStore (Psucc (index S)) (Tadd (index S) a (contents S)).
Definition get i S := Tget i (contents S).
Lemma get_empty : forall i, get i empty = PNone.
Inductive Full : Store -> Type:=
F_empty : Full empty
| F_push : forall a S, Full S -> Full (push a S).
Theorem get_Full_Gt : forall S, Full S ->
forall i, (i ?= index S) Eq = Gt -> get i S = PNone.
Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone.
Theorem get_push_Full :
forall i a S, Full S ->
get i (push a S) =
match (i ?= index S) Eq with
Eq => PSome a
| Lt => get i S
| Gt => PNone
end.
Lemma Full_push_compat : forall i a S, Full S ->
forall x, get i S = PSome x ->
get i (push a S) = PSome x.
Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty.
Lemma push_not_empty: forall a S, (push a S) <> empty.
Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop :=
match F with
F_empty => False
| F_push a SS FF => x=a \/ In x SS FF
end.
Lemma get_In : forall (x:A) (S:Store) (F:Full S) i ,
get i S = PSome x -> In x S F.
End Store.
Implicit Arguments PNone [A].
Implicit Arguments PSome [A].
Implicit Arguments Tempty [A].
Implicit Arguments Branch0 [A].
Implicit Arguments Branch1 [A].
Implicit Arguments Tget [A].
Implicit Arguments Tadd [A].
Implicit Arguments Tget_Tempty [A].
Implicit Arguments Tget_Tadd [A].
Implicit Arguments mkStore [A].
Implicit Arguments index [A].
Implicit Arguments contents [A].
Implicit Arguments empty [A].
Implicit Arguments get [A].
Implicit Arguments push [A].
Implicit Arguments get_empty [A].
Implicit Arguments get_push_Full [A].
Implicit Arguments Full [A].
Implicit Arguments F_empty [A].
Implicit Arguments F_push [A].
Implicit Arguments In [A].
Section Map.
Variables A B:Set.
Variable f: A -> B.
Fixpoint Tmap (T: Tree A) : Tree B :=
match T with
Tempty => Tempty
| Branch0 t1 t2 => Branch0 (Tmap t1) (Tmap t2)
| Branch1 a t1 t2 => Branch1 (f a) (Tmap t1) (Tmap t2)
end.
Lemma Tget_Tmap: forall T i,
Tget i (Tmap T)= match Tget i T with PNone => PNone
| PSome a => PSome (f a) end.
Lemma Tmap_Tadd: forall i a T,
Tmap (Tadd i a T) = Tadd i (f a) (Tmap T).
Definition map (S:Store A) : Store B :=
mkStore (index S) (Tmap (contents S)).
Lemma get_map: forall i S,
get i (map S)= match get i S with PNone => PNone
| PSome a => PSome (f a) end.
Lemma map_push: forall a S,
map (push a S) = push (f a) (map S).
Theorem Full_map : forall S, Full S -> Full (map S).
End Map.
Implicit Arguments Tmap [A B].
Implicit Arguments map [A B].
Implicit Arguments Full_map [A B f].
Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).