Lvc.Constr.CSetGet

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import Util LengthEq EqDec Get AllInRel.
Require Import CSetNotation CSetTac CSetBasic CSetComputable ElemEq.

Set Implicit Arguments.

Notation "'list_union' L" := (fold_left union L ) (at level 40).

Lemma list_union_start {X} `{OrderedType X} (s: set X) L t
: s t
   s fold_left union L t.
Proof.
  intros. general induction L; simpl; eauto.
  eapply IHL; eauto. cset_tac; intuition.
Qed.

Lemma list_union_incl {X} `{OrderedType X} (L:list (set X)) (s s':set X)
  : ( n t, get L n t t s')
    s s'
    fold_left union L s s'.
Proof.
  intros. general induction L; simpl. eauto.
  assert (a s'). eapply H0; eauto using get.
  eapply IHL; eauto. intros. rewrite H0; eauto using get.
  cset_tac; intuition.
Qed.

Lemma incl_list_union {X} `{OrderedType X} (s: set X) L n t u
: get L n t
   s t
   s fold_left union L u.
Proof.
  intros. general induction L.
  + simpl. inv H0; eauto.
    - eapply list_union_start; cset_tac; intuition.
Qed.

Lemma list_union_get {X} `{OrderedType X} L (x:X) u
: x fold_left union L u
   { n : nat & { t : set X | get L n t x t} } + { x u }.
Proof.
  intros. general induction L; simpl in *; eauto.
  - decide (x a).
    + left; do 2 eexists; split; eauto using get.
    + edestruct IHL as [[? []]|]; eauto; dcr.
      × left. eauto using get.
      × right. cset_tac; intuition.
Qed.

Lemma get_list_union_map X Y `{OrderedType Y} (f:X set Y) L n x
: get L n x
   f x [<=] list_union (List.map f L).
Proof.
  intros. eapply incl_list_union.
  + eapply map_get_1; eauto.
  + reflexivity.
Qed.

Lemma get_in_incl X `{OrderedType X} (L:list X) s
: ( n x, get L n x x s)
   of_list L s.
Proof.
  intros. general induction L; simpl.
  - cset_tac; intuition.
  - exploit H0; eauto using get.
    exploit IHL; intros; eauto using get.
    cset_tac; intuition.
Qed.

Lemma get_in_of_list X `{OrderedType X} L n x
    : get L n x
       x of_list L.
Proof.
  intros. general induction H0; simpl; cset_tac; intuition.
Qed.

Lemma list_union_start_swap X `{OrderedType X} (L : list (set X)) s
: fold_left union L s [=] s list_union L.
Proof.
  general induction L; simpl; eauto.
  - cset_tac; intuition.
  - rewrite IHL. symmetry. rewrite IHL.
    hnf; intros. cset_tac; intuition.
Qed.

Lemma list_union_app X `{OrderedType X} (L L' : list (set X)) s
: fold_left union (L ++ L') s [=] fold_left union L s list_union L'.
Proof.
  general induction L; simpl; eauto using list_union_start_swap.
Qed.

Lemma list_union_cons X `{OrderedType X} s sl
: list_union (s :: sl) [=] s list_union sl.
Proof.
  simpl. setoid_rewrite list_union_start_swap.
  hnf; intros. cset_tac; intuition.
Qed.

Lemma incl_list_union_cons X `{OrderedType X} s sl
: list_union sl list_union (s :: sl).
Proof.
  simpl. setoid_rewrite list_union_start_swap at 2.
  cset_tac; intuition.
Qed.

Hint Resolve incl_list_union_cons : cset.

Ltac norm_lunion :=
 repeat match goal with
      | [ |- context [ fold_left union ?A ?B ]] ⇒
        match B with
          | emptyfail 1
          | _rewrite (list_union_start_swap A B)
        end
    end.

Instance fold_left_union_morphism X `{OrderedType X}:
  Proper (PIR2 Equal ==> Equal ==> Equal) (fold_left union).
Proof.
  unfold Proper, respectful; intros.
  general induction H0; simpl; eauto.
  - rewrite IHPIR2; eauto. reflexivity.
    rewrite H1, pf. reflexivity.
Qed.

Instance fold_left_subset_morphism X `{OrderedType X}:
  Proper (PIR2 Subset ==> Subset ==> Subset) (fold_left union).
Proof.
  unfold Proper, respectful; intros.
  general induction H0; simpl; eauto with cset.
  eapply IHPIR2. rewrite H1, pf; eauto.
Qed.

Lemma list_union_eq {X} `{OrderedType X} (L L':list (set X)) (s s':set X)
: length L = length L'
   ( n s t, get L n s get L' n t s [=] t)
   s [=] s'
   fold_left union L s [=] fold_left union L' s'.
Proof.
  intros. length_equify.
  general induction H0; simpl; eauto.
  exploit H1; eauto using get.
  rewrite H2, H3; eauto using get.
Qed.

Lemma list_union_f_incl X `{OrderedType X} Y (f g:Yset X) s
: ( n y, get s n y f y g y)
   list_union (List.map f s) list_union (List.map g s).
Proof.
  intros. general induction s; simpl; eauto.
  norm_lunion.
  rewrite IHs, H0; eauto using get; reflexivity.
Qed.

Lemma list_union_f_eq X `{OrderedType X} Y (f g:Yset X) s
: ( n y, get s n y f y [=] g y)
   list_union (List.map f s) [=] list_union (List.map g s).
Proof.
  intros. general induction s; simpl; eauto.
  norm_lunion.
  rewrite IHs, H0; eauto using get; eauto.
Qed.

Lemma list_union_f_union X `{OrderedType X} Y (f g:Yset X) s
: list_union (List.map f s) list_union (List.map g s) [=]
             list_union (List.map (fun xf x g x) s).
Proof.
  intros. general induction s; simpl; eauto.
  - cset_tac; intuition.
  - norm_lunion.
    rewrite <- IHs; eauto using get. cset_tac.
Qed.

Lemma list_union_minus_dist X `{OrderedType X} D'' s s' L
  :
    s \ D'' [=] s'
  fold_left union L s \ D''
[=] fold_left union (List.map (fun ss \ D'') L) s'.
Proof.
  general induction L; simpl; eauto.
  - eapply IHL. rewrite <- H0.
    clear_all; cset_tac; intuition.
Qed.

Require Import CSetDisjoint.

Lemma list_union_disjunct {X} `{OrderedType X} Y D
: ( (n : nat) (D' : set X), get Y n D' disj D' D)
    disj (list_union Y) D.
Proof.
  split; intros.
  - eapply disj_intersection.
    eapply set_incl;[ cset_tac|].
    hnf; intros.
    general induction Y; simpl in × |- ×.
    + cset_tac.
    + exploit H0; eauto using get.
      exploit IHY; intros; eauto using get.
      rewrite list_union_start_swap.
      rewrite list_union_start_swap in H1.
      cset_tac.
  - eapply disj_1_incl; eauto.
    eapply incl_list_union; eauto.
Qed.

Lemma list_union_indexwise_ext X `{OrderedType X} Y (f:Yset X) Z (g:Z set X) L L'
: length L = length L'
   ( n y z, get L n y get L' n z f y [=] g z)
   list_union (List.map f L) [=] list_union (List.map g L').
Proof.
  intros. length_equify.
  general induction H0; simpl; eauto.
  rewrite list_union_start_swap.
  setoid_rewrite list_union_start_swap at 2.
  rewrite IHlength_eq, H1; eauto using get; reflexivity.
Qed.

Lemma list_union_rev X `{OrderedType X} (L:list (set X)) s
: fold_left union L s [=] fold_left union (rev L) s.
Proof.
  general induction L; simpl; eauto.
  rewrite list_union_app.
  simpl.
  rewrite IHL.
  rewrite list_union_start_swap.
  setoid_rewrite list_union_start_swap at 2.
  hnf; intros. clear_all; cset_tac; intuition.
Qed.

Require Import Drop.

Lemma list_union_drop_incl X `{OrderedType X} (L:list (set X)) n
: list_union (drop n L) list_union L.
Proof.
  intros; hnf; intros.
  edestruct list_union_get; eauto; dcr.
  eapply incl_list_union; eauto using get_drop. reflexivity.
  cset_tac; intuition.
Qed.

Lemma get_InA_OT X `{OrderedType X} (L:list X) n x
  : get L n x
      InA _eq x L.
Proof.
  intros Get. general induction Get; eauto using InA.
Qed.

Lemma get_InA X (L:list X) n x
  : get L n x
      InA eq x L.
Proof.
  intros Get. general induction Get; eauto using InA.
Qed.

Lemma get_elements_in X `{OrderedType X} s n x
  : get (elements s) n x
      x s.
Proof.
  intros Get. eapply get_InA_OT in Get.
  rewrite (@InA_in X H) in Get.
  rewrite of_list_elements in Get. eauto.
Qed.

Lemma of_list_get_first X `{OrderedType X} (Z:list X) z
: z of_list Z
   n z', get Z n z' z === z' ( n' z', n' < n get Z n' z' z' =/= z).
Proof.
  intros. general induction Z; simpl in ×. cset_tac; intuition.
  decide (z === a).
  - eexists 0, a; repeat split; eauto using get.
    + intros. exfalso. omega.
  - cset_tac'; intuition. edestruct IHZ; eauto. dcr.
    eexists (S x), x0; repeat split; eauto using get.
    + intros. inv H4; intro; eauto. eapply H5; eauto. omega.
Qed.

Lemma get_InA_R X (R:X X Prop) `{Reflexive X R} (L:list X) n x
  : Get.get L n x
      InA R x L.
Proof.
  revert_until X. clear.
  intros. general induction H0; eauto using InA.
Qed.

Lemma NoDupA_get_neq' X (R:X X Prop) `{Reflexive X R}
      `{Transitive X R}
      (L:list X) n x m y
  : NoDupA R L
     n < m
     Get.get L n x
     Get.get L m y
     ¬ R x y.
Proof.
  revert_until X. clear.
  intros.
  general induction H3; invt NoDupA.
  inv H4; try omega.
  eapply get_InA_R in H10; eauto.
  - revert H0 H6 H10 ; clear.
    intros. general induction H10.
    + intro. eapply H6. econstructor; eauto.
    + intro. eapply IHInA; eauto.
  - inv H4; try omega.
    eapply IHget; try eapply H11; eauto; omega.
Qed.

Lemma NoDupA_get_neq X (R:X X Prop) `{Reflexive X R}
      `{Symmetric X R}
      `{Transitive X R}
      (L:list X) n x m y
  : NoDupA R L
     n m
     Get.get L n x
     Get.get L m y
     ¬ R x y.
Proof.
  intros.
  decide (n < m).
  - eapply NoDupA_get_neq'; eauto.
  - assert (m < n) by omega.
    intro. symmetry in H7.
    eapply NoDupA_get_neq'; eauto.
Qed.

Lemma of_list_list_union
      (X : Type)
      `{OrderedType X}
      (s : X)
      (L : list X)
  :
    s of_list L s list_union L
.
Proof.
  intro s_in.
  apply of_list_1 in s_in.
  induction s_in;
    simpl in *; eauto.
  - rewrite H0.
    apply list_union_start.
    cset_tac.
  - rewrite list_union_start_swap, IHs_in.
    cset_tac.
Qed.

Lemma list_union_elem_eq_ext
      (X : Type)
      `{OrderedType X}
      (L L' : list X)
  :
    elem_eq L L'
     list_union L [=] list_union L'
.
Proof.
  intros. unfold elem_eq in H0.
  enough ( (l l' : list X),
                    of_list l of_list l'
                     list_union l list_union l') as enouf.
  {
    unfold elem_eq.
    apply eq_incl in H0 as [incl1 incl2].
    apply incl_eq; eauto.
  }
  clear L L' H0.
  intros.
  general induction l;
    simpl in *; eauto.
  - cset_tac.
  - norm_lunion.
    rewrite add_union_singleton in H0.
    assert (a list_union l') as a_sub.
    {
      apply of_list_list_union; eauto.
      clear IHl; cset_tac.
    }
    rewrite a_sub.
    rewrite IHl with (l':=l'); eauto.
    clear; cset_tac.
    cset_tac.
Qed.