diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v index 64bc0951026d9be664270882b74237c13ddbc78a..437e4e937e3ffd4f0fd53628796b7836213e38b4 100644 --- a/tests/multiset_solver.v +++ b/tests/multiset_solver.v @@ -27,48 +27,45 @@ Section test. 2 < multiplicity x X → X ⊆ Y → 1 < multiplicity x Y. Proof. multiset_solver. Qed. Lemma test_multiplicity_2 x X : - 2 < multiplicity x X → {[ x ]} ⊎ {[ x ]} ⊎ {[ x ]} ⊆ X. + 2 < multiplicity x X → {[ x ;+ x ;+ x ]} ⊆ X. Proof. multiset_solver. Qed. Lemma test_multiplicity_3 x X : - multiplicity x X < 3 → {[ x ]} ⊎ {[ x ]} ⊎ {[ x ]} ⊈ X. + multiplicity x X < 3 → {[ x ;+ x ;+ x ]} ⊈ X. Proof. multiset_solver. Qed. Lemma test_elem_of_1 x X : x ∈ X ↔ {[x]} ⊎ ∅ ⊆ X. Proof. multiset_solver. Qed. Lemma test_elem_of_2 x X : x ∈ X ↔ {[x]} ∪ ∅ ⊆ X. Proof. multiset_solver. Qed. - Lemma test_elem_of_3 x y X : x ≠y → x ∈ X → y ∈ X → {[x]} ⊎ {[y]} ⊆ X. + Lemma test_elem_of_3 x y X : x ≠y → x ∈ X → y ∈ X → {[x ;+ y]} ⊆ X. Proof. multiset_solver. Qed. - Lemma test_elem_of_4 x y X Y : x ≠y → x ∈ X → y ∈ Y → {[x]} ⊎ {[y]} ⊆ X ∪ Y. + Lemma test_elem_of_4 x y X Y : x ≠y → x ∈ X → y ∈ Y → {[x ;+ y]} ⊆ X ∪ Y. Proof. multiset_solver. Qed. Lemma test_elem_of_5 x y X Y : x ≠y → x ∈ X → y ∈ Y → {[x]} ⊆ (X ∪ Y) ∖ {[ y ]}. Proof. multiset_solver. Qed. - Lemma test_elem_of_6 x y X : {[x]} ⊎ {[y]} ⊆ X → x ∈ X ∧ y ∈ X. + Lemma test_elem_of_6 x y X : {[x ;+ y]} ⊆ X → x ∈ X ∧ y ∈ X. Proof. multiset_solver. Qed. Lemma test_big_1 x1 x2 x3 x4 : - {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊆@{gmultiset A} - {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]}. + {[ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ]} ⊆@{gmultiset A} + {[ x1 ;+ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ]}. Proof. multiset_solver. Qed. Lemma test_big_2 x1 x2 x3 x4 X : 2 ≤ multiplicity x4 X → - {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊆@{gmultiset A} - {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ X. + {[ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ]} ⊆@{gmultiset A} + {[ x1 ;+ x1 ;+ x2 ;+ x3 ]} ⊎ X. Proof. multiset_solver. Qed. Lemma test_big_3 x1 x2 x3 x4 X : 4 ≤ multiplicity x4 X → - {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎ - {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} + {[ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ;+ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ]} ⊆@{gmultiset A} - {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ - {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ X. + {[ x1 ;+ x1 ;+ x2 ;+ x3 ;+ x1 ;+ x1 ;+ x2 ;+ x3 ]} ⊎ X. Proof. multiset_solver. Qed. Lemma test_big_4 x1 x2 x3 x4 x5 x6 x7 x8 x9 : - {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎ - {[ x5 ]} ⊎ {[ x6 ]} ⊎ {[ x7 ]} ⊎ {[ x8 ]} ⊎ {[ x8 ]} ⊎ {[ x9 ]} + {[ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ;+ x5 ;+ x6 ;+ x7 ;+ x8 ;+ x8 ;+ x9 ]} ⊆@{gmultiset A} - {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎ - {[ x5 ]} ⊎ {[ x5 ]} ⊎ {[ x6 ]} ⊎ {[ x7 ]} ⊎ {[ x9 ]} ⊎ {[ x8 ]} ⊎ {[ x8 ]}. + {[ x1 ;+ x1 ;+ x2 ;+ x3 ;+ x4 ;+ x4 ;+ + x5 ;+ x5 ;+ x6 ;+ x7 ;+ x9 ;+ x8 ;+ x8 ]}. Proof. multiset_solver. Qed. Lemma test_firstorder_1 (P : A → Prop) x X : diff --git a/theories/base.v b/theories/base.v index 81f9078bf95e40c552b2bef27c67e974ea4cf775..8e2f922f819630feff7e4fc0d2bd60441e552b8f 100644 --- a/theories/base.v +++ b/theories/base.v @@ -866,6 +866,10 @@ Notation "{[ x ; y ; .. ; z ]}" := (union .. (union (singleton x) (singleton y)) .. (singleton z)) (at level 1) : stdpp_scope. +Notation "{[ x ;+ y ;+ .. ;+ z ]}" := + (disj_union .. (disj_union (singleton x) (singleton y)) .. (singleton z)) + (at level 1) : stdpp_scope. + Class SubsetEq A := subseteq: relation A. Global Hint Mode SubsetEq ! : typeclass_instances. Instance: Params (@subseteq) 2 := {}.