Library TabTree
Require Export PosInf.
Require Export ZArith.
Section TabTree.
Variable A : Set.
Variable bot : A.
Inductive tree : Set :=
| leaf : tree
| node : A -> tree -> tree -> tree.
Fixpoint apply_tree (t : tree) (p : BinPos.positive) {struct t} : A :=
match t with
| leaf => bot
| node a tO tI =>
match p with
| BinPos.xH => a
| BinPos.xO p => apply_tree tO p
| BinPos.xI p => apply_tree tI p
end
end.
Fixpoint subst_leaf (p : BinPos.positive) (v : A) {struct p} : tree :=
match p with
| BinPos.xH => node v leaf leaf
| BinPos.xO p' => node bot (subst_leaf p' v) leaf
| BinPos.xI p' => node bot leaf (subst_leaf p' v)
end.
Lemma apply_subst_leaf1 :
forall (p : BinPos.positive) (v : A), apply_tree (subst_leaf p v) p = v.
induction p; simpl in |- *; intuition.
Qed.
Lemma apply_subst_leaf2 :
forall (p1 p2 : BinPos.positive) (v : A),
p2 <> p1 -> apply_tree (subst_leaf p1 v) p2 = bot.
induction p1; simpl in |- *.
destruct p2 as [p| p| ]; intuition.
apply IHp1.
intros; elim H; subst; auto.
destruct p2 as [p| p| ]; intuition.
apply IHp1.
intros; elim H; subst; auto.
destruct p2 as [p| p| ]; intuition.
Qed.
Fixpoint modify_tree (t : tree) (p : BinPos.positive)
(f : A -> A) {struct t} : tree :=
match t with
| leaf => subst_leaf p (f bot)
| node a tO tI =>
match p with
| BinPos.xH => node (f a) tO tI
| BinPos.xO p' => node a (modify_tree tO p' f) tI
| BinPos.xI p' => node a tO (modify_tree tI p' f)
end
end.
Lemma apply_modify_tree1 :
forall (t : tree) (p : BinPos.positive) (f : A -> A),
apply_tree (modify_tree t p f) p = f (apply_tree t p).
induction t; intros; simpl in |- *.
apply apply_subst_leaf1.
case p; simpl in |- *; auto.
Qed.
Lemma apply_modify_tree2 :
forall (t : tree) (p x : BinPos.positive) (f : A -> A),
x <> p -> apply_tree (modify_tree t p f) x = apply_tree t x.
induction t; intros; simpl in |- *.
apply apply_subst_leaf2; assumption.
generalize H; case x; case p; intros; simpl in |- *; auto.
apply IHt2.
red in |- *; intros; elim H0; subst; auto.
apply IHt1.
red in |- *; intros; elim H0; subst; auto.
elim H0; reflexivity.
Qed.
Definition subst_tree (t : tree) (p : BinPos.positive)
(v : A) := modify_tree t p (fun _ => v).
Lemma apply_subst_tree1 :
forall (t : tree) (p : BinPos.positive) (v : A),
apply_tree (subst_tree t p v) p = v.
intros; unfold subst_tree in |- *.
apply apply_modify_tree1 with (f:= fun x : A => v).
Qed.
Lemma apply_subst_tree2 :
forall (t : tree) (p x : BinPos.positive) (v : A),
x <> p -> apply_tree (subst_tree t p v) x = apply_tree t x.
intros; unfold subst_tree in |- *.
apply apply_modify_tree2 with (f:= fun x : A => v).
assumption.
Qed.
End TabTree.
Section set.
Variable A:Set.
Variable bot:A.
Fixpoint modify_set_tree (t : tree A) (s : tree bool)
(f : A -> A) {struct s} : tree A :=
match t,s with
| _,leaf => t
| leaf,node true s1 s2 => node _ (f bot) (modify_set_tree (leaf _) s1 f) (modify_set_tree (leaf _) s2 f)
| leaf,node false s1 s2 => node _ bot (modify_set_tree (leaf _) s1 f) (modify_set_tree (leaf _) s2 f)
| node a tO tI,node true s1 s2 =>
node _ (f a) (modify_set_tree tO s1 f) (modify_set_tree tI s2 f)
| node a tO tI,node false s1 s2 =>
node _ a (modify_set_tree tO s1 f) (modify_set_tree tI s2 f)
end.
Lemma apply_modify_set_tree1 :
forall s t f p,
apply_tree bool false s p = true ->
apply_tree A bot (modify_set_tree t s f) p = f (apply_tree A bot t p).
induction s; intros; simpl in |- *.
simpl in H; discriminate H.
destruct t; simpl.
destruct a; simpl in H |- *; destruct p; auto.
rewrite IHs2; auto.
rewrite IHs1; auto.
rewrite IHs2; auto.
rewrite IHs1; auto.
discriminate H.
destruct a; simpl in H |- *; destruct p; auto.
discriminate H.
Qed.
Lemma apply_modify_set_tree :
forall s t f p,
apply_tree bool false s p = false ->
apply_tree A bot (modify_set_tree t s f) p = apply_tree A bot t p.
induction s; intros; simpl in |- *.
destruct t; simpl; auto.
destruct t; simpl.
destruct a; simpl in H |- *; destruct p; auto.
rewrite IHs2; auto.
rewrite IHs1; auto.
discriminate H.
rewrite IHs2; auto.
rewrite IHs1; auto.
destruct a; simpl in H |- *; destruct p; auto.
discriminate H.
Qed.
Variable f : A -> A -> A.
Variable R : A -> A -> Prop.
Variable Hyp1 : forall a1 a2, R a1 (f a1 a2).
Variable Hyp2 : forall a1 a2, R a2 (f a1 a2).
Variable Hyp3 : forall a, R bot a.
Variable Hyp4 : forall a1 a2 a3, R a1 a2 -> R a2 a3 -> R a1 a3.
Fixpoint apply_set_tree (t : tree A) (s : tree bool) {struct s} : A :=
match t,s with
| _,leaf => bot
| leaf,_ => bot
| node a tO tI,node true s1 s2 =>
f a (f (apply_set_tree tO s1) (apply_set_tree tI s2))
| node a tO tI,node false s1 s2 =>
(f (apply_set_tree tO s1) (apply_set_tree tI s2))
end.
Lemma apply_set_tree1 :
forall s t p,
apply_tree bool false s p = true ->
R (apply_tree A bot t p) (apply_set_tree t s).
induction s; intros; simpl in |- *.
simpl in H; discriminate H.
destruct t; simpl.
auto.
destruct a; simpl in H |- *; destruct p; auto.
apply Hyp4 with (f (apply_set_tree t1 s1) (apply_set_tree t2 s2)); auto.
apply Hyp4 with (apply_set_tree t2 s2); auto.
apply Hyp4 with (f (apply_set_tree t1 s1) (apply_set_tree t2 s2)); auto.
apply Hyp4 with (apply_set_tree t1 s1); auto.
apply Hyp4 with (apply_set_tree t2 s2); auto.
apply Hyp4 with (apply_set_tree t1 s1); auto.
discriminate H.
Qed.
End set.
Lemma positive_dec : forall p1 p2 : BinPos.positive, {p1 = p2} + {p1 <> p2}.
induction p1; intros.
case p2; intros.
case (IHp1 p); intros.
left; rewrite e; auto.
right; red in |- *; intros H'; elim n; injection H'; auto.
right; red in |- *; intros H'; discriminate H'.
right; red in |- *; intros H'; discriminate H'.
case p2; intros.
right; red in |- *; intros H'; discriminate H'.
case (IHp1 p); intros.
left; rewrite e; auto.
right; red in |- *; intros H'; elim n; injection H'; auto.
right; red in |- *; intros H'; discriminate H'.
case p2; intros.
right; red in |- *; intros H'; discriminate H'.
right; red in |- *; intros H'; discriminate H'.
left; auto.
Qed.
Fixpoint log_positive (p : BinPos.positive) : nat :=
match p with
| BinPos.xH => 0
| BinPos.xO p' => S (log_positive p')
| BinPos.xI p' => S (log_positive p')
end.
Lemma inf_log_trans :
forall (max : nat) (p2 p1 : BinPos.positive),
inf_log p2 max ->
(p1 ?= p2)%positive Datatypes.Eq = Datatypes.Lt -> inf_log p1 max.
induction max.
intros p2 p1 H.
inversion_clear H.
case p1; simpl in |- *; intros; try discriminate H.
simple destruct p2.
intros p p1 H; inversion_clear H.
case p1; simpl in |- *; intros; constructor; auto.
apply IHmax with p; auto.
elim (BinPos.Pcompare_Lt_Lt _ _ H); intros.
apply IHmax with p; auto.
rewrite H1; auto.
intros p p1 H; inversion_clear H.
case p1; simpl in |- *; intros; constructor; auto.
apply IHmax with p; auto.
apply BinPos.Pcompare_Gt_Lt; auto.
apply IHmax with p; auto.
simple destruct p1; simpl in |- *; intros; try discriminate H0.
Qed.
Lemma inf_log_dec :
forall (p : BinPos.positive) (n : nat), {inf_log p n} + {~ inf_log p n}.
induction p; intros.
case n; intros.
right; intros H; inversion H.
case (IHp n0); intros.
left; constructor; auto.
right; intros H; inversion_clear H; elim n1; auto.
case n; intros.
right; intros H; inversion H.
case (IHp n0); intros.
left; constructor; auto.
right; intros H; inversion_clear H; elim n1; auto.
left; constructor.
Qed.
Lemma log_inf_log_positive :
forall p : BinPos.positive, inf_log p (log_positive p).
induction p; simpl in |- *; intros; constructor; auto.
Qed.
Lemma max_inf_log_trans :
forall (p2 p1 : BinPos.positive) (n : nat),
inf_log p1 n -> ~ inf_log p2 n -> inf_log p1 (log_positive p2).
induction p2; simpl in |- *.
simple destruct p1.
intros p n H; inversion_clear H; intros.
constructor; apply IHp2 with n0; auto.
red in |- *; intros H'; elim H; constructor; auto.
intros p n H; inversion_clear H; intros.
constructor; apply IHp2 with n0; auto.
red in |- *; intros H'; elim H; constructor; auto.
intros; constructor.
simple destruct p1.
intros p n H; inversion_clear H; intros.
constructor; apply IHp2 with n0; auto.
red in |- *; intros H'; elim H; constructor; auto.
intros p n H; inversion_clear H; intros.
constructor; apply IHp2 with n0; auto.
red in |- *; intros H'; elim H; constructor; auto.
intros; constructor.
intros.
elim H0; constructor.
Qed.
Require Import List.
Section max_log_list.
Variable A : Set.
Variable f : A -> BinPos.positive.
Fixpoint max_log_list (l : list A) : nat :=
match l with
| nil => 0
| i :: q =>
let max := max_log_list q in
match inf_log_dec (f i) max with
| left _ => max
| right _ => log_positive (f i)
end
end.
Lemma in_inf_log :
forall (l : list A) (x : A), In x l -> inf_log (f x) (max_log_list l).
induction l; simpl in |- *.
intuition.
intros.
decompose [or] H.
subst.
case inf_log_dec; intros.
auto.
apply log_inf_log_positive.
case inf_log_dec; intros; auto.
apply max_inf_log_trans with (max_log_list l); auto.
Qed.
End max_log_list.
Section build_const_TabTree.
Variable A:Set.
Variable bot:A.
Variable const:A.
Fixpoint build_const_TabTree_rec (max:nat) : (tree A) :=
match max with
O => (node _ const (leaf _) (leaf _))
| S p => (node _ const (build_const_TabTree_rec p)
(build_const_TabTree_rec p))
end.
Lemma apply_build_const_TabTree_is_const :
forall (max:nat) (p:positive),
(inf_log p max) ->
(apply_tree A bot (build_const_TabTree_rec max) p)=const.
induction max; simpl; intros.
inversion_clear H; reflexivity.
inversion_clear H; simpl; auto.
Qed.
Lemma apply_build_const_TabTree_is_bot :
forall (max:nat) (p:positive),
~(inf_log p max) ->
(apply_tree A bot (build_const_TabTree_rec max) p)=bot.
induction max; simpl; intros.
generalize H; clear H.
case p; intros; simpl; auto.
elim H; constructor.
generalize H; clear H.
case p; intros; simpl; auto.
apply IHmax.
red; intros; elim H; constructor; auto.
apply IHmax.
red; intros; elim H; constructor; auto.
elim H; constructor.
Qed.
End build_const_TabTree.
Require Import Omega.
Lemma inf_log_trans' :
forall (max2 max1 : nat) (p : BinPos.positive),
inf_log p max1 -> max1 <= max2 -> inf_log p max2.
induction max2; intros.
inversion H0.
rewrite H1 in H; auto.
generalize H; clear H; case p; intros.
generalize H0; clear H0; inversion_clear H; intros; constructor.
apply IHmax2 with n; auto with zarith.
generalize H0; clear H0; inversion_clear H; intros; constructor.
apply IHmax2 with n; auto with zarith.
constructor.
Qed.
Index
This page has been generated by coqdoc