phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/base.v *)
Instance id2_assoc {A} : Assoc (=) (λ _ x : A, x).
Proof. intros ???; reflexivity. Qed.
(* stdpp/base.v *)
Instance id1_idemp {A} : IdemP (=) (λ x _ : A, x).
Proof. intros ?; reflexivity. Qed.
(* stdpp/base.v *)
Instance id2_idemp {A} : IdemP (=) (λ _ x : A, x).
Proof. intros ?; reflexivity. Qed.
(* stdpp/base.v *)
(* ** Lists *)
Instance list_inhabited {A} : Inhabited (list A)
:= populate [].
(* stdpp/base.v *)
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C
:=
  fix go l1 l2 :=
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
(* stdpp/base.v *)
Notation zip
:= (zip_with pair).
(* stdpp/base.v *)
(* The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
(* stdpp/base.v *)
Notation "(&&)"
:= andb (only parsing).
(* stdpp/base.v *)
Notation "(||)"
:= orb (only parsing).
(* stdpp/base.v *)
Instance bool_inhabated : Inhabited bool
:= populate true.
(* stdpp/base.v *)
Definition bool_le (β1 β2 : bool) : Prop
:= negb β1 || β2.
(* stdpp/base.v *)
Instance : PartialOrder bool_le.
Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
(* stdpp/base.v *)
Lemma andb_True b1 b2 : b1 && b2 ↔ b1 ∧ b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
(* stdpp/base.v *)
Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
(* stdpp/base.v *)
Lemma negb_True b : negb b ↔ ¬b.
Proof. destruct b; simpl; tauto. Qed.
(* stdpp/base.v *)
Lemma Is_true_true (b : bool) : b ↔ b = true.
Proof. now destruct b. Qed.
(* stdpp/base.v *)
Lemma Is_true_true_1 (b : bool) : b → b = true.
Proof. apply Is_true_true. Qed.
(* stdpp/base.v *)
Lemma Is_true_true_2 (b : bool) : b = true → b.
Proof. apply Is_true_true. Qed.
(* stdpp/base.v *)
Lemma Is_true_false (b : bool) : ¬ b ↔ b = false.
Proof. now destruct b; simpl. Qed.
(* stdpp/base.v *)
Lemma Is_true_false_1 (b : bool) : ¬b → b = false.
Proof. apply Is_true_false. Qed.
(* stdpp/base.v *)
Lemma Is_true_false_2 (b : bool) : b = false → ¬b.
Proof. apply Is_true_false. Qed.
(* stdpp/base.v *)
(* ** Unit *)
Instance unit_equiv : Equiv unit
:= λ _ _, True.
(* stdpp/base.v *)
Instance unit_equivalence : Equivalence (≡@{unit}).
Proof. repeat split. Qed.
(* stdpp/base.v *)
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
(* stdpp/base.v *)
Instance unit_inhabited: Inhabited unit
:= populate ().
(* stdpp/base.v *)
(* ** Empty *)
Instance Empty_set_equiv : Equiv Empty_set
:= λ _ _, True.
(* stdpp/base.v *)
Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
Proof. repeat split. Qed.
(* stdpp/base.v *)
Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Proof. intros [] []; reflexivity. Qed.
(* stdpp/base.v *)
(* ** Products *)
Notation "( x ,.)"
:= (pair x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(., y )"
:= (λ x, (x,y)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "p .1"
:= (fst p).
(* stdpp/base.v *)
Notation "p .2"
:= (snd p).
(* stdpp/base.v *)
Instance : Params (@pair) 2
:= {}.
(* stdpp/base.v *)
Instance : Params (@fst) 2
:= {}.
(* stdpp/base.v *)
Instance : Params (@snd) 2
:= {}.
(* stdpp/base.v *)
Instance : Params (@curry) 3
:= {}.
(* stdpp/base.v *)
Instance : Params (@uncurry) 3
:= {}.
(* stdpp/base.v *)
Definition uncurry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D
:=
  let '(a,b,c) := p in f a b c.
(* stdpp/base.v *)
Instance : Params (@uncurry3) 4
:= {}.
(* stdpp/base.v *)
Definition uncurry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E
:=
  let '(a,b,c,d) := p in f a b c d.
(* stdpp/base.v *)
Instance : Params (@uncurry4) 5
:= {}.
(* stdpp/base.v *)
Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D
:=
  f (a, b, c).
(* stdpp/base.v *)
Instance : Params (@curry3) 4
:= {}.
(* stdpp/base.v *)
Definition curry4 {A B C D E} (f : A * B * C * D → E)
  (a : A) (b : B) (c : C) (d : D) : E
:= f (a, b, c, d).
(* stdpp/base.v *)
Instance : Params (@curry4) 5
:= {}.
(* stdpp/base.v *)
Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B'
:=
  (f (p.1), g (p.2)).
(* stdpp/base.v *)
Instance : Params (@prod_map) 4
:= {}.
(* stdpp/base.v *)
Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'')
    (p : A * B) (q : A' * B') : A'' * B''
:= (f (p.1) (q.1), g (p.2) (q.2)).
(* stdpp/base.v *)
Instance : Params (@prod_zip) 6
:= {}.
(* stdpp/base.v *)
Definition prod_swap {A B} (p : A * B) : B * A
:= (p.2, p.1).
(* stdpp/base.v *)
Instance : Params (@prod_swap) 2
:= {}.
(* stdpp/base.v *)
Instance prod_inhabited {A B} (iA : Inhabited A)
    (iB : Inhabited B) : Inhabited (A * B)
:=
  match iA, iB with populate x, populate y => populate (x,y) end.
(* stdpp/base.v *)
(* Note that we need eta for products for the [uncurry_curry] lemmas to hold
in non-applied form ([uncurry (curry f) = f]). *)
Lemma curry_uncurry {A B C} (f : A → B → C) : curry (uncurry f) = f.
Proof. reflexivity. Qed.
(* stdpp/base.v *)
Lemma uncurry_curry {A B C} (f : A * B → C) p : uncurry (curry f) p = f p.
Proof. destruct p; reflexivity. Qed.
(* stdpp/base.v *)
Lemma curry3_uncurry3 {A B C D} (f : A → B → C → D) : curry3 (uncurry3 f) = f.
Proof. reflexivity. Qed.
(* stdpp/base.v *)
Lemma uncurry3_curry3 {A B C D} (f : A * B * C → D) p :
  uncurry3 (curry3 f) p = f p.
Proof. destruct p as [[??] ?]; reflexivity. Qed.
(* stdpp/base.v *)
Lemma curry4_uncurry4 {A B C D E} (f : A → B → C → D → E) :
  curry4 (uncurry4 f) = f.
Proof. reflexivity. Qed.
(* stdpp/base.v *)
Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p :
  uncurry4 (curry4 f) p = f p.
Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed.
(* stdpp/base.v *)
(* [pair_eq] as a name is more consistent with our usual naming. *)
Lemma pair_eq {A B} (a1 a2 : A) (b1 b2 : B) :
  (a1, b1) = (a2, b2) ↔ a1 = a2 ∧ b1 = b2.
Proof. apply pair_equal_spec. Qed.
(* stdpp/base.v *)
Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
Proof. injection 1; auto. Qed.
(* stdpp/base.v *)
Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
  Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g).
Proof.
  intros ?? [??] [??] ?; simpl in *; f_equal;
    [apply (inj f)|apply (inj g)]; congruence.
Qed.
(* stdpp/base.v *)
Instance prod_swap_cancel {A B} :
  Cancel (=) (@prod_swap A B) (@prod_swap B A).
Proof. intros [??]; reflexivity. Qed.
(* stdpp/base.v *)
Instance prod_swap_inj {A B} : Inj (=) (=) (@prod_swap A B).
Proof. apply cancel_inj. Qed.
(* stdpp/base.v *)
Instance prod_swap_surj {A B} : Surj (=) (@prod_swap A B).
Proof. apply cancel_surj. Qed.
(* stdpp/base.v *)
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
  relation (A * B)
:= λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2).
(* stdpp/base.v *)
Instance prod_relation_refl :
    Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB).
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance prod_relation_sym :
    Symmetric RA → Symmetric RB → Symmetric (prod_relation RA RB).
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance prod_relation_trans :
    Transitive RA → Transitive RB → Transitive (prod_relation RA RB).
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance prod_relation_equiv :
    Equivalence RA → Equivalence RB → Equivalence (prod_relation RA RB).
Proof. split; apply _. Qed.
(* stdpp/base.v *)
Instance pair_proper' : Proper (RA ==> RB ==> prod_relation RA RB) pair.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair.
Proof. inversion_clear 1; eauto. Qed.
(* stdpp/base.v *)
Instance fst_proper' : Proper (prod_relation RA RB ==> RA) fst.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance prod_swap_proper' :
    Proper (prod_relation RA RB ==> prod_relation RB RA) prod_swap.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance curry_proper' `{RC : relation C} :
    Proper ((prod_relation RA RB ==> RC) ==> RA ==> RB ==> RC) curry.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance uncurry_proper' `{RC : relation C} :
    Proper ((RA ==> RB ==> RC) ==> prod_relation RA RB ==> RC) uncurry.
Proof. intros f1 f2 Hf [x1 y1] [x2 y2] []; apply Hf; assumption. Qed.
(* stdpp/base.v *)
Instance curry3_proper' `{RC : relation C, RD : relation D} :
    Proper ((prod_relation (prod_relation RA RB) RC ==> RD) ==>
            RA ==> RB ==> RC ==> RD) curry3.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance uncurry3_proper' `{RC : relation C, RD : relation D} :
    Proper ((RA ==> RB ==> RC ==> RD) ==>
            prod_relation (prod_relation RA RB) RC ==> RD) uncurry3.
Proof. intros f1 f2 Hf [[??] ?] [[??] ?] [[??] ?]; apply Hf; assumption. Qed.
(* stdpp/base.v *)
Instance curry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
    Proper ((prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) ==>
            RA ==> RB ==> RC ==> RD ==> RE) curry4.
Proof. firstorder eauto. Qed.
(* stdpp/base.v *)
Instance uncurry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
    Proper ((RA ==> RB ==> RC ==> RD ==> RE) ==>
            prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) uncurry4.
Proof.
    intros f1 f2 Hf [[[??] ?] ?] [[[??] ?] ?] [[[??] ?] ?]; apply Hf; assumption.
  Qed.
(* stdpp/base.v *)
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B)
:=
  prod_relation (≡) (≡).
(* stdpp/base.v *)
Instance prod_equivalence :
    Equivalence (≡@{A}) → Equivalence (≡@{B}) → Equivalence (≡@{A * B})
:= _.
(* stdpp/base.v *)
Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair
:= _.
(* stdpp/base.v *)
Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair
:= _.
(* stdpp/base.v *)
Instance fst_proper : Proper ((≡@{A*B}) ==> (≡)) fst
:= _.
(* stdpp/base.v *)
Instance snd_proper : Proper ((≡@{A*B}) ==> (≡)) snd
:= _.
(* stdpp/base.v *)
Instance prod_swap_proper :
    Proper ((≡@{A*B}) ==> (≡@{B*A})) prod_swap
:= _.
(* stdpp/base.v *)
Instance curry_proper `{Equiv C} :
    Proper (((≡@{A*B}) ==> (≡@{C})) ==> (≡) ==> (≡) ==> (≡)) curry
:= _.
(* stdpp/base.v *)
Instance uncurry_proper `{Equiv C} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{A*B}) ==> (≡@{C})) uncurry
:= _.
(* stdpp/base.v *)
Instance curry3_proper `{Equiv C, Equiv D} :
    Proper (((≡@{A*B*C}) ==> (≡@{D})) ==>
            (≡) ==> (≡) ==> (≡) ==> (≡)) curry3
:= _.
(* stdpp/base.v *)
Instance uncurry3_proper `{Equiv C, Equiv D} :
    Proper (((≡) ==> (≡) ==> (≡) ==> (≡)) ==>
            (≡@{A*B*C}) ==> (≡@{D})) uncurry3
:= _.
(* stdpp/base.v *)
Instance curry4_proper `{Equiv C, Equiv D, Equiv E} :
    Proper (((≡@{A*B*C*D}) ==> (≡@{E})) ==>
            (≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) curry4
:= _.
(* stdpp/base.v *)
Instance uncurry4_proper `{Equiv C, Equiv D, Equiv E} :
    Proper (((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) ==>
            (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4
:= _.
(* stdpp/base.v *)
Lemma pair_equiv (a1 a2 : A) (b1 b2 : B) :
    (a1, b1) ≡ (a2, b2) ↔ a1 ≡ a2 ∧ b1 ≡ b2.
Proof. reflexivity. Qed.
(* stdpp/base.v *)
Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} :
  LeibnizEquiv (A * B).
Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
(* stdpp/base.v *)
(* ** Sums *)
Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B'
:=
  match xy with inl x => inl (f x) | inr y => inr (g y) end.
(* stdpp/base.v *)
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B)
:=
  match iA with populate x => populate (inl x) end.
(* stdpp/base.v *)
Instance sum_inhabited_r {A B} (iB : Inhabited B) : Inhabited (A + B)
:=
  match iB with populate y => populate (inr y) end.
(* stdpp/base.v *)
Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
(* stdpp/base.v *)
Instance inr_inj {A B} : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
(* stdpp/base.v *)
Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
  Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g).
Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed.
(* stdpp/base.v *)
Inductive sum_relation {A B}
     (RA : relation A) (RB : relation B) : relation (A + B)
:=
  | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2)
  | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2).
(* stdpp/base.v *)
Instance sum_relation_refl :
    Reflexive RA → Reflexive RB → Reflexive (sum_relation RA RB).
Proof. intros ?? [?|?]; constructor; reflexivity. Qed.
(* stdpp/base.v *)
Instance sum_relation_sym :
    Symmetric RA → Symmetric RB → Symmetric (sum_relation RA RB).
Proof. destruct 3; constructor; eauto. Qed.
(* stdpp/base.v *)
Instance sum_relation_trans :
    Transitive RA → Transitive RB → Transitive (sum_relation RA RB).
Proof. destruct 3; inversion_clear 1; constructor; eauto. Qed.
(* stdpp/base.v *)
Instance sum_relation_equiv :
    Equivalence RA → Equivalence RB → Equivalence (sum_relation RA RB).
Proof. split; apply _. Qed.
(* stdpp/base.v *)
Instance inl_proper' : Proper (RA ==> sum_relation RA RB) inl.
Proof. constructor; auto. Qed.
(* stdpp/base.v *)
Instance inr_proper' : Proper (RB ==> sum_relation RA RB) inr.
Proof. constructor; auto. Qed.
(* stdpp/base.v *)
Instance inl_inj' : Inj RA (sum_relation RA RB) inl.
Proof. inversion_clear 1; auto. Qed.
(* stdpp/base.v *)
Instance inr_inj' : Inj RB (sum_relation RA RB) inr.
Proof. inversion_clear 1; auto. Qed.
(* stdpp/base.v *)
Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B)
:= sum_relation (≡) (≡).
(* stdpp/base.v *)
Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B)
:= _.
(* stdpp/base.v *)
Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B)
:= _.
(* stdpp/base.v *)
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B)
:= _.
(* stdpp/base.v *)
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B)
:= _.
(* stdpp/base.v *)
(* ** Option *)
Instance option_inhabited {A} : Inhabited (option A)
:= populate None.
(* stdpp/base.v *)
(* Not in [option.v] so that [done] and [naive_solver] in [tactics.v] can
provide special support for it. *)
Definition is_Some {A} (mx : option A)
:= ∃ x, mx = Some x.
(* stdpp/base.v *)
Instance : Params (@is_Some) 1
:= {}.
(* stdpp/base.v *)
Notation "x ↾ p"
:= (exist _ x p) (at level 20) : stdpp_scope.
(* stdpp/base.v *)
Notation "` x"
:= (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
(* stdpp/base.v *)
Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
  x↾Px = y↾Py → x = y.
Proof. injection 1; trivial. Qed.
(* stdpp/base.v *)
Definition sig_map (x : sig P) : sig Q
:= f (`x) ↾ Hf _ (proj2_sig x).
(* stdpp/base.v *)
Instance sig_map_inj:
    (∀ x, ProofIrrel (P x)) → Inj (=) (=) f → Inj (=) (=) sig_map.
Proof.
    intros ?? [x Hx] [y Hy]. injection 1. intros Hxy.
    apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
  Qed.
(* stdpp/base.v *)
Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P
:=
  let '(ex_intro _ x _) := p in x.
(* stdpp/base.v *)
Definition proj2_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : Q (proj1_ex p)
:=
  let '(ex_intro _ x H) := p in H.
(* stdpp/base.v *)
(* We define operational type classes for the traditional operations and
relations on sets: the empty set [∅], the union [(∪)],
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A
:= empty: A.
(* stdpp/base.v *)
Notation "∅"
:= empty (format "∅") : stdpp_scope.
(* stdpp/base.v *)
Instance empty_inhabited `(Empty A) : Inhabited A
:= populate ∅.
(* stdpp/base.v *)
Class Union A
:= union: A → A → A.
(* stdpp/base.v *)
Instance : Params (@union) 2
:= {}.
(* stdpp/base.v *)
Notation "(∪)"
:= union (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ∪.)"
:= (union x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∪ x )"
:= (λ y, union y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∪*)"
:= (zip_with (∪)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Definition union_list `{Empty A, Union A} : list A → A
:= fold_right (∪) ∅.
(* stdpp/base.v *)
Instance : Params (@union_list) 3
:= {}.
(* stdpp/base.v *)
Notation "⋃ l"
:= (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
(* stdpp/base.v *)
Class Intersection A
:= intersection: A → A → A.
(* stdpp/base.v *)
Instance : Params (@intersection) 2
:= {}.
(* stdpp/base.v *)
Notation "(∩)"
:= intersection (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ∩.)"
:= (intersection x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∩ x )"
:= (λ y, intersection y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Class Difference A
:= difference: A → A → A.
(* stdpp/base.v *)
Instance : Params (@difference) 2
:= {}.
(* stdpp/base.v *)
Notation "(∖)"
:= difference (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ∖.)"
:= (difference x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∖ x )"
:= (λ y, difference y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∖*)"
:= (zip_with (∖)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
(* The operation [cprod X Y] gives the Cartesian product of set-like structures
[X] and [Y], i.e., [cprod X Y := { (x,y) | x ∈ X, y ∈ Y }]. The implementation/
instance depends on the representation of the set. *)
Class CProd A B C
:= cprod : A → B → C.
(* stdpp/base.v *)
Instance : Params (@cprod) 4
:= {}.
(* stdpp/base.v *)
(* We do not have a notation for [cprod] (yet) since this operation seems
not commonly enough used. *)
Class Singleton A B
:= singleton: A → B.
(* stdpp/base.v *)
Instance : Params (@singleton) 3
:= {}.
(* stdpp/base.v *)
Notation "{[ x ]}"
:= (singleton x) (at level 0) : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ x ; y ; .. ; z ]}"
:=
  (union .. (union (singleton x) (singleton y)) .. (singleton z))
  (at level 0) : stdpp_scope.
(* stdpp/base.v *)
Class SubsetEq A
:= subseteq: relation A.
(* stdpp/base.v *)
Instance : Params (@subseteq) 2
:= {}.
(* stdpp/base.v *)
Notation "(⊆)"
:= subseteq (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ⊆.)"
:= (subseteq X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊆ X )"
:= (λ Y, Y ⊆ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊈ Y"
:= (¬X ⊆ Y) (at level 70) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊈)"
:= (λ X Y, X ⊈ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ⊈.)"
:= (λ Y, X ⊈ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊈ X )"
:= (λ Y, Y ⊈ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊆@{ A } )"
:= (@subseteq A _) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊆*)"
:= (Forall2 (⊆)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊂)"
:= (strict (⊆)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ⊂.)"
:= (strict (⊆) X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊂ X )"
:= (λ Y, Y ⊂ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊄ Y"
:= (¬X ⊂ Y) (at level 70) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊄)"
:= (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ⊄.)"
:= (λ Y, X ⊄ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊄ X )"
:= (λ Y, Y ⊄ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊂@{ A } )"
:= (strict (⊆@{A})) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊆ Y ⊆ Z"
:= (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊆ Y ⊂ Z"
:= (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊂ Y ⊆ Z"
:= (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ⊂ Y ⊂ Z"
:= (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
(* stdpp/base.v *)
(* We define type classes for multisets: disjoint union [⊎] and the multiset
singleton [{[+ _ +]}]. Multiset literals [{[+ x1; ..; xn +]}] are defined in
terms of iterated disjoint union [{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}], and are thus
different from set literals [{[ x1; ..; xn ]}], which use [∪].

Note that in principle we could reuse the set singleton [{[ _ ]}] for multisets,
and define [{[+ x1; ..; xn +]}] as [{[ x1 ]} ⊎ .. ⊎ {[ xn ]}]. However, this
would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
Class DisjUnion A
:= disj_union: A → A → A.
(* stdpp/base.v *)
Instance : Params (@disj_union) 2
:= {}.
(* stdpp/base.v *)
Notation "(⊎)"
:= disj_union (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ⊎.)"
:= (disj_union x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊎ x )"
:= (λ y, disj_union y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Definition disj_union_list `{Empty A, DisjUnion A} : list A → A
:= fold_right (⊎) ∅.
(* stdpp/base.v *)
Instance : Params (@disj_union_list) 3
:= {}.
(* stdpp/base.v *)
(* There is no "big" version of [⊎] in unicode, we thus use [⋃+]. *)
Notation "⋃+ l"
:= (disj_union_list l) (at level 20, format "⋃+  l") : stdpp_scope.
(* stdpp/base.v *)
Class SingletonMS A B
:= singletonMS: A → B.
(* stdpp/base.v *)
Instance : Params (@singletonMS) 3
:= {}.
(* stdpp/base.v *)
Notation "{[+ x +]}"
:= (singletonMS x)
  (at level 0, format "{[+  x  +]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[+ x ; y ; .. ; z +]}"
:=
  (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
  (at level 0, format "{[+  x ;  y ;  .. ;  z  +]}") : stdpp_scope.
(* stdpp/base.v *)
Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C
:=
  match mx with None => ∅ | Some x => {[ x ]} end.
(* stdpp/base.v *)
Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C
:=
  match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end.
(* stdpp/base.v *)
Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A) : C
:=
  match l with [] => ∅ | x :: l => {[+ x +]} ⊎ list_to_set_disj l end.
(* stdpp/base.v *)
Class ScalarMul N A
:= scalar_mul : N → A → A.
(* stdpp/base.v *)
(* The [N] arguments is typically [nat] or [Z], so we do not want to rewrite
in that. Hence, the value of [Params] is 3. *)
Instance : Params (@scalar_mul) 3
:= {}.
(* stdpp/base.v *)
Notation "(*:)"
:=  scalar_mul (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x *:.)"
:= (scalar_mul x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.*: x )"
:= (λ y, scalar_mul y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
(* The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from
the order [(⊆)]. *)
Class Lexico A
:= lexico: relation A.
(* stdpp/base.v *)
Class ElemOf A B
:= elem_of: A → B → Prop.
(* stdpp/base.v *)
Instance : Params (@elem_of) 3
:= {}.
(* stdpp/base.v *)
Notation "(∈)"
:= elem_of (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ∈.)"
:= (elem_of x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∈ X )"
:= (λ x, elem_of x X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "x ∉ X"
:= (¬x ∈ X) (at level 70) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∉)"
:= (λ x X, x ∉ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ∉.)"
:= (λ X, x ∉ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∉ X )"
:= (λ x, x ∉ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∈@{ B } )"
:= (@elem_of _ B _) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "x ∉@{ B } X"
:= (¬x ∈@{B} X) (at level 70, only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∉@{ B } )"
:= (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Class Disjoint A
:= disjoint : A → A → Prop.
(* stdpp/base.v *)
Instance : Params (@disjoint) 2
:= {}.
(* stdpp/base.v *)
Notation "(##)"
:= disjoint (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ##.)"
:= (disjoint X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.## X )"
:= (λ Y, Y ## X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(##@{ A } )"
:= (@disjoint A _) (only parsing) : stdpp_scope.