Require Export Mark_abstract.
Load param.

(* For mark_gray to be defined, I need a coloration weight : the number
   of objects that are white or gray.
   This weight requires a priori the set of valid elements of A to be finite.

   Idea : all valid elements of A can be contained in a list.
*)

Require Export Arith.
Require Export Wf_nat.

Lemma le_refl_2 : forall p q, p = q -> p <= q.
intros ; subst ; apply le_n.
Qed.

Section Finite.

Variable A : Set.

Hypothesis eq_A_dec : forall a b : A, {a = b} + {a <> b}.

Definition elem_weight col (a : A) := match col a with
| Black => O
| _ => 1
end.

Fixpoint weight_l l col : nat :=
match l with
| nil => O
| a::m => elem_weight col a + @weight_l m col
end.

Lemma weight_extensional : forall l col1 col2,
(forall x, member x l -> col1 x = col2 x) -> weight_l l col1 = weight_l l col2.

Proof.
induction l ; auto.
introvars.
intro H.
simpl.
unfold elem_weight.
rewrite H.
 f_equal.
 apply IHl.
 intros.
 apply H ; apply member_tail ; auto.
 apply member_head.
Qed.

Lemma set_color_gray_weight_2 : forall l col a,
(col a = White \/ col a = Gray) ->
weight_l l col = weight_l l (set_color eq_A_dec a Gray col).

Proof.
induction l ; auto.
intros col a0 H.
simpl.
unfold elem_weight.
unfold set_color at 1.
destruct (eq_A_dec a a0).
 subst.
 destruct H ; rewrite H ; f_equal ; apply IHl ; auto.
f_equal ; apply IHl ; auto.
Qed.

Lemma set_color_black_weight_2 : forall l col a, member a l ->
(col a = White \/ col a = Gray) ->
weight_l l (set_color eq_A_dec a Black col) < weight_l l col.

Proof.
induction l.
 inversion 1.

 simpl.
 unfold elem_weight.
 unfold set_color at 1.
 intros col a0 H H0.
 destruct (eq_A_dec a a0).
  subst.
  apply plus_lt_le_compat.
  destruct H0 ; rewrite H0 ; auto with arith.
  destruct (member_dec eq_A_dec l a0).
   apply lt_le_weak.
   apply IHl ; auto.
  apply le_refl_2.
  apply weight_extensional.
  intros x H1.
  unfold set_color.
  destruct (eq_A_dec x a0) ; auto.
  subst ; contradiction.
 apply plus_lt_compat_l.
 apply IHl ; auto.
  inversion H ; subst ; auto.
  contradiction (refl_equal a).
Qed.

Section Finite_mark.

(* The following function shows that one can constructively decide whether
   to exhibit a gray object or to tell there is none.
   But it may remain unused in practice (there may be
   other functions deciding that.
 *)

Variable valid : A -> bool.

Example first_gray_finite_twolists :
forall q p col,
(forall a : A, (member a p -> col a = Gray -> False)) ->
(forall a, valid a = true -> {member a q} + {member a p}) ->
{a | valid a = true /\ col a = Gray} + {forall a, valid a = true -> col a = Gray -> False}.

Proof.
 induction q.
  intros.
  right.
  intros.
  destruct (H0 a) ; auto.
   inversion m.
   eapply H ; eauto.
  intros.
  case_eq (col a).
  intros.
  apply (IHq (a::p)).
  intros.
  inversion H2.
   subst. rewrite H3 in H1. discriminate.
   subst. eapply H ; eauto.
  intros.
  destruct (eq_A_dec a0 a).
   subst. right. apply member_head.
   destruct (H0 a0); auto.
    left. inversion m.
     subst. contradiction (refl_equal a).
     trivial.

  intros.
  case_eq (valid a).
  intros.
  left.
  exists a ; auto.
  intros.
  apply (IHq p); auto.
  intros a0 H3.
  destruct (H0 _ H3).
  left.
  inversion m.
  subst.
  discr.
  auto.
  auto.

  intros.
  apply (IHq (a::p)).
  intros.
  inversion H2.
   subst. rewrite H3 in H1. discriminate.
   subst. eapply H ; eauto.
  intros.
  destruct (eq_A_dec a0 a).
   subst. right. apply member_head.
   destruct (H0 a0); auto.
    left. inversion m.
     subst. contradiction (refl_equal a).
     trivial.

Defined.

Variable first_gray : (A -> color) -> option A.
Hypothesis Hfirst_gray_some : forall col a, first_gray col = Some a -> (valid a = true /\ col a = Gray).
Hypothesis Hfirst_gray_none : forall col, first_gray col = None ->forall a, valid a = true -> col a = Gray -> False. 

Variable B : Set.
Variable cache_is_full : B -> bool.
Variables (push pop : B -> B).


Variable children : A -> list A.
Variable raw : A -> bool.
Variable roots : list (A).

Section Finite_mark_term.

Variable lA : list A.
Hypothesis all_in_lA : forall a, valid a = true -> member a lA.

Definition weight := weight_l lA.
Hint Unfold weight.

Lemma set_color_gray_weight : forall col a,
(col a = White \/ col a = Gray) ->
weight col = weight (set_color eq_A_dec a Gray col).

Proof.
 unfold weight.
 apply set_color_gray_weight_2.
Qed.

Lemma set_color_black_weight : forall col a,
valid a = true ->
(col a = White \/ col a = Gray) ->
weight (set_color eq_A_dec a Black col) < weight col.

Proof.
 intros.
 unfold weight.
 apply set_color_black_weight_2 ; auto.
Qed.

Example first_gray_finite (col : A -> color) :
 {a | valid a = true /\ col a = Gray} + {forall a, valid a = true -> col a = Gray -> False}.

Proof.
 intros.
 apply first_gray_finite_twolists with lA (nil (A:=A)) .
  intros.
  inversion H.
  left ; auto.
Defined.

(* But (first_gray_finite) is only an example : one could
   find another function ad hoc.
*)

Let mark_block := mark_block  valid eq_A_dec cache_is_full push raw.
Hint Unfold mark_block.

Lemma mark_block_weight : forall col overflow cache cache_full a col2 o2 cache2 cache_full_2,
(col2, ((o2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
weight col2 <= weight col.

Proof.
unfold mark_block.
unfold Mark_abstract.mark_block.
introvars.
case_eq (valid a).
intro Hvalid.
case_eq (col a).
injection 2; intros; subst; auto.
injection 2; intros; subst; auto.
intro Hcol.
case (raw a).
injection 1 ; intros ; subst.
 apply lt_le_weak.
 apply set_color_black_weight ; auto.
injection 1 ; intros ; subst.
 apply le_refl_2.
 symmetry. 
 apply set_color_gray_weight ; auto.
injection 2; intros; subst; auto.
Qed.

Let mark_list := mark_list valid eq_A_dec cache_is_full push raw.

Lemma mark_list_weight : forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
weight col2 <= weight col.

Proof.
induction l.
unfold mark_list.
unfold Mark_abstract.mark_list.
intros ; injection H ; intros ; subst ; apply le_refl.
introvars.
change (mark_list col overflow cache cache_full (a::l)) with
(let (col3, p) := mark_block col overflow cache cache_full a in
 let (q, cache_full_3) := p in
 let (overflow3, cache3) := q in
 mark_list col3 overflow3 cache3 cache_full_3 l).
var (mark_block col overflow cache cache_full a).
destruct v as [? [[? ?] ?]].
intros.
apply le_trans with (weight c).
eapply IHl ; eauto.
eapply mark_block_weight ; eauto.
Qed.

Let mark_gray_term := mark_gray_term valid eq_A_dec first_gray cache_is_full push pop children raw.


Theorem mark_gray_term_finite : forall col overflow cache cache_full,
(forall x, member x cache -> col x = Gray) ->
(forall x, member x cache -> valid x = true) ->
no_duplicates cache ->
mark_gray_term col overflow cache cache_full.

Proof.
generalize (well_founded_ind (well_founded_ltof _ (weight))).
intro WF.
apply (WF (fun col => forall overflow cache cache_full, (forall x, member x cache -> col x = Gray) -> 
(forall x, member x cache -> valid x = true) -> no_duplicates cache ->
mark_gray_term col overflow cache cache_full)).
clear WF.
intros x IH overflow cache cache_full Hgray Hvalid Hno_dup.
setvar v (cache_pop first_gray pop x overflow cache cache_full) Hv.
destruct v as [[o l] b1].
destruct o ; unfold mark_gray_term.

 Focus 2.
 eapply Mark_gray_base ; eauto.

 setvar v (mark_list (set_color eq_A_dec a Black x) overflow l b1 (children a)) Hv0.
 destruct v as [c [[b l0] cf2]].
 eapply Mark_gray_call1; eauto.
 apply IH.
 unfold ltof.
 symmetry in Hv.
 symmetry in Hv0.
 apply le_lt_trans with (weight (set_color eq_A_dec a Black x)).
 eapply mark_list_weight ; eauto.
 apply set_color_black_weight.

 (* valid a = true *)
 eapply (cache_pop_valid_elem (A := A)).
 eassumption.
 eassumption.
 assumption.

 right.
 apply (cache_pop_gray_elem Hfirst_gray_some Hv) ; auto.
 symmetry in Hv0.
 apply (mark_list_gray_cache Hv0).
 intros.
 symmetry in Hv.
 unfold set_color.
 destruct (eq_A_dec x0 a).
 subst.
 destruct (cache_pop_not_mem Hv Hno_dup H).

 destruct (cache_pop_which Hv) as [H0 | ].
 inversion H0.
 subst.
 inversion H.
 subst.
 apply Hgray.
 apply member_tail.
 trivial.

 intros; 
 eapply (mark_list_cache_valid (A := A)).
 eauto.
 unfold mark_list in Hv0; eauto.
 intros;eapply (cache_pop_valid_cache (A := A)).
 eauto.
 auto.
 auto.
 auto.

 symmetry in Hv0.
 generalize (mark_list_no_dupl Hv0).
 intros.

 symmetry in Hv.
 apply H ; auto.
 2 : (apply (cache_pop_no_dupl Hv); trivial).

 intros.
 unfold set_color.
 destruct (eq_A_dec x0 a).
 subst.
 destruct (cache_pop_not_mem Hv Hno_dup H0).
 destruct (cache_pop_which Hv).
 inversion H1.
 subst.
 inversion H0.
 subst.
 apply Hgray.
 apply member_tail.
 trivial.
 
Qed.

Corollary gc_mark_term_finite cache_full : gc_mark_term valid eq_A_dec first_gray cache_is_full push pop children raw roots cache_full.

Proof.
(* inversion_clear HlA as [lA all_in_lA]. *)
unfold gc_mark_term.
intros.
apply mark_gray_term_finite (* with lA ; auto *).
intros.
apply (mark_list_gray_cache H). 
inversion 1.
trivial.
intros.
eapply (mark_list_cache_valid (A := A)).
eassumption.
inversion 1.
auto.

generalize (mark_list_no_dupl H).
intros.
apply H0.
inversion 1.
apply no_duplicates_nil.
Qed.

End Finite_mark_term.

Hypothesis HlA : exists lA, forall a : A, valid a = true -> member a lA.

Definition gc_mark_finite cache_full_0 :
 {col : _ & {overflow : _ & {cache : _ & {cache_full | gc_mark_prop valid eq_A_dec first_gray cache_is_full push pop children raw roots cache_full_0 col overflow cache cache_full}}}}.

Proof.
 intros.
 eapply gc_mark.
 inversion HlA.
 eapply gc_mark_term_finite ; eauto.
Defined.

End Finite_mark.

End Finite.

(* In such a way, A may be infinite, only {a : A | valid a = true} must be finite *)

(*
Recursive Extraction gc_mark_finite.
Print gc_mark_finite.
*)