Library ordset_pairs

Require Import ssrbool eqtype ssrfun ssreflect.
Require Import Arith_ext seq_ext.
Require Import order.

Section sequence_of_pairs.

Variable A B : eqType.


Lemma pair_proj : forall (a : A) (b : B) c d, ((a, b) == (c, d)) = (a == c) && (b == d).

Implicit Type k : seq_eqType (prod_eqType A B).

Lemma mem_unzip1 : forall k x y, (x, y) \in k -> x \in unzip1 k.

Lemma mem_unzip2 : forall k x y, (x, y) \in k -> y \in unzip2 k.

Lemma not_unzip1_not_mem : forall k x, ~ fst x \in unzip1 k -> ~ x \in k.

Lemma unzip1_filter : forall k p, unzip1 (filter (fun x => p (fst x)) k) = filter p (unzip1 k).

Lemma unzip1_filter' : forall k p, unzip1 (filter (fun x => ~~ p (fst x)) k) = filter (fun x => ~~ p x) (unzip1 k).

Lemma filter_in_cons : forall k hd tl, hd \notin unzip1 k ->
  filter (fun x => x.1 \in hd :: tl) k = filter (fun x => x.1 \in tl) k.

Lemma dis_seq_unzip1 : forall k1 k2, dis (unzip1 k1) (unzip1 k2) -> dis k1 k2.

Lemma filter_dis : forall k1 k2, dis (unzip1 k1) (unzip1 k2) -> filter (fun x => x.1 \in unzip1 k2) k1 = [::].

End sequence_of_pairs.

Module FinSetOfPairsForMap.

Section finset_map.

Variable A : eqType.
Variable ltA : A -> A -> bool.
Notation "x < y" := (ltA x y) : section_ordered_sequence.
Open Local Scope section_ordered_sequence.
Variable ltA_trans : forall n m p, m < n -> n < p -> m < p.
Variable ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Variable ltA_irr : forall a, a < a = false.
Variable B : eqType.

Fixpoint add_map (x : A) (y : B) (l : seq_eqType (prod_eqType A B)) {struct l} :=
  match l with
    | [::] => [:: (x, y)]
    | (h1, h2) :: t =>
      if x < h1 then (x, y) :: (h1, h2) :: t else
        if x == h1 then (h1, h2) :: t
          else (h1, h2) :: add_map x y t
  end.

Lemma mem_add_map : forall l x y, ~ x \in unzip1 l -> (x, y) \in add_map x y l.

Lemma mem_unzip1_add_map : forall k x a b, x \in unzip1 k -> x \in unzip1 (add_map a b k).

Lemma mem_unzip1_add_map' : forall k a b, a \in unzip1 (add_map a b k).

Lemma mem_add_app_inv : forall k x a b,
  x \in add_map a b k -> x = (a, b) \/ fst x \in unzip1 k.

Lemma mem_add_app_inv_unzip1 : forall k x a b, x \in unzip1 (add_map a b k) -> x = a \/ x \in unzip1 k.

Lemma not_mem_unzip1_add_map : forall k x a b, x <> a ->
  ~ x \in unzip1 k -> ~ a \in unzip1 k -> ~ x \in unzip1 (add_map a b k).

Lemma add_map_comm' : forall l n n' w w', n < n' ->
  add_map n w (add_map n' w' l) = add_map n' w' (add_map n w l).

Lemma add_map_comm : forall l n n' w w', n <> n' ->
  add_map n w (add_map n' w' l) = add_map n' w' (add_map n w l).

Lemma add_map_reg : forall (l1 l2 : seq_eqType (prod_eqType A B)) x y y',
  ~ x \in unzip1 l1 -> ~ x \in unzip1 l2 ->
  add_map x y l1 = add_map x y' l2 ->
  y = y' /\ l1 = l2.

Lemma ocamlfind_add_map : forall k n w, ~ n \in unzip1 k ->
  ocamlfind (fun x => n == x.1) (add_map n w k) = Some (n, w).

Lemma ocamlfind_add_map' : forall k n w n', n <> n' -> ~ n \in unzip1 k ->
  ocamlfind (fun x => n' == x.1) (add_map n w k) =
  ocamlfind (fun x => n' == x.1) k.

Require Import ordset.
Import OrderedSequence.

Lemma lb_dom_filter : forall (k : seq (A * B)) n p,
  lb ltA n (unzip1 k) -> lb ltA n (unzip1 (filter p k)).

Lemma ordered_unzip1_filter : forall (k : seq_eqType (prod_eqType A B)) p,
  ordered ltA (unzip1 k) -> ordered ltA (unzip1 (filter p k)).

Lemma map_filter_drop : forall k : seq (A * B), ordered ltA (unzip1 k) ->
  forall l1 l2, unzip1 k = l1 ++ l2 ->
    filter (fun x => x.1 \in l2) k = drop (size l1) k.

Lemma map_filter_take : forall (k : seq (A * B)), ordered ltA (unzip1 k) ->
  forall l1 l2, unzip1 k = l1 ++ l2 ->
    filter (fun x => x.1 \notin l2) k = take (size l1) k.

Lemma add_map_lb : forall l x y, lb ltA x (unzip1 l) -> add_map x y l = (x,y) :: l.

Lemma lb_unzip1_add_map : forall l h n w, lb ltA h (unzip1 l) -> h < n ->
  lb ltA h (unzip1 (add_map n w l)).

Lemma ordered_unzip1_add_map : forall l n w, ordered ltA (unzip1 l) ->
  ~ n \in unzip1 l -> ordered ltA (unzip1 (add_map n w l)).

Lemma in_inj : forall (l : seq_eqType (prod_eqType A B)) x1 x2 y1 y2,
  ordered ltA (unzip1 l) -> (x1, x2) \in l -> (y1, y2) \in l ->
  x1 = y1 -> x2 = y2.

End finset_map.

End FinSetOfPairsForMap.