Contribution: DistributedReferenceCounting

# Library DistributedReferenceCounting.abstract.bibli

Require Export Arith.
Require Export Omega.
Require Import List.

Section SEPAR.

Lemma eq_bool_dec : forall b : bool, {b = true} + {b = false}.
Proof.
simple induction b; auto.
Defined.

Definition eq_dec (E : Set) := forall a b : E, {a = b} + {a <> b}.

Lemma case_eq :
forall (E F : Set) (eq_E_dec : eq_dec E) (x : E) (y z : F),
match eq_E_dec x x with
| left _ => y
| right _ => z
end = y.
Proof.
intros; case (eq_E_dec x x).
auto.

intros; absurd (x = x); auto.
Qed.

Lemma case_ineq :
forall (E F : Set) (eq_E_dec : eq_dec E) (x x' : E) (y z : F),
x <> x' -> match eq_E_dec x x' with
| left _ => y
| right _ => z
end = z.
Proof.
intros; case (eq_E_dec x x').
intros; absurd (x = x'); auto.

trivial.
Qed.

Lemma eq_couple_dec :
forall (E F : Set) (eq_E_dec : eq_dec E) (eq_F_dec : eq_dec F)
(x1 x2 : E) (y1 y2 : F), {x1 = x2 /\ y1 = y2} + {x1 <> x2 \/ y1 <> y2}.
Proof.
intros; case (eq_E_dec x1 x2); case (eq_F_dec y1 y2); intros; auto.
Qed.

End SEPAR.

Section OTHER.

Definition Int (b : bool) := if b then 1%Z else 0%Z.

Lemma true_not_false : forall b : bool, b = true -> false <> b.
Proof.
intros; rewrite H; discriminate.
Qed.

Axiom
funct_eq :
forall (E F : Set) (g h : E -> F), (forall e : E, g e = h e) -> g = h.

Lemma in_not_in :
forall (E : Set) (a b : E) (l : list E), In a l -> ~ In b l -> a <> b.
Proof.
intros; red in |- *; intros.
elim H0; rewrite <- H1; auto.
Qed.

End OTHER.

Section PointFixe.

Variable A : Set.
Variable P : A -> Set.
Variable R : A -> A -> Prop.
Hypothesis Rwf : well_founded R.
Variable F : forall x : A, (forall y : A, R y x -> P y) -> P x.

Hypothesis
F_ext :
forall (x : A) (f g : forall y : A, R y x -> P y),
(forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g.

Fixpoint Fix_F (x : A) (r : Acc R x) {struct r} : P x :=
F x (fun (y : A) (p : R y x) => Fix_F y (Acc_inv r y p)).

Scheme Acc_inv_dep := Induction for Acc Sort Prop.

Lemma Fix_F_eq :
forall (x : A) (r : Acc R x),
Fix_F x r = F x (fun (y : A) (p : R y x) => Fix_F y (Acc_inv r y p)).
intros x r; elim r using Acc_inv_dep; auto.
Qed.

Lemma Fix_F_inv : forall (x : A) (r s : Acc R x), Fix_F x r = Fix_F x s.
intro x; elim (Rwf x); intros.
rewrite (Fix_F_eq x0 r); rewrite (Fix_F_eq x0 s); intros.
apply F_ext; auto.
Qed.

Definition Fix (x : A) := Fix_F x (Rwf x).

Lemma fix_eq : forall x : A, Fix x = F x (fun (y : A) (p : R y x) => Fix y).
intro; unfold Fix in |- *.
rewrite (Fix_F_eq x).
apply F_ext; intros.
apply Fix_F_inv.
Qed.

End PointFixe.

Section WF_ROOT.

Variable E : Set.

Variable f : E -> nat.

Variable R : E -> E -> Prop.

Hypothesis R_dec : forall x : E, {y : E | R y x} + {(forall y : E, ~ R y x)}.

Hypothesis strict : forall x y : E, R x y -> f x < f y.

Lemma lt_acc : forall (n : nat) (y : E), f y < n -> Acc R y.
Proof.
simple induction n.
intros; absurd (f y < 0); auto with v62.
intros; apply Acc_intro.
intros; apply H.
apply lt_le_trans with (m := f y); auto with v62.
Qed.

Lemma wf_R : well_founded R.
Proof.
unfold well_founded in |- *; intro.
apply Acc_intro; intros.
apply (lt_acc (f a)); auto.
Qed.

Definition F (x : E) (f : forall y : E, R y x -> E) :=
match R_dec x with
| inleft z => let (y0, r0) := z in f y0 r0
| inright _ => x
end.

Lemma F_eq :
forall (x : E) (f1 f2 : forall y : E, R y x -> E),
(forall (y : E) (r : R y x), f1 y r = f2 y r) -> F x f1 = F x f2.
Proof.
intros; unfold F in |- *; case (R_dec x); intros.
elim s; intros; auto.

trivial.
Qed.

Definition root := Fix E (fun _ : E => E) R wf_R F.

Definition root_eq := fix_eq E (fun _ : E => E) R wf_R F F_eq.

Lemma root_no_R : forall x y : E, ~ R y (root x).
Proof.
intros; elim (wf_R x).
intros; rewrite root_eq.
unfold F at 1 in |- *; case (R_dec x0); intros.
elim s; intros.
fold (root x1) in |- *; apply H0; trivial.

trivial.
Qed.

Lemma prop_root :
forall (P : E -> Prop) (x : E),
P x -> (forall y z : E, P y -> R z y -> P z) -> P (root x).
Proof.
intros; generalize H.
elim (wf_R x).
intros; unfold root in |- *; rewrite root_eq.
unfold F at 1 in |- *; case (R_dec x0); intros.
elim s; intros x1 y.
apply (H2 x1 y).
apply H0 with (y := x0); trivial.

trivial.
Qed.

End WF_ROOT.