Library Coq.rtauto.Bintree
Require Export List.
Require Export BinPos.
Require Arith.EqNat.
Open Scope positive_scope.
Ltac clean :=
try (
simpl;
congruence).
Lemma Gt_Psucc:
forall p q,
(p ?= Pos.succ q) = Gt -> (p ?= q) = Gt.
Lemma Psucc_Gt :
forall p,
(Pos.succ p ?= p) = Gt.
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 .
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 Arith.EqNat.beq_nat 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.
Inductive Poption {
A} :
Type:=
PSome :
A -> Poption
|
PNone :
Poption.
Inductive Tree {
A} :
Type :=
Tempty :
Tree
|
Branch0 :
Tree -> Tree -> Tree
|
Branch1 :
A -> Tree -> Tree -> Tree.
Section Store.
Variable A:
Type.
Notation Poption := (
Poption A).
Notation Tree := (
Tree A).
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)
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 (
Pos.succ (
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) = 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)
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.
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.
Notation "hyps \ A" := (
push A hyps) (
at level 72,
left associativity).