Merge pull request #206 from vlj/subset-lattice

Add a distrLattice canonical structure to set T.

CHANGELOG_UNRELEASED.md

@@ -11,6 +11,10 @@
     `setDUr`, `setDUl`, `setIDA`, `setDD`
   + definition `dep_arrow_choiceType`
   + lemma `bigcup_set0`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `subsetPset`, `properPset`
+  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType`
+  + lemma `not_exists2P`
+
 - in `normedtype.v`:
   + lemma `closed_ereal_le_ereal`
   + lemma `closed_ereal_ge_ereal`
@@ -54,13 +58,18 @@
   + lemma `oppe_continuous`
   + lemmas `setUCl`, `setDv`
   + lemmas `image_preimage_subset`, `image_subset`, `preimage_subset`
+  + definition `proper` and its notation `<`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `properEneq`
+  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`.
 
 ### Changed
 
 - in `classical_sets.v`:
   + the index in `bigcup_set1` generalized from `nat` to some `Type`
   + lemma `bigcapCU` generalized
   + lemmas `preimage_setU` and `preimage_setI` are about the `setU` and `setI` (instead of `bigcup` and `bigcap`)
+  + `eqEsubset` changed from an implication to an equality
 - lemma `asboolb` moved from `discrete.v` to `boolp.v`
 - lemma `exists2NP` moved from `discrete.v` to `boolp.v`
 - lemma `neg_or` moved from `discrete.v` to `boolp.v` and renamed to `not_orP`
@@ -74,6 +83,8 @@
   + the first argument of `real_of_er` is now maximal implicit
   + the first argument of `is_real` is now maximal implicit
   + generalization of `lee_sum`
+- in `boolp.v`:
+  + rename `exists2NP` to `forall2NP` and make it bidirectionnal
 
 ### Renamed
 

theories/altreals/discrete.v

@@ -151,7 +151,7 @@ Lemma finiteNP (E : pred T): (forall s : seq T, ~ {subset E <= s}) ->
 Proof.
 move=> finN; elim=> [|n [s] [<- uq_s sE]]; first by exists [::].
 have [x sxN xE]: exists2 x, x \notin s & x \in E.
-  apply: contra_notP (finN (filter (mem E) s)) => /exists2NP finE x Ex.
+  apply: contra_notP (finN (filter (mem E) s)) => /forall2NP finE x Ex.
   move/or_asboolP: (finE x).
   by rewrite !asbool_neg !asboolb negbK Ex mem_filter orbF [(mem E) x]Ex.
 exists (x :: s) => /=; rewrite sxN; split=> // y.

theories/boolp.v

@@ -278,6 +278,18 @@ move=> cb /asboolPn nb; apply/asboolPn.
 by apply: contra nb => /asboolP /cb /asboolP.
 Qed.
 
+(** subsumed by mathcomp 1.12, to be removed *)
+Lemma contra_notT (P: Prop) (b:bool) : (~~ b -> P) -> ~ P -> b.
+Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed.
+
+(** subsumed by mathcomp 1.12, to be removed *)
+Lemma contra_notN (P: Prop) (b:bool) : (b -> P) -> ~ P -> ~~ b.
+Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed.
+
+(** subsumed by mathcomp 1.12, to be removed *)
+Lemma contra_not_neq (T: eqType)  (P: Prop) (x y:T) : (x = y -> P) -> ~ P -> x != y.
+Proof. by move=> imp; apply: contra_notN => /eqP. Qed.
+
 Lemma contraPnot (Q P : Prop) : (Q -> ~ P) -> P -> ~ Q.
 Proof.
 move=> cb /asboolP hb; apply/asboolPn.
@@ -598,11 +610,18 @@ Proof. by rewrite forallNE. Qed.
 Lemma not_forallP T (P : T -> Prop) : (forall x, P x) <-> ~ exists x, ~ P x.
 Proof. by rewrite existsNE notK. Qed.
 
-Lemma exists2NP T (P Q : T -> Prop) :
-  ~ (exists2 x, P x & Q x) -> forall x, ~ P x \/ ~ Q x.
+Lemma not_exists2P T (P Q : T -> Prop) :
+  (exists2 x, P x & Q x) <-> ~ forall x, ~ P x \/ ~ Q x.
+Proof.
+split=> [[x Px Qx] /(_ x) [|]//|]; apply: contra_notP => PQ t.
+by rewrite -not_andP; apply: contra_not PQ => -[Pt Qt]; exists t.
+Qed.
+
+Lemma forall2NP T (P Q : T -> Prop) :
+  (forall x, ~ P x \/ ~ Q x) <-> ~ (exists2 x, P x & Q x).
 Proof.
-apply: contra_notP; case/asboolPn/existsp_asboolPn=> [x].
-by case/not_orP => /contrapT Px /contrapT Qx; exists x.
+split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
+by rewrite -not_andP => -[Pt Qt]; apply PQ; exists t.
 Qed.
 
 (* -------------------------------------------------------------------- *)

theories/classical_sets.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg matrix finmap.
+From mathcomp Require Import all_ssreflect ssralg matrix finmap order.
 Require Import boolp.
 
 (******************************************************************************)
@@ -144,6 +144,7 @@ Reserved Notation "\bigcap_ ( i : T ) F"
 Reserved Notation "\bigcap_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \bigcap_ i '/  '  F ']'").
+Reserved Notation "A `<` B" (at level 70, no associativity).
 Reserved Notation "A `<=` B" (at level 70, no associativity).
 Reserved Notation "A `<=>` B" (at level 70, no associativity).
 Reserved Notation "f @^-1` A" (at level 24).
@@ -243,15 +244,21 @@ Notation "\bigcap_ ( i : T ) F" :=
 Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.
 
 Definition subset {A} (X Y : set A) := forall a, X a -> Y a.
-
 Notation "A `<=` B" := (subset A B) : classical_set_scope.
+
+Definition proper {A} (X Y : set A) := X `<=` Y /\ ~ (Y `<=` X).
+Notation "A `<` B" := (proper A B) : classical_set_scope.
+
 Notation "A `<=>` B" := ((A `<=` B) /\ (B `<=` A)) : classical_set_scope.
 Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
 Notation "f @` A" := (image f A) : classical_set_scope.
 Notation "A !=set0" := (nonempty A) : classical_set_scope.
 
-Lemma eqEsubset T (F G : set T) : F `<=` G -> G `<=` F -> F = G.
-Proof. by move=> H K; rewrite funeqE=> s; rewrite propeqE; split=> [/H|/K]. Qed.
+Lemma eqEsubset T (F G : set T) : (F = G) = (F `<=` G /\ G `<=` F).
+Proof.
+rewrite propeqE; split => [->|[FG GF]]; [by split|].
+by rewrite predeqE => t; split=> [/FG|/GF].
+Qed.
 
 Lemma sub0set T (X : set T) : set0 `<=` X.
 Proof. by []. Qed.
@@ -289,12 +296,13 @@ Lemma setDv T (A : set T) : A `\` A = set0.
 Proof. by rewrite predeqE => t; split => // -[]. Qed.
 
 Lemma subset0 T (X : set T) : (X `<=` set0) = (X = set0).
-Proof. rewrite propeqE; split => [?|-> //]; exact/eqEsubset. Qed.
+Proof. by rewrite eqEsubset propeqE; split => [X0|[]//]; split. Qed.
 
 Lemma set0P T (X : set T) : (X != set0) <-> (X !=set0).
 Proof.
 split=> [/negP X_neq0|[t tX]]; last by apply/negP => /eqP X0; rewrite X0 in tX.
-by apply: contrapT => /asboolPn/forallp_asboolPn X0; apply/X_neq0/eqP/eqEsubset.
+apply: contrapT => /asboolPn/forallp_asboolPn X0; apply/X_neq0/eqP.
+by rewrite eqEsubset; split.
 Qed.
 
 Lemma imageP {A B} (f : A -> B) (X : set A) a : X a -> (f @` X) (f a).
@@ -307,25 +315,26 @@ by move=> f_inj; rewrite propeqE; split => [[b Xb /f_inj <-]|/(imageP f)//].
 Qed.
 Arguments image_inj {A B} [f X a].
 
-Lemma image_comp T U V (f : T -> U) (g : U -> V) A : g @` (f @` A) = (g \o f) @` A.
+Lemma image_comp T U V (f : T -> U) (g : U -> V) A :
+  g @` (f @` A) = (g \o f) @` A.
 Proof.
-apply eqEsubset => c.
+rewrite eqEsubset; split => x.
 - by case => b [] a Xa <- <-; apply/imageP.
 - by case => a Xa <-; apply/imageP/imageP.
 Qed.
 
 Lemma image_id T (A : set T) : id @` A = A.
-Proof. by apply eqEsubset => a; [case=> /= x Xx <-|exists a]. Qed.
+Proof. by rewrite eqEsubset; split => a; [case=> /= x Xx <-|exists a]. Qed.
 
 Lemma image_setU T U (f : T -> U) A B : f @` (A `|` B) = f @` A `|` f @` B.
 Proof.
-apply eqEsubset => b.
+rewrite eqEsubset; split => b.
 - by case=> a [] Ha <-; [left | right]; apply imageP.
 - by case=> -[] a Ha <-; apply imageP; [left | right].
 Qed.
 
 Lemma image_set0 T U (f : T -> U) : f @` set0 = set0.
-Proof. by apply eqEsubset => b // -[]. Qed.
+Proof. by rewrite eqEsubset; split => b // -[]. Qed.
 
 Lemma image_set0_set0 T U (A : set T) (f : T -> U) : f @` A = set0 -> A = set0.
 Proof.
@@ -334,12 +343,12 @@ by have : set0 (f t) by rewrite -fA0; exists t.
 Qed.
 
 Lemma image_set1 T U (f : T -> U) (t : T) : f @` [set t] = [set f t].
-Proof. by apply eqEsubset => b; [case=> a' -> <- | move->; apply imageP]. Qed.
+Proof. by rewrite eqEsubset; split => [b [a' -> <-] //|b ->]; exact/imageP. Qed.
 
 Lemma subset_set1 T (A : set T) a : A `<=` [set a] -> A = set0 \/ A = [set a].
 Proof.
 move=> Aa; have [|/set0P/negP/negPn/eqP->] := pselect (A !=set0); [|by left].
-by case=> t At; right; apply: eqEsubset => // ? ->; rewrite -(Aa _ At).
+by case=> t At; right; rewrite eqEsubset; split => // ? ->; rewrite -(Aa _ At).
 Qed.
 
 Lemma sub_image_setI {A B} (f : A -> B) (X Y : set A) :
@@ -465,7 +474,14 @@ rewrite propeqE; split=> [XDY0 a|sXY].
 by rewrite predeqE => ?; split=> // - [?]; apply; apply: sXY.
 Qed.
 
-Lemma nonsubset {A} (X Y:set A): ~ (X `<=` Y) -> X `&` ~` Y !=set0.
+Lemma properEneq {A} (X Y : set A) : (X `<` Y) = (X != Y /\ X `<=` Y).
+Proof.
+rewrite /proper andC propeqE; split => [[YX XY]|[/eqP]].
+by split => //; apply/negP; apply: contra_not YX => /eqP ->.
+by rewrite eqEsubset => XY YX; split => //; exact: contra_not XY.
+Qed.
+
+Lemma nonsubset {A} (X Y : set A) : ~ (X `<=` Y) -> X `&` ~` Y !=set0.
 Proof. by rewrite -setD_eq0 setDE -set0P => /eqP. Qed.
 
 Lemma setIC {A} (X Y : set A) : X `&` Y = Y `&` X.
@@ -603,9 +619,20 @@ by move=> [[Xt|Zt] [Yt|Zt']]; by [left|right].
 Qed.
 
 Lemma setUIr T : right_distributive (@setU T) (@setI T).
-move.
 Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUIl. Qed.
 
+Lemma setUK T (A B : set T) : (A `|` B) `&` A = A.
+Proof. by rewrite eqEsubset; split => [t []//|t ?]; split => //; left. Qed.
+
+Lemma setKU T (A B : set T) : A `&` (B `|` A) = A.
+Proof. by rewrite eqEsubset; split => [t []//|t ?]; split => //; right. Qed.
+
+Lemma setIK T (A B : set T) : (A `&` B) `|` A = A.
+Proof. by rewrite eqEsubset; split => [t [[]//|//]|t At]; right. Qed.
+
+Lemma setKI T (A B : set T) : A `|` (B `&` A) = A.
+Proof. by rewrite eqEsubset; split => [t [//|[]//]|t At]; left. Qed.
+
 Lemma setDUl T (A B C : set T) : (A `|` B) `\` C = (A `\` C) `|` (B `\` C).
 Proof. by rewrite !setDE setIUl. Qed.
 
@@ -616,10 +643,10 @@ Lemma setDD T (A B : set T) : A `\` (A `\` B) = A `&` B.
 Proof. by rewrite 2!setDE setCI setCK setIUr setICr set0U. Qed.
 
 Lemma bigcup_set0 T U (X : U -> set T) : \bigcup_(i in set0) X i = set0.
-Proof. by apply eqEsubset => a // []. Qed.
+Proof. by rewrite eqEsubset; split => a // []. Qed.
 
 Lemma bigcup_set1 T V (U : V -> set T) v : \bigcup_(i in [set v]) U i = U v.
-Proof. by apply: eqEsubset => ? => [[] ? -> //|]; exists v. Qed.
+Proof. by rewrite eqEsubset; split => ? => [[] ? -> //|]; exists v. Qed.
 
 Lemma bigcapCU T I (U : I -> set T) E :
   \bigcap_(i in E) (U i) = ~` (\bigcup_(i in E) (~` U i)).
@@ -652,7 +679,8 @@ CoInductive xget_spec {T : choiceType} x0 (P : set T) : T -> Prop -> Type :=
 | XGetSome x of x = xget x0 P & P x : xget_spec x0 P x True
 | XGetNone of (forall x, ~ P x) : xget_spec x0 P x0 False.
 
-Lemma xgetP {T : choiceType} x0 (P : set T) : xget_spec x0 P (xget x0 P) (P (xget x0 P)).
+Lemma xgetP {T : choiceType} x0 (P : set T) :
+  xget_spec x0 P (xget x0 P) (P (xget x0 P)).
 Proof.
 move: (erefl (xget x0 P)); set y := {2}(xget x0 P).
 rewrite /xget; case: pselect => /= [?|neqP _].
@@ -675,7 +703,8 @@ Lemma xget_unique  {T : choiceType} x0 (P : set T) (x : T) :
   P x -> (forall y, P y -> y = x) -> xget x0 P = x.
 Proof. by move=> /xget_subset1 gPx eqx; apply: gPx=> y z /eqx-> /eqx. Qed.
 
-Lemma xgetPN {T : choiceType} x0 (P : set T) : (forall x, ~ P x) -> xget x0 P = x0.
+Lemma xgetPN {T : choiceType} x0 (P : set T) :
+  (forall x, ~ P x) -> xget x0 P = x0.
 Proof. by case: xgetP => // x _ Px /(_ x). Qed.
 
 Definition fun_of_rel {A} {B : choiceType} (f0 : A -> B) (f : A -> B -> Prop) :=
@@ -685,9 +714,10 @@ Lemma fun_of_relP {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a :
   f a !=set0 -> f a (fun_of_rel f0 f a).
 Proof. by move=> [b fab]; rewrite /fun_of_rel; apply: xgetI fab. Qed.
 
-Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a :
+Lemma fun_of_rel_uniq {A} {B : choiceType}
+    (f : A -> B -> Prop) (f0 : A -> B) a :
   is_subset1 (f a) -> forall b, f a b ->  fun_of_rel f0 f a = b.
-Proof. by move=> fa_prop b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.
+Proof. by move=> fa1 b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.
 
 Section SetMonoids.
 Variable (T : Type).
@@ -804,7 +834,8 @@ Canonical arrow_pointedType (T : Type) (T' : pointedType) :=
   PointedType (T -> T') (fun=> point).
 
 Definition dep_arrow_pointedType (T : Type) (T' : T -> pointedType) :=
-  Pointed.Pack (Pointed.Class (dep_arrow_choiceClass T') (fun i => @point (T' i))).
+  Pointed.Pack
+   (Pointed.Class (dep_arrow_choiceClass T') (fun i => @point (T' i))).
 
 Canonical bool_pointedType := PointedType bool false.
 Canonical Prop_pointedType := PointedType Prop False.
@@ -1136,3 +1167,103 @@ exists n.+1; split => // m Em; case/existsNP : En => k /not_implyP[Ek /negP].
 rewrite -Order.TotalTheory.ltNge => kn.
 by rewrite (Order.POrderTheory.le_trans _ (Em _ Ek)).
 Qed.
+
+Fact set_display : unit. Proof. by []. Qed.
+
+Module SetOrder.
+Module Internal.
+Section SetOrder.
+
+Context {T : Type}.
+Implicit Types X Y : set T.
+
+Lemma le_def X Y : `[< X `<=` Y >] = (X `&` Y == X).
+Proof. by apply/asboolP/eqP; rewrite setIidPl. Qed.
+
+Lemma lt_def X Y : `[< X `<` Y >] = (Y != X) && `[< X `<=` Y >].
+Proof.
+apply/idP/idP => [/asboolP|/andP[YX /asboolP XY]]; rewrite properEneq eq_sym;
+  by [move=> [] -> /asboolP|apply/asboolP].
+Qed.
+
+Fact SetOrder_joinKI (Y X : set T) : X `&` (X `|` Y) = X.
+Proof. by rewrite setUC setKU. Qed.
+
+Fact SetOrder_meetKU (Y X : set T) : X `|` (X `&` Y) = X.
+Proof. by rewrite setIC setKI. Qed.
+
+Definition orderMixin := @MeetJoinMixin _ _ (fun X Y => `[<proper X Y>]) setI
+  setU le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _) SetOrder_joinKI
+  SetOrder_meetKU (@setIUl _) setIid.
+
+Local Canonical porderType := POrderType set_display (set T) orderMixin.
+Local Canonical latticeType := LatticeType (set T) orderMixin.
+Local Canonical distrLatticeType := DistrLatticeType (set T) orderMixin.
+
+Fact SetOrder_sub0set (x : set T) : (set0 <= x)%O.
+Proof. by apply/asboolP; apply: sub0set. Qed.
+
+Fact SetOrder_setTsub (x : set T) : (x <= setT)%O.
+Proof. exact/asboolP. Qed.
+
+Local Canonical bLatticeType :=
+  BLatticeType (set T) (Order.BLattice.Mixin  SetOrder_sub0set).
+Local Canonical tbLatticeType :=
+  TBLatticeType (set T) (Order.TBLattice.Mixin SetOrder_setTsub).
+Local Canonical bDistrLatticeType := [bDistrLatticeType of set T].
+Local Canonical tbDistrLatticeType := [tbDistrLatticeType of set T].
+
+Lemma subKI X Y : Y `&` (X `\` Y) = set0.
+Proof. by rewrite setDE setICA setICr setI0. Qed.
+
+Lemma joinIB X Y : (X `&` Y) `|` X `\` Y = X.
+Proof. by rewrite setDE -setIUr setUCr setIT. Qed.
+
+Local Canonical cbDistrLatticeType := CBDistrLatticeType (set T)
+  (@CBDistrLatticeMixin _ _ (fun X Y => X `\` Y) subKI joinIB).
+
+Local Canonical ctbDistrLatticeType := CTBDistrLatticeType (set T)
+  (@CTBDistrLatticeMixin _ _ _ (fun X => ~` X) (fun x => esym (setTD x))).
+
+End SetOrder.
+End Internal.
+
+Module Exports.
+
+Canonical Internal.porderType.
+Canonical Internal.latticeType.
+Canonical Internal.distrLatticeType.
+Canonical Internal.bLatticeType.
+Canonical Internal.tbLatticeType.
+Canonical Internal.bDistrLatticeType.
+Canonical Internal.tbDistrLatticeType.
+Canonical Internal.cbDistrLatticeType.
+Canonical Internal.ctbDistrLatticeType.
+
+Lemma subsetEset {T} (X Y : set T) : (X <= Y)%O = (X `<=` Y) :> Prop.
+Proof. by rewrite asboolE. Qed.
+
+Lemma properEset  {T} (X Y : set T) : (X < Y)%O = (X `<` Y) :> Prop.
+Proof. by rewrite asboolE. Qed.
+
+Lemma subEset {T} (X Y : set T) : (X `\` Y)%O = (X `\` Y). Proof. by []. Qed.
+
+Lemma complEset {T} (X Y : set T) : (~` X)%O = ~` X. Proof. by []. Qed.
+
+Lemma botEset {T} (X Y : set T) : 0%O = @set0 T. Proof. by []. Qed.
+
+Lemma topEset {T} (X Y : set T) : 1%O = @setT T. Proof. by []. Qed.
+
+Lemma meetEset {T} (X Y : set T) : (X `&` Y)%O = (X `&` Y). Proof. by []. Qed.
+
+Lemma joinEset {T} (X Y : set T) : (X `|` Y)%O = (X `|` Y). Proof. by []. Qed.
+
+Lemma subsetPset {T} (X Y : set T) : reflect (X `<=` Y) (X <= Y)%O.
+Proof. by apply: (iffP idP); rewrite subsetEset. Qed.
+
+Lemma properPset {T} (X Y : set T) : reflect (X `<` Y) (X < Y)%O.
+Proof. by apply: (iffP idP); rewrite properEset. Qed.
+
+End Exports.
+End SetOrder.
+Export SetOrder.Exports.

theories/topology.v

@@ -806,7 +806,7 @@ Definition near_simpl := (@near_simpl, @near_filter_onE).
 Program Definition trivial_filter_on T := FilterType [set setT : set T] _.
 Next Obligation.
 split=> // [_ _ -> ->|Q R sQR QT]; first by rewrite setIT.
-by apply: eqEsubset => // ? _; apply/sQR; rewrite QT.
+by move; rewrite eqEsubset; split => // ? _; apply/sQR; rewrite QT.
 Qed.
 Canonical trivial_filter_on.