Module AssocList


Require Import
  Utf8 Coqlib Util Maps.

Set Implicit Arguments.

Section ASSOC.

Context (A B: Type)
        `{EqDec A}
        (a: A).

Fixpoint assoc (l: list (A * B)) : option B :=
  match l with
  | cons (a', b) l' =>
    if eq_dec a' a then Some b else assoc l'
  | nil => None
  end.

Definition assoc_prop l pre (b: B) post : Prop :=
  l = pre ++ (a, b) :: post
  ∀ b', ¬ In (a, b') pre.

Fixpoint assoc_dep (l : list (A * B)) :
  { res | assoc_prop l (fst (fst res)) (snd (fst res)) (snd res) } + { ∀ b, ¬ In (a, b) l}.
  refine(
  match l with
  | cons (a', b) l' =>
    match eq_dec a' a with
    | left EQ => inleft (exist _ (nil, b, l') _)
    | right NE => match assoc_dep l' with
                  | inleft (exist r R) =>
                    match r as r' return assoc_prop l' (fst (fst r')) (snd (fst r')) (snd r') → _ with
                    | (pre, b', post) => λ R', inleft (exist _ ((a', b) :: pre, b', post) _)
                    end R
                  | inright R => inright _
                  end
    end
  | nil => inright _
  end).
Proof.
  exact_ K, K).
  clear -EQ. abstract (split; [rewrite EQ; reflexivity | exact_ K, K)]).
  clear -NE R'. abstract (simpl in *; destruct R' as [R1 R2]; split;[simpl; congruence|
  (intros c [ K | K ];[eq_some_inv; intuition | exact (R2 _ K)])]).
  clear -NE R. abstract (intros c [K | K]; [eq_some_inv; intuition | exact (R _ K)]).
Defined.
Global Opaque assoc_dep.

Lemma assoc_in l :
  ∀ b, assoc l = Some bIn (a, b) l.
Proof.
  induction l as [|(a', b') l IH].
  exact_ H, None_not_Some H _).
  intros b. simpl.
  destruct eq_dec. intro. eq_some_inv. left. subst. reflexivity.
  intuition.
Qed.

Lemma assoc_Some l :
  ∀ b,
    assoc l = Some b
    ∃ pre post,
      l = pre ++ (a, b) :: post
      ∀ b', ¬ In (a, b') pre.
Proof.
  induction l as [|(a', b') l IH].
  exact_ H, None_not_Some H _).
  intros b. simpl.
  destruct eq_dec as [EQ|NE].
  intros EQ'.
  exists nil. exists l. simpl. eq_some_inv. intuition. subst. reflexivity.
  intros R. destruct (IH _ R) as (pre & post & X & Y).
  exists ((a', b') :: pre), post.
  split. simpl. subst. reflexivity.
  intros z [Q|Q]. apply pair_eq_inv in Q. intuition.
  intuition eauto.
Qed.

Lemma assoc_None l :
  assoc l = None
  ∀ b, ¬ In (a, b) l.
Proof.
  induction l as [|(a', b') l IH]. intuition.
  simpl. destruct eq_dec. split. intro; eq_some_inv.
  intros K. destruct (K b'). left. congruence.
  split.
  intros K b [X|X]. eq_some_inv. auto.
  exact (proj1 IH K b X).
  intros K. firstorder.
Qed.

Lemma In_norepet_assoc (b: B) l :
  list_norepet (map fst l) →
  In (a, b) lassoc l = Some b.
Proof.
  induction l as [|(a', b') l IH]. intros _ ().
  intros NR [IN|IN].
  eq_some_inv. simpl. subst. rewrite dec_eq_true. reflexivity.
  simpl. inv NR. rewrite dec_eq_false. apply IH; auto.
  intros ->. elim H2. rewrite in_map_iff. exists (a, b). intuition.
Qed.

Lemma assoc_app l m :
  assoc (l ++ m) = match assoc l with Some r => Some r | None => assoc m end.
Proof.
  induction l as [|(x,b) l IH]. reflexivity.
  simpl. destruct eq_dec; auto.
Qed.

Corollary assoc_iff l b :
  assoc l = Some b ↔ ∃ pre post, assoc_prop l pre b post.
Proof.
  split. apply assoc_Some.
  intros (pre & post & -> & K).
  rewrite assoc_app.
  generalize (assoc_in pre).
  destruct (assoc pre). intros X. elim (K _ (X _ eq_refl)).
  intros _. simpl. rewrite dec_eq_true. reflexivity.
Qed.

End ASSOC.

Lemma ptree_get_assoc {A: Type} (m: PTree.t A) :
  ∀ x, m ! x = assoc x (PTree.elements m).
Proof.
  intros x.
  generalize (PTree.elements_correct m x).
  generalize (PTree.elements_complete m x).
  generalize (PTree.elements_keys_norepet m).
  intros NR C I.
  destruct (m ! x). specialize (I _ eq_refl). symmetry. apply In_norepet_assoc; auto.
  generalize (assoc_in x (PTree.elements m)).
  destruct assoc; auto.
Qed.

Section NTH.

Context (A: Type).

Fixpoint nth (m: list A) (p: positive) : option A :=
  match m with
  | nil => None
  | x :: n => match p with xH => Some x | xI q => nth n (xO q) | xO q => nth n (Pos.pred_double q) end
  end.

Lemma nth_succ (m: list A) p :
  nth m (Pos.succ p) = match m with nil => None | _ :: m' => nth m' p end.
Proof.
  destruct p as [ p | p | ]; destruct m as [ | a m ]; simpl; auto.
  f_equal. apply Pos.pred_double_succ.
Qed.

Lemma nth_in p (m: list A) a :
  nth m p = Some aIn a m.
Proof.
  revert p.
  induction m as [ | b m IH ]. simpl; intros; eq_some_inv.
  intros [ f | f | ]; simpl;
  (intuition congruence) ||
  (intros H; specialize (IH _ H); auto).
Qed.

End NTH.

Section PLENGTH.

Local Open Scope positive_scope.

Context (A: Type).

Fixpoint plength_aux (m: list A) (acc: positive) : positive :=
  match m with nil => acc | _ :: m' => plength_aux m' (Pos.succ acc) end.

Definition plength (m: list A) : positive :=
  plength_aux m xH.

Lemma plength_nil : plength nil = xH.
Proof.
reflexivity. Qed.

Lemma plength_aux_add (m: list A) (x y: positive) :
  plength_aux m (x + y) = plength_aux m x + y.
Proof.
  revert x.
  induction m as [ | a m IH ]; intros x.
  reflexivity.
  now simpl; rewrite <- IH, Pos.add_succ_l.
Qed.

Lemma plength_length_aux (m: list A) acc :
   Pos.pred (acc + Pos.of_succ_nat (Datatypes.length m)) = plength_aux m acc.
Proof.
  revert acc.
  induction m as [ | a m IH ]; simpl; intros acc;
  try rewrite <- IH;
  rewrite Ppred_minus; zify; rewrite ! Pos2Z.inj_sub; Psatz.lia.
Qed.

Lemma plength_length (m: list A) :
   Pos.of_succ_nat (Datatypes.length m) = plength m.
Proof.
  unfold plength. rewrite <- plength_length_aux.
  now rewrite <- Pplus_one_succ_l, Pos.pred_succ.
Qed.

Definition plength_cons (a: A) (m: list A) :
  plength (a :: m) = Pos.succ (plength m).
Proof.
  unfold plength.
  now rewrite Pplus_one_succ_r, <- plength_aux_add, <- Pplus_one_succ_r.
Qed.

Definition plength_app (m n: list A) :
  plength (m ++ n) = Pos.pred (plength m + plength n)%positive.
Proof.
  revert n.
  induction m as [ | a m IH ].
  now intros n; rewrite <- Pplus_one_succ_l, Pos.pred_succ.
  intros n. simpl app. rewrite ! plength_cons.
  rewrite IH. rewrite ! Pplus_one_succ_l, ! Ppred_minus. zify.
  repeat (rewrite ? Pos2Z.inj_add; rewrite ? Pos2Z.inj_sub; Psatz.lia).
Qed.

Definition plength_snoc (a: A) (m: list A) :
  plength (m ++ a :: nil) = Pos.succ (plength m).
Proof.
  rewrite plength_app, plength_cons, Ppred_minus, ! Pplus_one_succ_l, plength_nil.
  zify. rewrite Pos2Z.inj_sub; Psatz.lia.
Qed.

Lemma rev_plength (m: list A) :
  plength (rev m) = plength m.
Proof.
  induction m as [ | a m IH ].
  reflexivity. now simpl; rewrite plength_cons, plength_snoc; f_equal.
Qed.

End PLENGTH.

Lemma map_plength {A B} (f: AB) (m: list A) :
  plength (map f m) = plength m.
Proof.
  induction m.
  now rewrite plength_nil.
  simpl. rewrite ! plength_cons. congruence.
Qed.