include "tutorial/chapter5.ma".
+include "basics/core_notation/singl_1.ma".
(*************************** Naive Set Theory *********************************)
B ≐ C → A ∪ B ≐ A ∪ C.
#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
+ A ≐ C → A - B ≐ C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
+ B ≐ C → A - B ≐ A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
+(* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop.
+ A ∪ ∅ ≐ A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+qed.
+
+lemma union_comm : ∀U.∀A,B:U →Prop.
+ A ∪ B ≐ B ∪ A.
+#U #A #B #a % * /2/ qed.
+
+lemma union_assoc: ∀U.∀A,B,C:U → Prop.
+ A ∪ B ∪ C ≐ A ∪ (B ∪ C).
+#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
+qed.
+
+(*distributivities *)
+
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
+qed.
+
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) - C ≐ (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
+qed.
+
(************************ Sets with decidable equality ************************)
(* We say that a property P:A → Prop over a datatype A is decidable when we have
notation "\b H" non associative with precedence 90
for @{(proj2 … (eqb_true ???) $H)}.
+lemma eqb_false: ∀S:DeqSet.∀a,b:S.
+ (eqb ? a b) = false ↔ a ≠ b.
+#S #a #b % #H
+ [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
+ |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
+ ]
+qed.
+
+notation "\Pf H" non associative with precedence 90
+ for @{(proj1 … (eqb_false ???) $H)}.
+
+notation "\bf H" non associative with precedence 90
+ for @{(proj2 … (eqb_false ???) $H)}.
+
(****************************** Unification hints *****************************)
(* Suppose now to write an expression of the following kind:
| cons a tl ⇒ (x == a) ∨ memb S x tl
].
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
+qed.
+
+lemma memb_cons: ∀S,a,b,l.
+ memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize //
+qed.
+
+lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+ [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
+qed.
+
let rec uniqueb (S:DeqSet) l on l : bool ≝
match l with
[ nil ⇒ true
#A #B #f #l elim l
[#b normalize #H destruct (H)
|#a #tl #Hind #b #H cases (orb_true_l … H)
- [#eqb @(ex_intro … a) <(\P eqb) % // normalize >(\b (refl ? a)) //
+ [#eqb @(ex_intro … a) <(\P eqb) % //
|#memb cases (Hind … memb) #a * #mema #eqb
@(ex_intro … a) /3/
]