From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.

Utility: Std++ List Sets

Section sec_fst_defs.

Context `{EqDecision A}.

Definition set := list A.

Definition empty_set : set := [].

Fixpoint set_add (a : A) (x : set) : set :=
  match x with
  | [] => [a]
  | a1 :: x1 => if decide (a = a1) then a1 :: x1 else a1 :: set_add a x1
  end.

Fixpoint set_remove (a : A) (x : set) : set :=
  match x with
  | [] => empty_set
  | a1 :: x1 => if decide (a = a1) then x1 else a1 :: set_remove a x1
  end.

Fixpoint set_union (x y : set) : set :=
  match y with
  | [] => x
  | a1 :: y1 => set_add a1 (set_union x y1)
  end.

Fixpoint set_diff (x y : set) : set :=
  match x with
  | [] => []
  | a1 :: x1 => if decide (a1 ∈ y) then set_diff x1 y else set_add a1 (set_diff x1 y)
  end.

Lemma set_add_intro1 :
  forall (a b : A) (x : set), a ∈ x -> a ∈ set_add b x.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a ∈ x → a ∈ set_add b x
Proof.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a ∈ x → a ∈ set_add b x
  induction x; cbn.A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [] → a ∈ [b]
A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a ∈ x → a ∈ set_add b x
a ∈ a0 :: x
→ a
  ∈ (if decide (b = a0)
     then a0 :: x
     else a0 :: set_add b x)
  -A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [] → a ∈ [b] by inversion 1.
  -A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a ∈ x → a ∈ set_add b x
a ∈ a0 :: x
→ a
  ∈ (if decide (b = a0)
     then a0 :: x
     else a0 :: set_add b x) by destruct (decide (b = a0)); rewrite !elem_of_cons; itauto.
Qed.

Lemma set_add_intro2 :
  forall (a b : A) (x : set), a = b -> a ∈ set_add b x.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a = b → a ∈ set_add b x
Proof.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a = b → a ∈ set_add b x
  induction x; cbn.A: Type
EqDecision0: EqDecision A
a, b: A
a = b → a ∈ [b]
A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a = b → a ∈ set_add b x
a = b
→ a
  ∈ (if decide (b = a0)
     then a0 :: x
     else a0 :: set_add b x)
  -A: Type
EqDecision0: EqDecision A
a, b: A
a = b → a ∈ [b] by rewrite elem_of_cons; left.
  -A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a = b → a ∈ set_add b x
a = b
→ a
  ∈ (if decide (b = a0)
     then a0 :: x
     else a0 :: set_add b x) by intros ->; destruct (decide (b = a0)); rewrite !elem_of_cons; itauto.
Qed.

#[local] Hint Resolve set_add_intro1 set_add_intro2 : core.

Lemma set_add_intro :
  forall (a b : A) (x : set), a = b \/ a ∈ x -> a ∈ set_add b x.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a = b ∨ a ∈ x → a ∈ set_add b x
Proof.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a = b ∨ a ∈ x → a ∈ set_add b x
  by intros a b x [H1 | H2]; auto.
Qed.

Lemma set_add_elim :
  forall (a b : A) (x : set), a ∈ set_add b x -> a = b \/ a ∈ x.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a ∈ set_add b x → a = b ∨ a ∈ x
Proof.A: Type
EqDecision0: EqDecision A
∀ (a b : A) (x : set), a ∈ set_add b x → a = b ∨ a ∈ x
  induction x; cbn.A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [b] → a = b ∨ a ∈ []
A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a ∈ set_add b x → a = b ∨ a ∈ x
a
∈ (if decide (b = a0)
   then a0 :: x
   else a0 :: set_add b x) → 
a = b ∨ a ∈ a0 :: x
  -A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [b] → a = b ∨ a ∈ [] by rewrite elem_of_cons.
  -A: Type
EqDecision0: EqDecision A
a, b, a0: A
x: list A
IHx: a ∈ set_add b x → a = b ∨ a ∈ x
a
∈ (if decide (b = a0)
   then a0 :: x
   else a0 :: set_add b x) → a = b ∨ a ∈ a0 :: x by destruct (decide (b = a0)); rewrite !elem_of_cons; itauto.
Qed.

Lemma set_add_not_empty :
  forall (a : A) (x : set), set_add a x <> empty_set.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x : set), set_add a x ≠ empty_set
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x : set), set_add a x ≠ empty_set
  by induction x as [| a' x']; cbn; [| destruct (decide (a = a'))].
Qed.

Lemma set_add_iff a b l :
  a ∈ set_add b l <-> a = b \/ a ∈ l.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_add b l ↔ a = b ∨ a ∈ l
Proof.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_add b l ↔ a = b ∨ a ∈ l
  split.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_add b l → a = b ∨ a ∈ l
A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a = b ∨ a ∈ l → a ∈ set_add b l
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_add b l → a = b ∨ a ∈ l by apply set_add_elim.
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a = b ∨ a ∈ l → a ∈ set_add b l by apply set_add_intro.
Qed.

Lemma set_add_nodup a l :
  NoDup l -> NoDup (set_add a l).A: Type
EqDecision0: EqDecision A
a: A
l: list A
NoDup l → NoDup (set_add a l)
Proof.A: Type
EqDecision0: EqDecision A
a: A
l: list A
NoDup l → NoDup (set_add a l)
  induction 1 as [| x l H H' IH]; cbn.A: Type
EqDecision0: EqDecision A
a: A
NoDup [a]
A: Type
EqDecision0: EqDecision A
a, x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_add a l)
NoDup
  (if decide (a = x) then x :: l else x :: set_add a l)
  -A: Type
EqDecision0: EqDecision A
a: A
NoDup [a] by constructor; [inversion 1 | apply NoDup_nil].
  -A: Type
EqDecision0: EqDecision A
a, x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_add a l)
NoDup
  (if decide (a = x) then x :: l else x :: set_add a l) by destruct (decide (a = x)) as [<- | Hax]; constructor
    ; rewrite ?set_add_iff; itauto.
Qed.

Lemma set_remove_1 (a b : A) (l : set) :
  a ∈ set_remove b l -> a ∈ l.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_remove b l → a ∈ l
Proof.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ set_remove b l → a ∈ l
  induction l as [| x xs Hrec]; cbn; [done |].A: Type
EqDecision0: EqDecision A
a, b, x: A
xs: list A
Hrec: a ∈ set_remove b xs → a ∈ xs
a
∈ (if decide (b = x) then xs else x :: set_remove b xs)
→ a ∈ x :: xs
  by destruct (decide (b = x)); rewrite !elem_of_cons; itauto.
Qed.

Lemma set_remove_2 (a b : A) (l : set) :
  NoDup l -> a ∈ set_remove b l -> a <> b.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
NoDup l → a ∈ set_remove b l → a ≠ b
Proof.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
NoDup l → a ∈ set_remove b l → a ≠ b
  induction l as [| x l IH]; intro Hnd; cbn; [by inversion 1 |].A: Type
EqDecision0: EqDecision A
a, b, x: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
Hnd: NoDup (x :: l)
a
∈ (if decide (b = x) then l else x :: set_remove b l)
→ a ≠ b
  inversion_clear Hnd.A: Type
EqDecision0: EqDecision A
a, b, x: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
H: x ∉ l
H0: NoDup l
a
∈ (if decide (b = x) then l else x :: set_remove b l)
→ a ≠ b
  destruct (decide (b = x)) as [<- | Hbx].A: Type
EqDecision0: EqDecision A
a, b: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
H: b ∉ l
H0: NoDup l
a ∈ l → a ≠ b
A: Type
EqDecision0: EqDecision A
a, b, x: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
H: x ∉ l
H0: NoDup l
Hbx: b ≠ x
a ∈ x :: set_remove b l → a ≠ b
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
H: b ∉ l
H0: NoDup l
a ∈ l → a ≠ b by intros Ha ->.
  -A: Type
EqDecision0: EqDecision A
a, b, x: A
l: list A
IH: NoDup l → a ∈ set_remove b l → a ≠ b
H: x ∉ l
H0: NoDup l
Hbx: b ≠ x
a ∈ x :: set_remove b l → a ≠ b by rewrite elem_of_cons; firstorder subst.
Qed.

Lemma set_remove_3 (a b : A) (l : set) :
  a ∈ l -> a <> b -> a ∈ set_remove b l.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ l → a ≠ b → a ∈ set_remove b l
Proof.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
a ∈ l → a ≠ b → a ∈ set_remove b l
  induction l as [| x xs Hrec]; cbn.A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [] → a ≠ b → a ∈ empty_set
A: Type
EqDecision0: EqDecision A
a, b, x: A
xs: list A
Hrec: a ∈ xs → a ≠ b → a ∈ set_remove b xs
a ∈ x :: xs
→ a ≠ b
  → a
    ∈ (if decide (b = x)
       then xs
       else x :: set_remove b xs)
  -A: Type
EqDecision0: EqDecision A
a, b: A
a ∈ [] → a ≠ b → a ∈ empty_set by inversion 1.
  -A: Type
EqDecision0: EqDecision A
a, b, x: A
xs: list A
Hrec: a ∈ xs → a ≠ b → a ∈ set_remove b xs
a ∈ x :: xs
→ a ≠ b
  → a
    ∈ (if decide (b = x)
       then xs
       else x :: set_remove b xs) by destruct (decide (b = x)) as [<- | Hbx]; rewrite !elem_of_cons; itauto.
Qed.

Lemma set_remove_iff (a b : A) (l : set) :
  NoDup l -> a ∈ set_remove b l <-> a ∈ l /\ a <> b.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
NoDup l → a ∈ set_remove b l ↔ a ∈ l ∧ a ≠ b
Proof.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
NoDup l → a ∈ set_remove b l ↔ a ∈ l ∧ a ≠ b
  repeat split.A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
H0: a ∈ set_remove b l
a ∈ l
A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
H0: a ∈ set_remove b l
a ≠ b
A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
a ∈ l ∧ a ≠ b → a ∈ set_remove b l
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
H0: a ∈ set_remove b l
a ∈ l by eapply set_remove_1.
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
H0: a ∈ set_remove b l
a ≠ b by eapply set_remove_2.
  -A: Type
EqDecision0: EqDecision A
a, b: A
l: set
H: NoDup l
a ∈ l ∧ a ≠ b → a ∈ set_remove b l by destruct 1; apply set_remove_3.
Qed.

Lemma set_remove_nodup a l
  : NoDup l -> NoDup (set_remove a l).A: Type
EqDecision0: EqDecision A
a: A
l: list A
NoDup l → NoDup (set_remove a l)
Proof.A: Type
EqDecision0: EqDecision A
a: A
l: list A
NoDup l → NoDup (set_remove a l)
  induction 1 as [| x l H H' IH]; cbn; [by constructor |].A: Type
EqDecision0: EqDecision A
a, x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_remove a l)
NoDup
  (if decide (a = x) then l else x :: set_remove a l)
  destruct (decide (a = x)) as [<- | Hax]; [done |].A: Type
EqDecision0: EqDecision A
a, x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_remove a l)
Hax: a ≠ x
NoDup (x :: set_remove a l)
  constructor; [| done].A: Type
EqDecision0: EqDecision A
a, x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_remove a l)
Hax: a ≠ x
x ∉ set_remove a l
  by rewrite set_remove_iff; itauto.
Qed.

Lemma set_union_intro :
  forall (a : A) (x y : set),
    a ∈ x \/ a ∈ y -> a ∈ set_union x y.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ x ∨ a ∈ y → a ∈ set_union x y
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ x ∨ a ∈ y → a ∈ set_union x y
  induction y; cbn.A: Type
EqDecision0: EqDecision A
a: A
x: set
a ∈ x ∨ a ∈ [] → a ∈ x
A: Type
EqDecision0: EqDecision A
a: A
x: set
a0: A
y: list A
IHy: a ∈ x ∨ a ∈ y → a ∈ set_union x y
a ∈ x ∨ a ∈ a0 :: y → a ∈ set_add a0 (set_union x y)
  -A: Type
EqDecision0: EqDecision A
a: A
x: set
a ∈ x ∨ a ∈ [] → a ∈ x by rewrite elem_of_nil; itauto.
  -A: Type
EqDecision0: EqDecision A
a: A
x: set
a0: A
y: list A
IHy: a ∈ x ∨ a ∈ y → a ∈ set_union x y
a ∈ x ∨ a ∈ a0 :: y → a ∈ set_add a0 (set_union x y) by rewrite elem_of_cons, set_add_iff; itauto.
Qed.

Lemma set_union_elim :
  forall (a : A) (x y : set),
    a ∈ set_union x y -> a ∈ x \/ a ∈ y.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ set_union x y → a ∈ x ∨ a ∈ y
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ set_union x y → a ∈ x ∨ a ∈ y
  by induction y; cbn; rewrite ?elem_of_cons, ?set_add_iff; itauto.
Qed.

Lemma set_union_iff a l l' :
  a ∈ set_union l l' <-> a ∈ l \/ a ∈ l'.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_union l l' ↔ a ∈ l ∨ a ∈ l'
Proof.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_union l l' ↔ a ∈ l ∨ a ∈ l'
  split.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_union l l' → a ∈ l ∨ a ∈ l'
A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ l ∨ a ∈ l' → a ∈ set_union l l'
  -A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_union l l' → a ∈ l ∨ a ∈ l' by apply set_union_elim.
  -A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ l ∨ a ∈ l' → a ∈ set_union l l' by apply set_union_intro.
Qed.

Lemma set_union_nodup l l' :
  NoDup l -> NoDup l' -> NoDup (set_union l l').A: Type
EqDecision0: EqDecision A
l, l': list A
NoDup l → NoDup l' → NoDup (set_union l l')
Proof.A: Type
EqDecision0: EqDecision A
l, l': list A
NoDup l → NoDup l' → NoDup (set_union l l')
  by induction 2 as [| x' l' ? ? IH]; cbn; [| apply set_add_nodup].
Qed.

Lemma set_diff_intro :
  forall (a : A) (x y : set),
    a ∈ x -> a ∉ y -> a ∈ set_diff x y.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ x → a ∉ y → a ∈ set_diff x y
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set),
  a ∈ x → a ∉ y → a ∈ set_diff x y
  induction x; cbn; [by inversion 1 |].A: Type
EqDecision0: EqDecision A
a, a0: A
x: list A
IHx: ∀ y : set, a ∈ x → a ∉ y → a ∈ set_diff x y
∀ y : set,
  a ∈ a0 :: x
  → a ∉ y
    → a
      ∈ (if decide (a0 ∈ y)
         then set_diff x y
         else set_add a0 (set_diff x y))
  by intros y; destruct (decide (a0 ∈ y));
    rewrite elem_of_cons, ?set_add_iff; firstorder congruence.
Qed.

Lemma set_diff_elim1 :
  forall (a : A) (x y : set),
    a ∈ set_diff x y -> a ∈ x.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set), a ∈ set_diff x y → a ∈ x
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set), a ∈ set_diff x y → a ∈ x
  induction x; cbn; [done |]; intros y.A: Type
EqDecision0: EqDecision A
a, a0: A
x: list A
IHx: ∀ y : set, a ∈ set_diff x y → a ∈ x
y: set
a
∈ (if decide (a0 ∈ y)
   then set_diff x y
   else set_add a0 (set_diff x y)) → a ∈ a0 :: x
  by destruct (decide (a0 ∈ y)); rewrite elem_of_cons, ?set_add_iff; firstorder.
Qed.

Lemma set_diff_elim2 :
  forall (a : A) (x y : set), a ∈ set_diff x y -> a ∉ y.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set), a ∈ set_diff x y → a ∉ y
Proof.A: Type
EqDecision0: EqDecision A
∀ (a : A) (x y : set), a ∈ set_diff x y → a ∉ y
  induction x; cbn; [by inversion 1 |].A: Type
EqDecision0: EqDecision A
a, a0: A
x: list A
IHx: ∀ y : set, a ∈ set_diff x y → a ∉ y
∀ y : set,
  a
  ∈ (if decide (a0 ∈ y)
     then set_diff x y
     else set_add a0 (set_diff x y)) → a ∉ y
  by intros y; destruct (decide (a0 ∈ y)); rewrite ?set_add_iff; firstorder congruence.
Qed.

Lemma set_diff_iff a l l' :
  a ∈ set_diff l l' <-> a ∈ l /\ a ∉ l'.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_diff l l' ↔ a ∈ l ∧ a ∉ l'
Proof.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_diff l l' ↔ a ∈ l ∧ a ∉ l'
  split.A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_diff l l' → a ∈ l ∧ a ∉ l'
A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ l ∧ a ∉ l' → a ∈ set_diff l l'
  -A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ set_diff l l' → a ∈ l ∧ a ∉ l' by eauto using set_diff_elim1, set_diff_elim2.
  -A: Type
EqDecision0: EqDecision A
a: A
l, l': set
a ∈ l ∧ a ∉ l' → a ∈ set_diff l l' by destruct 1; apply set_diff_intro.
Qed.

Lemma set_diff_nodup l l' :
  NoDup l -> NoDup (set_diff l l').A: Type
EqDecision0: EqDecision A
l: list A
l': set
NoDup l → NoDup (set_diff l l')
Proof.A: Type
EqDecision0: EqDecision A
l: list A
l': set
NoDup l → NoDup (set_diff l l')
  induction 1 as [| x l H H' IH]; cbn.A: Type
EqDecision0: EqDecision A
l': set
NoDup []
A: Type
EqDecision0: EqDecision A
l': set
x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_diff l l')
NoDup
  (if decide (x ∈ l')
   then set_diff l l'
   else set_add x (set_diff l l'))
  -A: Type
EqDecision0: EqDecision A
l': set
NoDup [] by constructor.
  -A: Type
EqDecision0: EqDecision A
l': set
x: A
l: list A
H: x ∉ l
H': NoDup l
IH: NoDup (set_diff l l')
NoDup
  (if decide (x ∈ l')
   then set_diff l l'
   else set_add x (set_diff l l')) by case_decide; [| apply set_add_nodup].
Qed.

End sec_fst_defs.

Arguments set : clear implicits.

Section sec_other_defs.

Definition set_prod : forall {A B : Type}, set A -> set B -> set (A * B) :=
  list_prod.

Definition set_fold_right {A B : Type} (f : A -> B -> B) (x : set A) (b : B) : B :=
  fold_right f b x.

Definition set_map {A B : Type} `{EqDecision B} (f : A -> B) (x : set A) : set B :=
  set_fold_right (fun a => set_add (f a)) x empty_set.

End sec_other_defs.