Contribution: DistributedReferenceCounting

# Library DistributedReferenceCounting.abstract.finite

Require Import List.
Require Export bibli.

Section DEFIN.

Variable E : Set.

Hypothesis eq_E_dec : eq_dec E.

Fixpoint only_once (x : E) (l : list E) {struct l} : Prop :=
match l with
| nil => False
| y :: l' =>
if eq_E_dec x y then ~ In x l' else only_once x l'
end.

Definition list_of_elements (l : list E) := forall x : E, only_once x l.

Lemma only_once_in : forall (l : list E) (x : E), only_once x l -> In x l.
Proof.
simple induction l.
auto.
simpl in |- *; intros a l0 hrec x.
case (eq_E_dec x a); auto.
Qed.

Lemma equality_from_membership :
forall (x y : E) (l : list E), In y l -> ~ In x l -> x <> y.
Proof.
simple induction l.
simpl in |- *; intuition.

intros a l' H.
simpl in |- *.
case (eq_E_dec a y).
intro e.
rewrite e.
intro H0.
intuition.

intros n H0 H1.
apply H.
auto.
intuition.
intuition.
Qed.

End DEFIN.

Section SUM.

Variable E : Set.

Fixpoint sigma (l1 : list E) : (E -> Z) -> Z :=
fun f : E -> Z =>
match l1 with
| nil => 0%Z
| e :: l2 => (f e + sigma l2 f)%Z
end.

Lemma sigma_null : forall l : list E, sigma l (fun e : E => 0%Z) = 0%Z.
Proof.
simple induction l; auto.
Qed.

Lemma sigma_pos :
forall (f : E -> Z) (l : list E),
(forall x_ : E, (f x_ >= 0)%Z) -> (sigma l f >= 0)%Z.
Proof.
intros; elim l; simpl in |- *.
omega.

intros; generalize (H a); omega.
Qed.

Lemma le_sigma :
forall (l : list E) (f : E -> Z) (x : E),
(forall x_ : E, (f x_ >= 0)%Z) -> In x l -> (f x <= sigma l f)%Z.
Proof.
simple induction l; simpl in |- *; intros.

decompose [or] H1.
rewrite H2; generalize (sigma_pos f l0 H0); omega.

generalize (H0 a); generalize (H f x H0 H2); omega.
Qed.

Lemma sigma_simpl :
forall (l : list E) (f g : E -> Z),
(forall x : E, In x l -> f x = g x) -> sigma l f = sigma l g.
Proof.
simple induction l.
auto.

simpl in |- *; intros.
rewrite (H f g).
rewrite (H0 a); auto.

auto.
Qed.

Remark le_sigma_sigma :
forall (l : list E) (f g : E -> Z),
(forall x : E, (f x <= g x)%Z) -> (sigma l f <= sigma l g)%Z.
Proof.
simple induction l; simpl in |- *; intros.
trivial with zarith.

generalize (H f g H0); generalize (H0 a); omega.
Qed.

Lemma ge_sigma_sigma :
forall (l : list E) (f g : E -> Z),
(forall x : E, (f x >= g x)%Z) -> (sigma l f >= sigma l g)%Z.
Proof.
intros; apply Zle_ge; apply le_sigma_sigma; intros; apply Zge_le; trivial.
Qed.

Hypothesis eq_E_dec : eq_dec E.

Lemma lt_sigma_sigma :
forall (l : list E) (f g : E -> Z),
(forall x : E, (f x <= g x)%Z) ->
(exists y : E, (f y < g y)%Z /\ In y l) -> (sigma l f < sigma l g)%Z.
Proof.
intros; elim H0; elim l; simpl in |- *; intros.

decompose [and or] H2.
rewrite H5; generalize (le_sigma_sigma l0 f g H); omega.

cut (sigma l0 f < sigma l0 g)%Z.
generalize (H a); omega.

apply (H1 x); auto.
Qed.

End SUM.

Section SIGMA_BUT.

Variable E : Set.

Variable x0 : E.

Hypothesis eq_E_dec : eq_dec E.

Variable f : E -> Z.

Fixpoint sigma_but (l1 : list E) : (E -> Z) -> Z :=
fun f : E -> Z =>
match l1 with
| nil => 0%Z
| e :: l2 =>
if eq_E_dec e x0
then sigma_but l2 f
else (f e + sigma_but l2 f)%Z
end.

Lemma sigma_but_pos :
forall (f : E -> Z) (l : list E),
(forall x_ : E, (f x_ >= 0)%Z) -> (sigma_but l f >= 0)%Z.
Proof.
intros; elim l; simpl in |- *.
omega.
intros a l0 H0.
case (eq_E_dec a x0); intro.
auto.
generalize (H a); omega.
Qed.

Lemma sigma_sigma_but_not_in :
forall l : list E, ~ In x0 l -> sigma E l f = sigma_but l f.
Proof.
simple induction l.
simpl in |- *.
auto.

intros a l0 H H0.
case (eq_E_dec a x0).
intros e.
elim H0.
rewrite e; simpl in |- *.
left; auto.

intros n.
simpl in |- *.
rewrite case_ineq.
rewrite H.
auto.

generalize H0.
simpl in |- *.
intro H1.
generalize H1.
intuition.

auto.
Qed.

Lemma sigma_sigma_but :
forall l : list E,
only_once E eq_E_dec x0 l -> sigma E l f = (sigma_but l f + f x0)%Z.
Proof.
simple induction l.
simpl in |- *; intuition.

intros a l0 H H0.
case (eq_E_dec a x0).
intro; rewrite e; simpl in |- *.
rewrite case_eq.
rewrite sigma_sigma_but_not_in.
omega.

generalize H0; simpl in |- *.
rewrite e.
case (eq_E_dec x0 x0).
auto.

intuition.

intros n.
simpl in |- *.
rewrite case_ineq.
rewrite H.
omega.

generalize H0; simpl in |- *.
case (eq_E_dec x0 a).
intros e H1.
rewrite e in n.
elim n.
auto.

intro n0.
auto.

auto.
Qed.

Lemma sigma_but_simpl :
forall (l : list E) (f g : E -> Z),
(forall x : E, x <> x0 -> In x l -> f x = g x) ->
sigma_but l f = sigma_but l g.
Proof.
simple induction l.
auto.

simpl in |- *; intros.
case (eq_E_dec a x0).
intro e.
apply (H f0 g).
intros x H1 H2.
apply H0.
auto.

right; auto.

intro n.
rewrite H0.
rewrite (H f0 g).
auto.

intros x H1 H2.
apply H0.
auto.

right; auto.

auto.

left; auto.
Qed.

End SIGMA_BUT.