Lvc.Constr.MapDefined

Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util AutoIndTac.
Require Export CSet Containers.SetDecide MoreList.
Require Export LengthEq MapBasics MapLookup MapUpdate MapComposition.

Set Implicit Arguments.

Definition defined_on {X} `{OrderedType X} {Y} (G:set X) (E:X option Y)
  := x, x G y, E x = Some y.

Lemma defined_on_update_some X `{OrderedType X} Y (G:set X) (E:X option Y) x v
  : defined_on (G \ {{x}}) E
     defined_on G (E [x <- Some v]).
Proof.
  unfold defined_on; intros. lud.
  - eauto.
  - eapply H0; eauto. cset_tac; intuition.
Qed.

Lemma defined_on_incl X `{OrderedType X} Y (G G':set X) (E:X option Y)
  : defined_on G E
     G' G
     defined_on G' E.
Proof.
  unfold defined_on; intros; eauto.
Qed.

Lemma defined_on_update_list X `{OrderedType X} Y lv (E: X option Y) Z vl
: length vl = length Z
   defined_on (lv \ of_list Z) E
   defined_on lv (E [Z <-- List.map Some vl]).
Proof.
  unfold defined_on; intros.
  decide (x of_list Z).
  - length_equify. clear H1.
    general induction H0; simpl in × |- ×.
    + exfalso. cset_tac.
    + lud; eauto.
      eapply IHlength_eq; eauto; cset_tac; intuition.
  - edestruct H1; eauto. cset_tac.
     x0. rewrite <- H3.
    eapply update_with_list_no_update; eauto.
Qed.

Instance defined_on_morph_incl X `{OrderedType X} Y
  : Proper (flip Subset ==> eq ==> impl) (@defined_on X _ Y).
Proof.
  unfold Proper, respectful, impl; intros; subst.
  eapply defined_on_incl; eauto.
Qed.

Instance defined_on_morph_equal X `{OrderedType X} Y
  : Proper (Equal ==> eq ==> iff) (@defined_on X _ Y).
Proof.
  unfold Proper, respectful, flip, impl; intros; subst.
  eapply eq_incl in H0; dcr; split; intros; eauto using defined_on_incl.
Qed.

Lemma defined_on_agree X `{OrderedType X} Y R D (f g:Xoption Y)
  : defined_on D f
     agree_on (option_eq R) D f g
     defined_on D g.
Proof.
  intros; hnf; intros.
  edestruct H0; eauto.
  exploit H1; eauto.
  rewrite H3 in H4. inv H4. eauto.
Qed.

Lemma defined_on_agree_eq X `{OrderedType X} Y D (f g:Xoption Y)
  : defined_on D f
     agree_on eq D f g
     defined_on D g.
Proof.
  intros; hnf; intros.
  edestruct H0; eauto.
  exploit H1; eauto.
  rewrite H3 in H4. inv H4. eauto.
Qed.

Lemma defined_on_union X `{OrderedType X} Y (f:X option Y) s t
  : defined_on s f
     defined_on t f
     defined_on (s t) f.
Proof.
  intros; hnf; intros. cset_tac.
Qed.

Inductive defined X : list (option X) Prop :=
| NilDefined : defined nil
| ConsDefined x xs: defined xs defined (Some x::xs).

Lemma defined_get X (L:list (option X)) n x
  : defined L
     get L n x
     y, x = Some y.
Proof.
  intros. general induction H0; invt defined; eauto.
Qed.

Lemma defined_on_update_list' X `{OrderedType X} Y (E:X option Y) L L' (Len:L=L') s
  : defined_on (s \ of_list L) E
     defined L'
     defined_on s (E [L <-- L']).
Proof.
  intros.
  hnf; intros. decide (x of_list L).
  - edestruct update_with_list_lookup_in_list; try eapply i; dcr; eauto.
    rewrite H6. exploit defined_get; eauto.
  - rewrite lookup_set_update_not_in_Z; eauto.
    eapply H0; cset_tac.
Qed.

Lemma get_defined X (L:list (option X))
  : ( n x, get L n x y, x = Some y)
     defined L.
Proof.
  intros. general induction L; eauto using defined, get.
  edestruct H; dcr; eauto using get. subst.
  eauto using defined, get.
Qed.

Lemma defined_on_defined X `{OrderedType X} Y (V:Xoption Y) L
      `{Proper _ (_eq ==> eq) V}
  : defined_on (of_list L) V
     defined (V L).
Proof.
  split; intros.
  - eapply get_defined; intros; inv_get.
    eapply get_in_of_list in H2. eauto.
  - hnf; intros.
    edestruct of_list_get_first; eauto; dcr.
    eapply defined_get; eauto.
    rewrite H4. eapply map_get_1; eauto.
Qed.

Lemma defined_on_comp X `{OrderedType X} Y (f:XX) D (V:X option Y)
      `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> eq) V}
  : defined_on (map f D) V defined_on D (f V).
Proof.
  split; intros; hnf; intros.
  - exploit H2; eauto with cset.
  - eapply map_iff in H3; dcr; eauto.
    setoid_rewrite H6; eauto.
Qed.

Lemma defined_on_update_list_disj X `{OrderedType X} Y lv (E: X option Y) (Z:list X) vl
: defined_on lv E
   disj (of_list Z) lv
   defined_on lv (E [Z <-- vl]).
Proof.
  unfold defined_on; intros.
  general induction Z; destruct vl; simpl in *; eauto.
  - lud.
    + exfalso. eapply H1; eauto. simpl. cset_tac.
    + eapply IHZ; eauto with cset.
Qed.