sets.v

  Global Instance set_infinite_subseteq :
    Proper ((⊆) ==> impl) (@set_infinite A C _).
  Proof. intros X Y HX ?. eapply pred_infinite_impl; set_solver. Qed.
  Global Instance set_infinite_proper : Proper ((≡) ==> iff) (@set_infinite A C _).
  Proof. intros X Y HX; apply forall_proper. by setoid_rewrite HX. Qed.

  Lemma union_infinite_l X Y : set_infinite X → set_infinite (X ∪ Y).
  Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
  Lemma union_infinite_r X Y : set_infinite Y → set_infinite (X ∪ Y).
  Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
End set_finite_infinite.

Section more_finite.
  Context `{Set_ A C}.
  Implicit Types X Y : C.

  Lemma intersection_finite_l X Y : set_finite X → set_finite (X ∩ Y).
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
  Lemma intersection_finite_r X Y : set_finite Y → set_finite (X ∩ Y).
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
  Lemma difference_finite X Y : set_finite X → set_finite (X ∖ Y).
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_difference; auto. Qed.
  Lemma difference_finite_inv X Y `{∀ x, Decision (x ∈ Y)} :
    set_finite Y → set_finite (X ∖ Y) → set_finite X.
  Proof.
    intros [l ?] [k ?]; exists (l ++ k).
    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver.
  Qed.

  Lemma difference_infinite X Y :
    set_infinite X → set_finite Y → set_infinite (X ∖ Y).
  Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
End more_finite.

(** Sets of sequences of natural numbers *)
(* The set [seq_seq start len] of natural numbers contains the sequence
[start, start + 1, ..., start + (len-1)]. *)
Fixpoint set_seq `{Singleton nat C, Union C, Empty C} (start len : nat) : C :=
  match len with
  | O => ∅
  | S len' => {[ start ]} ∪ set_seq (S start) len'
  end.

Section set_seq.
  Context `{SemiSet nat C}.
  Implicit Types start len x : nat.

  Lemma elem_of_set_seq start len x :
    x ∈ set_seq (C:=C) start len ↔ start ≤ x < start + len.
  Proof.
    revert start. induction len as [|len IH]; intros start; simpl.
    - rewrite elem_of_empty. lia.
    - rewrite elem_of_union, elem_of_singleton, IH. lia.
  Qed.
  Global Instance set_unfold_seq start len :
    SetUnfoldElemOf x (set_seq (C:=C) start len) (start ≤ x < start + len).
  Proof. constructor; apply elem_of_set_seq. Qed.

  Lemma set_seq_plus_disjoint start len1 len2 :
    set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
  Proof. set_solver by lia. Qed.
  Lemma set_seq_plus start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
  Proof. set_solver by lia. Qed.
  Lemma set_seq_plus_L `{!LeibnizEquiv C} start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    = set_seq start len1 ∪ set_seq (start + len1) len2.
  Proof. unfold_leibniz. apply set_seq_plus. Qed.

  Lemma set_seq_S_start_disjoint start len :
    {[ start ]} ## set_seq (C:=C) (S start) len.
  Proof. set_solver by lia. Qed.
  Lemma set_seq_S_start start len :
    set_seq (C:=C) start (S len) ≡ {[ start ]} ∪ set_seq (S start) len.
  Proof. set_solver by lia. Qed.

  Lemma set_seq_S_end_disjoint start len :
    {[ start + len ]} ## set_seq (C:=C) start len.
  Proof. set_solver by lia. Qed.
  Lemma set_seq_S_end_union start len :
    set_seq start (S len) ≡@{C} {[ start + len ]} ∪ set_seq start len.
  Proof. set_solver by lia. Qed.
  Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len :
    set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
  Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.

  Lemma list_to_set_seq start len :
    list_to_set (seq start len) =@{C} set_seq start len.
  Proof. revert start; induction len; intros; f_equal/=; auto. Qed.

  Lemma set_seq_finite start len : set_finite (set_seq (C:=C) start len).
  Proof.
    exists (seq start len); intros x. rewrite <-list_to_set_seq. set_solver.
  Qed.
End set_seq.

(** Mimimal elements *)
Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
  ∀ y, y ∈ X → R y x → R x y.
Instance: Params (@minimal) 5 := {}.
Typeclasses Opaque minimal.

Section minimal.
  Context `{SemiSet A C} {R : relation A}.
  Implicit Types X Y : C.

  Global Instance minimal_proper x : Proper ((≡@{C}) ==> iff) (minimal R x).
  Proof. intros X X' y; unfold minimal; set_solver. Qed.

  Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
    minimal R x X → y ∈ X → R y x → x = y.
  Proof. intros Hmin ??. apply (anti_symm _); auto. Qed.
  Lemma minimal_anti_symm `{!AntiSymm (=) R} X x :
    minimal R x X ↔ ∀ y, y ∈ X → R y x → x = y.
  Proof. unfold minimal; naive_solver eauto using minimal_anti_symm_1. Qed.

  Lemma minimal_strict_1 `{!StrictOrder R} X x y :
    minimal R x X → y ∈ X → ¬R y x.
  Proof. intros Hmin ??. destruct (irreflexivity R x); trans y; auto. Qed.
  Lemma minimal_strict `{!StrictOrder R} X x :
    minimal R x X ↔ ∀ y, y ∈ X → ¬R y x.
  Proof. unfold minimal; split; [eauto using minimal_strict_1|naive_solver]. Qed.

  Lemma empty_minimal x : minimal R x (∅ : C).
  Proof. unfold minimal; set_solver. Qed.
  Lemma singleton_minimal x : minimal R x ({[ x ]} : C).
  Proof. unfold minimal; set_solver. Qed.
  Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x ({[ y ]} : C).
  Proof. unfold minimal; set_solver. Qed.
  Lemma union_minimal X Y x :
    minimal R x X → minimal R x Y → minimal R x (X ∪ Y).
  Proof. unfold minimal; set_solver. Qed.
  Lemma minimal_subseteq X Y x : minimal R x X → Y ⊆ X → minimal R x Y.
  Proof. unfold minimal; set_solver. Qed.

  Lemma minimal_weaken `{!Transitive R} X x x' :
    minimal R x X → R x' x → minimal R x' X.
  Proof.
    intros Hmin ? y ??. trans x; [done|]. by eapply (Hmin y), transitivity.
  Qed.
End minimal.