Set Implicit Arguments.

From Coq Require Import List Arith Lia.

From hydras Require Import more_list list_permut.

Module Type S.

Declare Module DS : decidable_set.S.

Definition elt := DS.A.
Definition eq_elt_dec := DS.eq_A_dec.

Fixpoint without_red (l : list elt) {struct l} : Prop :=
  match l with
  | nil ⇒ True
  | e :: le ⇒ if (In_dec eq_elt_dec e le) then False else without_red le
  end.

Record t : Set :=
  mk_set
  {
     support : list elt;
     is_a_set : without_red support
  }.

Definition cardinal s := List.length s.(support).

Definition subset s1 s2 : Prop :=
  ∀ e, In e s1.(support) → In e s2.(support).

Axiom cardinal_subset :
  ∀ s1 s2, subset s1 s2 → cardinal s1 ≤ cardinal s2.

End S.

Module Make (DS1 : decidable_set.S) <: S with Module DS:= DS1.

Module DS := DS1.
Import DS1.
Module LP := list_permut.Make (DS1).

Definition elt := DS.A.
Definition eq_elt_dec : ∀ t1 t2 : elt, {t1 = t2} + {t1 ≠ t2} := DS.eq_A_dec.

Fixpoint without_red (l : list elt) {struct l} : Prop :=
  match l with
  | nil ⇒ True
  | e :: le ⇒ if (In_dec eq_elt_dec e le) then False else without_red le
  end.

Record t : Set :=
  mk_set
  {
     support : list elt;
     is_a_set : without_red support
  }.

Definition mem e s := In e s.(support).

Lemma mem_dec : ∀ e s, {mem e s}+{¬mem e s}.

Lemma add_prf :
  ∀ e l, without_red l → ¬In e l → without_red (e :: l).

Definition add e s :=
  match In_dec eq_elt_dec e s.(support) with
  | left _ ⇒ s
  | right R ⇒ mk_set (e :: s.(support)) (add_prf e s.(support) s.(is_a_set) R)
  end.

Lemma add_1 : ∀ e s, mem e (add e s).

Lemma add_2 : ∀ e e' s, mem e s → mem e (add e' s).

Lemma add_12 : ∀ e e' s, mem e (add e' s) → e = e' ∨ mem e s.

Fixpoint filter_aux (P : elt → Prop) (P_dec : ∀ e, {P e}+{¬ P e})
   (l : list elt) {struct l} : list elt :=
  match l with
  | nil ⇒ nil
  | e :: le ⇒
           if (P_dec e)
           then e :: (filter_aux P P_dec le)
           else filter_aux P P_dec le
   end.

Lemma included_filter_aux :
∀ P P_dec e l, In e (filter_aux P P_dec l) → In e l.

Lemma without_red_filter_aux :
  ∀ P P_dec l, without_red l → without_red (filter_aux P P_dec l).

Definition filter P P_dec s :=
   mk_set (filter_aux P P_dec s.(support))
               (without_red_filter_aux P P_dec _ s.(is_a_set)).

Lemma filter_1_list :
  ∀ (P : elt → Prop) P_dec l e, In e l → P e → In e (filter_aux P P_dec l).

Lemma filter_1 :
  ∀ (P : elt → Prop) P_dec s e, mem e s → P e → mem e (filter P P_dec s).

Lemma filter_2_list :
 ∀ (P : elt → Prop) P_dec l e, In e (filter_aux P P_dec l) →
                In e l ∧ P e.

Lemma filter_2 :
 ∀ (P : elt → Prop) P_dec s e, mem e (filter P P_dec s) →
                mem e s ∧ P e.

Fixpoint remove_red (l : list elt) : list elt :=
  match l with
  | nil ⇒ nil
  | e :: le ⇒
           if (In_dec eq_elt_dec e le)
           then remove_red le
           else e :: (remove_red le)
   end.

Lemma included_remove_red :
∀ e l, In e (remove_red l) → In e l.

Lemma remove_red_included : ∀ e l, In e l → In e (remove_red l).

Lemma without_red_remove_red : ∀ l, without_red (remove_red l).

Lemma without_red_remove :
  ∀ e l1 l2, without_red (l1 ++ e :: l2) → without_red (l1 ++ l2).

Lemma without_red_add :
  ∀ e l1 l2, without_red (l1 ++ l2) → ¬In e (l1 ++ l2) →
  without_red (l1 ++ e :: l2).

Lemma without_red_nil : without_red nil.

Definition empty : t :=
  mk_set nil without_red_nil.

Lemma without_red_singleton : ∀ e : elt, without_red (e :: nil).

Definition singleton (e : elt) : t :=
  mk_set (e :: nil) (without_red_singleton e).

Definition make_set (l : list elt) : t :=
  mk_set (remove_red l) (without_red_remove_red l).

Fixpoint add_without_red (acc l : list elt) {struct l} : list elt :=
  match l with
  | nil ⇒ acc
  | e :: le ⇒
     if (In_dec eq_elt_dec e acc)
     then add_without_red acc le
     else add_without_red (e :: acc) le
  end.

Lemma without_red_add_without_red :
  ∀ l1 l2, without_red l1 → without_red (add_without_red l1 l2).

Definition union s1 s2 :=
  mk_set (add_without_red s1.(support) s2.(support))
               (without_red_add_without_red s1.(support) s2.(support) s1.(is_a_set)).

Lemma union_1_aux :
∀ (l1 l2 : list elt) (e : elt), In e l1 → In e (add_without_red l1 l2).

Lemma union_1 : ∀ s1 s2 e, mem e s1 → mem e (union s1 s2).

Lemma union_2_aux :
∀ (l1 l2 : list elt) (e : elt), In e l2 → In e (add_without_red l1 l2).

Lemma union_2 : ∀ s1 s2 e, mem e s2 → mem e (union s1 s2).

Lemma union_12_aux :
∀ (l1 l2 : list elt) (e : elt), In e (add_without_red l1 l2) → In e l1 ∨ In e l2.

Lemma union_12 :
  ∀ s1 s2 e, mem e (union s1 s2) → mem e s1 ∨ mem e s2.

Fixpoint remove_not_common (acc l1 l2 : list elt) {struct l2} : list elt :=
  match l2 with
  | nil ⇒ acc
  | e :: l ⇒
      if In_dec eq_elt_dec e l1
      then remove_not_common (e :: acc) l1 l
      else remove_not_common acc l1 l
  end.

Lemma without_red_remove_not_common_aux :
  ∀ acc l1 l2, (∀ e, In e acc ∧ In e l2 → False) →
                           without_red acc → without_red l1 → without_red l2 →
                           without_red (remove_not_common acc l1 l2).

Lemma without_red_remove_not_common :
  ∀ l1 l2, without_red l1 → without_red l2 →
                    without_red (remove_not_common nil l1 l2).

Definition inter s1 s2 :=
  mk_set (remove_not_common nil s1.(support) s2.(support))
               (without_red_remove_not_common _ _ s1.(is_a_set) s2.(is_a_set)).

Lemma inter_1_aux :
  ∀ acc l1 l2 e, In e (remove_not_common acc l1 l2) → In e acc ∨ In e l1.

Lemma inter_1 : ∀ s1 s2 e, mem e (inter s1 s2) → mem e s1.

Lemma inter_2_aux :
  ∀ acc l1 l2 e, In e (remove_not_common acc l1 l2) → In e acc ∨ In e l2.

Lemma inter_2 : ∀ s1 s2 e, mem e (inter s1 s2) → mem e s2.

Lemma inter_12_aux :
  ∀ acc l1 l2 e, In e l1 → In e l2 → In e (remove_not_common acc l1 l2).

Lemma inter_12 :
  ∀ s1 s2 e, mem e s1 → mem e s2 → mem e (inter s1 s2).

Definition subset s1 s2 : Prop :=
  ∀ e, mem e s1 → mem e s2.

Lemma subset_dec : ∀ s1 s2, {subset s1 s2} + {¬ subset s1 s2}.

Lemma subset_union_1 :
  ∀ s1 s2, subset s1 (union s1 s2).

Lemma subset_union_2 :
  ∀ s1 s2, subset s2 (union s1 s2).

Lemma subset_inter_1 :
  ∀ s1 s2, subset (inter s1 s2) s1.

Lemma subset_inter_2 :
  ∀ s1 s2, subset (inter s1 s2) s2.

Definition eq_set s1 s2 :=
  ∀ e, mem e s1 ↔ mem e s2.

Lemma eq_set_dec : ∀ s1 s2, {eq_set s1 s2} + {¬eq_set s1 s2}.

Lemma eq_set_refl : ∀ s, eq_set s s.

Lemma eq_set_sym :
  ∀ s1 s2, eq_set s1 s2 → eq_set s2 s1.

Lemma eq_set_trans :
  ∀ s1 s2 s3, eq_set s1 s2 → eq_set s2 s3 → eq_set s1 s3.

Lemma add_comm :
  ∀ e1 e2 s, eq_set (add e1 (add e2 s)) (add e2 (add e1 s)).

Lemma union_empty_1 :
  ∀ s, eq_set s (union empty s).

Lemma union_empty_2 :
  ∀ s, eq_set s (union s empty).

Lemma union_comm :
  ∀ s1 s2, eq_set (union s1 s2) (union s2 s1).

Lemma union_assoc :
  ∀ s1 s2 s3, eq_set (union s1 (union s2 s3)) (union (union s1 s2) s3).

Lemma filter_union :
  ∀ P P_dec s1 s2,
  eq_set (filter P P_dec (union s1 s2)) (union (filter P P_dec s1) (filter P P_dec s2)).

Lemma subset_filter :
  ∀ (P1 P2 : elt → Prop) P1_dec P2_dec s1 s2, subset s1 s2 →
  (∀ e, P1 e → P2 e) → subset (filter P1 P1_dec s1) (filter P2 P2_dec s2).

Lemma subset_compat_1 :
  ∀ s1 s1' s2, eq_set s1 s1' → subset s1 s2 → subset s1' s2.

Lemma subset_compat_2 :
  ∀ s1 s2 s2', eq_set s2 s2' → subset s1 s2 → subset s1 s2'.

Lemma subset_compat :
   ∀ s1 s1' s2 s2', eq_set s1 s1' → eq_set s2 s2' →
                                    subset s1 s2 → subset s1' s2'.

Lemma union_compat_subset_1 :
  ∀ s1 s2 s, subset s1 s2 → subset (union s1 s) (union s2 s).

Lemma union_compat_subset_2 :
  ∀ s1 s2 s, subset s1 s2 → subset (union s s1) (union s s2).

Lemma union_compat_eq_set :
  ∀ s1 s1' s2 s2', eq_set s1 s1' → eq_set s2 s2' →
    eq_set (union s1 s2) (union s1' s2').

Lemma subset_subset_union :
  ∀ s1 s2 s, subset s1 s → subset s2 s → subset (union s1 s2) s.

Definition cardinal s := List.length s.(support).

Lemma cardinal_subset :
  ∀ s1 s2, subset s1 s2 → cardinal s1 ≤ cardinal s2.

Lemma cardinal_union_1 :
  ∀ s1 s2, cardinal s1 ≤ cardinal (union s1 s2).

Lemma cardinal_union_2 :
  ∀ s1 s2, cardinal s2 ≤ cardinal (union s1 s2).

Lemma cardinal_union_inter_12 :
  ∀ s1 s2, cardinal (union s1 s2) + cardinal (inter s1 s2) = cardinal s1 + cardinal s2.

Lemma cardinal_union:
  ∀ s1 s2, cardinal (union s1 s2) = cardinal s1 + cardinal s2 -cardinal (inter s1 s2).

Lemma cardinal_eq_set : ∀ s1 s2, eq_set s1 s2 → cardinal s1 = cardinal s2.

Lemma subset_cardinal_not_eq_not_eq_set :
 ∀ s1 s2 e, subset s1 s2 → ¬mem e s1 → mem e s2 →
  cardinal s1 < cardinal s2.

Lemma eq_set_list_permut_support :
  ∀ s1 s2, eq_set s1 s2 →
                 LP.list_permut s1.(support) s2.(support).

Lemma without_red_permut :
 ∀ l1 l2, without_red l1 → LP.list_permut l1 l2 → without_red l2.

End Make.