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).