diff --git a/src/finlattice.v b/src/finlattice.v index aef0449..458e563 100644 --- a/src/finlattice.v +++ b/src/finlattice.v @@ -1,17 +1,14 @@ -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect finmap. Require Import xbigop extra_misc. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing.Theory Num.Theory. - Local Open Scope fset_scope. -Local Open Scope ring_scope. +Local Open Scope order_scope. -Import RelOrder. -Import RelOrder.Theory. +Import RelOrder.Theory Order.LTheory. (* -------------------------------------------------------------------- *) Section FsetOrderTheory. @@ -67,447 +64,437 @@ End FsetOrderTheory. (* -------------------------------------------------------------------- *) (* TODO: move this section to relorder.v *) -Section POrderMonotonyTheory. -Context (T T' : choiceType) (r : {pOrder T}) (r' : {pOrder T'}). -Context (D D' : pred T) (f : T -> T'). - -Hint Resolve rlt_neqAle rle_anti : core. - -Lemma ltW_homo : - {homo f : x y / x <_r y >-> x <_r' y} - -> {homo f : x y / x <=_r y >-> x <=_r' y}. -Proof. exact: homoW. Qed. - -Lemma inj_homo_lt : - injective f - -> {homo f : x y / x <=_r y >-> x <=_r' y} - -> {homo f : x y / x <_r y >-> x <_r' y}. -Proof. exact: inj_homo. Qed. - -Lemma inc_inj : {mono f : x y / x <=_r y >-> x <=_r' y} -> injective f. -Proof. exact: mono_inj. Qed. - -Lemma leW_mono : - {mono f : x y / x <=_r y >-> x <=_r' y} - -> {mono f : x y / x <_r y >-> x <_r' y}. -Proof. exact: anti_mono. Qed. - -Lemma ltW_homo_in : - {in D & D', {homo f : x y / x <_r y >-> x <_r' y}} - -> {in D & D', {homo f : x y / x <=_r y >-> x <=_r' y}}. -Proof. exact: homoW_in. Qed. - -Lemma inj_homo_lt_in : - {in D & D', injective f} - -> {in D & D', {homo f : x y / x <=_r y >-> x <=_r' y}} - -> {in D & D', {homo f : x y / x <_r y >-> x <_r' y}}. -Proof. exact: inj_homo_in. Qed. - -Lemma inc_inj_in : - {in D &, {mono f : x y / x <=_r y >-> x <=_r' y}} - -> {in D &, injective f}. -Proof. exact: mono_inj_in. Qed. - -Lemma leW_mono_in : - {in D &, {mono f : x y / x <=_r y >-> x <=_r' y}} - -> {in D &, {mono f : x y / x <_r y >-> x <_r' y}}. -Proof. exact: anti_mono_in. Qed. -End POrderMonotonyTheory. - (* -------------------------------------------------------------------- *) -(* TODO: move this section to relorder.v *) Section POrderMonotonyTheoryCodom. -Context (d : unit) (T : choiceType) (T' : porderType d) (r : {pOrder T}). +Context (T : choiceType) (r : {pOrder T}). +Context (d : Order.disp_t) (T' : porderType d). Context (D D' : pred T) (f : T -> T'). Hint Resolve rlt_neqAle rle_anti : core. -Hint Resolve Order.POrderTheory.lt_neqAle Order.POrderTheory.le_anti : core. Lemma ltW_homo_as : - {homo f : x y / x <_r y >-> (x < y)%O} - -> {homo f : x y / x <=_r y >-> (x <= y)%O}. + {homo f : x y / x <_r y >-> x < y} -> {homo f : x y / x <=_r y >-> x <= y}. Proof. by apply: homoW. Qed. Lemma inj_homo_lt_as : - injective f - -> {homo f : x y / x <=_r y >-> (x <= y)%O} - -> {homo f : x y / x <_r y >-> (x < y)%O}. + injective f -> + {homo f : x y / x <=_r y >-> x <= y} -> {homo f : x y / x <_r y >-> x < y}. Proof. exact: inj_homo. Qed. -Lemma inc_inj_as : {mono f : x y / x <=_r y >-> (x <= y)%O} -> injective f. +Lemma inc_inj_as : {mono f : x y / x <=_r y >-> x <= y} -> injective f. Proof. exact: mono_inj. Qed. Lemma leW_mono_as : - {mono f : x y / x <=_r y >-> (x <= y)%O} - -> {mono f : x y / x <_r y >-> (x < y)%O}. + {mono f : x y / x <=_r y >-> x <= y} -> {mono f : x y / x <_r y >-> x < y}. Proof. exact: anti_mono. Qed. Lemma ltW_homo_in_as : - {in D & D', {homo f : x y / x <_r y >-> (x < y)%O}} - -> {in D & D', {homo f : x y / x <=_r y >-> (x <= y)%O}}. + {in D & D', {homo f : x y / x <_r y >-> x < y}} -> + {in D & D', {homo f : x y / x <=_r y >-> x <= y}}. Proof. exact: homoW_in. Qed. Lemma inj_homo_lt_in_as : - {in D & D', injective f} - -> {in D & D', {homo f : x y / x <=_r y >-> (x <= y)%O}} - -> {in D & D', {homo f : x y / x <_r y >-> (x < y)%O}}. + {in D & D', injective f} -> + {in D & D', {homo f : x y / x <=_r y >-> x <= y}} -> + {in D & D', {homo f : x y / x <_r y >-> x < y}}. Proof. exact: inj_homo_in. Qed. Lemma inc_inj_in_as : - {in D &, {mono f : x y / x <=_r y >-> (x <= y)%O}} - -> {in D &, injective f}. + {in D &, {mono f : x y / x <=_r y >-> x <= y}} -> + {in D &, injective f}. Proof. exact: mono_inj_in. Qed. Lemma leW_mono_in_as : - {in D &, {mono f : x y / x <=_r y >-> (x <= y)%O}} - -> {in D &, {mono f : x y / x <_r y >-> (x < y)%O}}. + {in D &, {mono f : x y / x <=_r y >-> x <= y}} -> + {in D &, {mono f : x y / x <_r y >-> x < y}}. Proof. exact: anti_mono_in. Qed. + End POrderMonotonyTheoryCodom. (* -------------------------------------------------------------------- *) -Module PreLattice. +Module Prelattice. Section ClassDef. -Context {T : choiceType}. - Set Primitive Projections. -Record mixin_of (le : rel T) (witness : T) - (premeet : {fset T} -> T -> T -> T) - (prejoin : {fset T} -> T -> T -> T) := Mixin -{ - premeet_min : forall S x y, x \in S -> y \in S -> - le (premeet S x y) x /\ le (premeet S x y) y; - premeet_inf : forall S x y z, x \in S -> y \in S -> z \in S -> - le z x -> le z y -> le z (premeet S x y); - premeet_incr : forall S S' x y, S `<=` S' -> x \in S -> y \in S -> - le (premeet S x y) (premeet S' x y); - prejoin_max : forall S x y, x \in S -> y \in S -> - rdual_rel le (prejoin S x y) x /\ rdual_rel le (prejoin S x y) y; - prejoin_sumeet : forall S x y z, x \in S -> y \in S -> z \in S -> - rdual_rel le z x -> rdual_rel le z y -> - rdual_rel le z (prejoin S x y); - prejoin_decr : forall S S' x y, S `<=` S' -> x \in S -> y \in S -> - rdual_rel le (prejoin S x y) (prejoin S' x y) -}. - -Record class_of (le lt : rel T) (witness : T) - (premeet : {fset T} -> T -> T -> T) - (prejoin : {fset T} -> T -> T -> T) := Class { - base : POrder.class_of le lt; - mixin : mixin_of le witness premeet prejoin; -}. - -Structure order (phT : phant T) := Pack { - le : rel T; - lt : rel T; +Record mixin_of (T0 : Type) (b : Order.POrder.class_of T0) + (T := Order.POrder.Pack Order.disp_tt b) := Mixin { witness : T; premeet : {fset T} -> T -> T -> T; prejoin : {fset T} -> T -> T -> T; - class_ : class_of le lt witness premeet prejoin + premeet_min : forall S x y, x \in S -> y \in S -> + premeet S x y <= x /\ premeet S x y <= y; + premeet_inf : forall S x y z, x \in S -> y \in S -> z \in S -> + z <= x -> z <= y -> z <= premeet S x y; + premeet_incr : forall S U x y, S `<=` U -> x \in S -> y \in S -> + premeet U x y \in S -> premeet S x y <= premeet U x y; + prejoin_max : forall S x y, x \in S -> y \in S -> + prejoin S x y >= x /\ prejoin S x y >= y; + prejoin_sumeet : forall S x y z, x \in S -> y \in S -> z \in S -> + z >= x -> z >= y -> z >= prejoin S x y; + prejoin_decr : forall S U x y, S `<=` U -> x \in S -> y \in S -> + prejoin U x y \in S -> prejoin S x y >= prejoin U x y }. -Unset Primitive Projections. +Record class_of (T : Type) := Class { + base : Order.POrder.class_of T; + mixin : mixin_of base; +}. -Local Coercion base : class_of >-> POrder.class_of. +Unset Primitive Projections. +Local Coercion base : class_of >-> Order.POrder.class_of. -Variable (phT : phant T) (ord : order phT). +Structure type (disp : Order.disp_t) := Pack { sort; _ : class_of sort }. -Definition class : class_of (le ord) (lt ord) - (witness ord) (premeet ord) (prejoin ord) := - let: Pack _ _ _ _ _ c as ord' := ord in c. -Definition pOrder := @POrder.Pack _ phT (le ord) (lt ord) class. +Local Coercion sort : type >-> Sortclass. -Variable (leT ltT : rel T) (wT : T) - (premeetT : {fset T} -> T -> T -> T) - (prejoinT : {fset T} -> T -> T -> T). +Variables (T : Type) (disp : Order.disp_t) (cT : type disp). -Definition clone c of phant_id class c := - @Pack phT leT ltT wT premeetT prejoinT (nosimpl c). +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Definition pack (m0 : mixin_of leT wT premeetT prejoinT) := - fun (bord : POrder.order phT) b - & phant_id (POrder.class bord) b => - fun m & phant_id m0 m => - @Pack phT leT ltT wT premeetT prejoinT - (@Class leT ltT wT premeetT prejoinT b m). +Definition pack := + fun bT b & phant_id (@Order.POrder.class disp bT) b => + fun m => Pack disp (@Class T b m). +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @Order.POrder.Pack disp cT class. End ClassDef. -(* ---------------------------------------------------------------------- *) Module Exports. -Coercion base : class_of >-> POrder.class_of. -Coercion pOrder : order >-> POrder.order. -Canonical pOrder. -Notation "{ 'preLattice' T }" := (order (Phant T)) - (at level 0, format "{ 'preLattice' T }"). -Notation PreLattice le lt w premeet prejoin mixin := - (@pack _ (Phant _) le lt w premeet prejoin mixin _ _ id _ id). -Notation "[ 'preLattice' 'of' le ]" := - (@clone _ (Phant _) _ le (nosimpl _) (nosimpl _) (nosimpl _) (nosimpl _) _ id) - (at level 0, format "[ 'preLattice' 'of' le ]"). -Notation witness := witness. -Notation premeet := premeet. -Notation prejoin := prejoin. +Coercion base : class_of >-> Order.POrder.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. +Coercion choiceType : type >-> Choice.type. +Coercion porderType : type >-> Order.POrder.type. +Canonical eqType. +Canonical choiceType. +Canonical porderType. +Notation prelatticeType := type. +Notation PrelatticeType T m := (@pack T _ _ _ id m). +Notation "[ 'prelatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'prelatticeType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'prelatticeType' 'of' T 'for' cT 'with' disp ]" := + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'prelatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. +Notation "[ 'prelatticeType' 'of' T ]" := [prelatticeType of T for _] + (at level 0, format "[ 'prelatticeType' 'of' T ]") : form_scope. +Notation "[ 'prelatticeType' 'of' T 'with' disp ]" := + [prelatticeType of T for _ with disp] + (at level 0, format "[ 'prelatticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End PreLattice. -Import PreLattice.Exports. +End Prelattice. +Export Prelattice.Exports. -Section DualPreLattice. +Section PrelatticeDef. +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Definition witness : T := Prelattice.witness (Prelattice.class T). +Definition premeet : {fset T} -> T -> T -> T := + Prelattice.premeet (Prelattice.class T). +Definition prejoin : {fset T} -> T -> T -> T := + Prelattice.prejoin (Prelattice.class T). +End PrelatticeDef. -Context {T: choiceType}. -Variable (L : {preLattice T}). +Notation dual_premeet := (@premeet (Order.dual_display _) _). +Notation dual_prejoin := (@prejoin (Order.dual_display _) _). +Notation "premeet^d" := dual_premeet. +Notation "prejoin^d" := dual_prejoin. -Definition DualPreLatticeMixin := - let: PreLattice.Class _ m := PreLattice.class L in - @PreLattice.Mixin T - _ - (PreLattice.witness L) - (prejoin L) (premeet L) - (PreLattice.prejoin_max m) (PreLattice.prejoin_sumeet m) - (PreLattice.prejoin_decr m) - (PreLattice.premeet_min m) (PreLattice.premeet_inf m) - (PreLattice.premeet_incr m). +Section PrelatticeTheory. -Canonical DualPreLatticePack := - PreLattice (rdual_rel <=:L) (rdual_rel <:L) _ _ _ DualPreLatticeMixin. +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Implicit Type (S : {fset T}) (x y : T). -End DualPreLattice. +Lemma premeet_minlr S: + {in S &, forall x y, premeet S x y <= x /\ premeet S x y <= y}. +Proof. exact: Prelattice.premeet_min. Qed. -Notation "L ^~pl" := ([preLattice of rdual_rel <=:L]) (at level 0, only parsing). +Lemma premeet_minl S: + {in S &, forall x y, premeet S x y <= x}. +Proof. by move=> x y xS yS; case: (premeet_minlr xS yS). Qed. -Section PreLatticeTheory. +Lemma premeet_minr S: + {in S &, forall x y, premeet S x y <= y}. +Proof. by move=> x y xS yS; case: (premeet_minlr xS yS). Qed. -Context {T: choiceType}. -Implicit Type L: {preLattice T}. +Definition premeet_min := (premeet_minl, premeet_minr). -(* TO IMPROVE *) -Definition mixin L := (PreLattice.mixin (PreLattice.class L)). +Lemma premeet_inf S: + {in S & &, forall x y z, z <= x -> z <= y -> z <= premeet S x y}. +Proof. exact: Prelattice.premeet_inf. Qed. -Lemma premeet_min_r L S: - {in S &, forall x y, premeet L S x y <=_L x /\ premeet L S x y <=_L y}. -Proof. exact: (PreLattice.premeet_min (mixin L)). Qed. +Lemma premeet_incr S U: S `<=` U -> + {in S &, forall x y, premeet U x y \in S -> + premeet S x y <= premeet U x y}. +Proof. move=> ??????; exact: Prelattice.premeet_incr. Qed. -Lemma premeet_minl L S: - {in S &, forall x y, premeet L S x y <=_L x}. -Proof. by move=> x y xS yS; case: (PreLattice.premeet_min (mixin L) xS yS). Qed. +Lemma prejoin_max S: + {in S &, forall x y, x <= prejoin S x y /\ y <= prejoin S x y}. +Proof. exact: Prelattice.prejoin_max. Qed. -Lemma premeet_minr L S: - {in S &, forall x y, premeet L S x y <=_L y}. -Proof. by move=> x y xS yS; case: (PreLattice.premeet_min (mixin L) xS yS). Qed. +Lemma prejoin_maxl S: + {in S &, forall x y, x <= prejoin S x y}. +Proof. by move=> x y xS yS; case: (prejoin_max xS yS). Qed. -Definition premeet_min := (premeet_minl, premeet_minr). +Lemma prejoin_maxr S: + {in S &, forall x y, y <= prejoin S x y}. +Proof. by move=> x y xS yS; case: (prejoin_max xS yS). Qed. -Lemma premeet_inf L S: - {in S & &, forall x y z, z <=_L x -> z <=_L y -> z <=_L premeet L S x y}. -Proof. exact: (PreLattice.premeet_inf (mixin L)). Qed. +Lemma prejoin_sumeet S: + {in S & &, forall x y z, x <= z -> y <= z -> prejoin S x y <= z}. +Proof. exact: Prelattice.prejoin_sumeet. Qed. -Lemma premeet_incr L S S': S `<=` S' -> - {in S &, forall x y, premeet L S x y <=_L premeet L S' x y}. -Proof. move=> ?????; exact: (PreLattice.premeet_incr (mixin L)). Qed. +Lemma prejoin_decr S U: S `<=` U -> + {in S &, forall x y, + prejoin U x y \in S -> prejoin U x y <= prejoin S x y}. +Proof. move=> ??????; exact: Prelattice.prejoin_decr. Qed. -Lemma prejoin_max L S: - {in S &, forall x y, x <=_L prejoin L S x y /\ y <=_L prejoin L S x y}. -Proof. exact: (PreLattice.prejoin_max (mixin L)). Qed. +End PrelatticeTheory. -Lemma prejoin_maxl L S: - {in S &, forall x y, x <=_L prejoin L S x y}. -Proof. by move=> x y xS yS; case: (PreLattice.prejoin_max (mixin L) xS yS). Qed. +Section DualPrelattice. -Lemma prejoin_maxr L S: - {in S &, forall x y, y <=_L prejoin L S x y}. -Proof. by move=> x y xS yS; case: (PreLattice.prejoin_max (mixin L) xS yS). Qed. +Context {disp : Order.disp_t} (T : prelatticeType disp). -Lemma prejoin_sumeet L S: - {in S & &, forall x y z, x <=_L z -> y <=_L z -> prejoin L S x y <=_L z}. -Proof. exact: (PreLattice.prejoin_sumeet (mixin L)). Qed. +Definition dual_prelatticeMixin := + @Prelattice.Mixin _ (Order.POrder.class [porderType of T^d]) witness + (@prejoin _ T) (@premeet _ T) + (@Prelattice.prejoin_max _ _ (Prelattice.class T)) + (@Prelattice.prejoin_sumeet _ _ (Prelattice.class T)) + (@Prelattice.prejoin_decr _ _ (Prelattice.class T)) + (@Prelattice.premeet_min _ _ (Prelattice.class T)) + (@Prelattice.premeet_inf _ _ (Prelattice.class T)) + (@Prelattice.premeet_incr _ _ (Prelattice.class T)). -Lemma prejoin_decr L S S': S `<=` S' -> - {in S &, forall x y, prejoin L S' x y <=_L prejoin L S x y}. -Proof. move=> ?????; exact: (PreLattice.prejoin_decr (mixin L)). Qed. +Canonical dual_prelatticeType := PrelatticeType T^d dual_prelatticeMixin. -Lemma dual_premeet L S x y: - premeet [preLattice of rdual_rel <=:L] S x y = prejoin L S x y. +Lemma prejoinEdual (S : {fset T}) (x y : T) : + prejoin^d (S : {fset T^d}) x y = premeet S x y. Proof. by []. Qed. -Lemma dual_prejoin L S x y: - prejoin [preLattice of rdual_rel <=:L] S x y = premeet L S x y. +Lemma premeetEdual (S : {fset T}) (x y : T) : + premeet^d (S : {fset T^d}) x y = prejoin S x y. Proof. by []. Qed. -End PreLatticeTheory. +End DualPrelattice. (* ================================================================== *) -Section MeetToPreLattice. +Section MeetToPrelattice. -Context {T: choiceType} (M : {tMeetOrder T}). -Definition Mmeet (S: {fset T}) := meet M. -Definition Mjoin (S:{fset T}) x y := - \big[ (meet M) / (top M) ]_(i <- S | (x <=_M i) && (y <=_M i)) i. +Context {disp : Order.disp_t} {T : tMeetSemilatticeType disp}. -Lemma Mmeet_min S x y : x \in S -> y \in S -> - Mmeet S x y <=_M x /\ Mmeet S x y <=_M y. -Proof. by move=> xS yS; rewrite rleIl rleIr. Qed. +Definition mpremeet & {fset T} := @Order.meet _ T. -Lemma Mmeet_inf S x y z : - x \in S -> y \in S -> z \in S -> - z <=_M x -> z <=_M y -> - z <=_M Mmeet S x y. -Proof. by move=> xS yS zS; rewrite rlexI => -> ->. Qed. +Definition mprejoin (S : {fset T}) x y := + \meet_(i <- S | (x <= i) && (y <= i)) i. + +Lemma mpremeet_min S x y : x \in S -> y \in S -> + mpremeet S x y <= x /\ mpremeet S x y <= y. +Proof. by move=> xS yS; rewrite leIl leIr. Qed. -Lemma Mmeet_incr S S' x y : - S `<=` S' -> x \in S -> y \in S -> - Mmeet S x y <=_M Mmeet S' x y. +Lemma mpremeet_inf S x y z : + x \in S -> y \in S -> z \in S -> z <= x -> z <= y -> z <= mpremeet S x y. +Proof. by move=> xS yS zS; rewrite lexI => -> ->. Qed. + +Lemma mpremeet_incr S U x y : + S `<=` U -> x \in S -> y \in S -> + mpremeet U x y \in S -> + mpremeet S x y <= mpremeet U x y. Proof. by []. Qed. -Lemma Mjoin_max S x y : +Lemma mprejoin_max S x y : x \in S -> y \in S -> - x <=_M Mjoin S x y /\ y <=_M Mjoin S x y. -Proof. by move=> xS yS; split; apply/rmeetsP_seq => ?? /andP []. Qed. + x <= mprejoin S x y /\ y <= mprejoin S x y. +Proof. by move=> xS yS; split; apply/meetsP_seq => ?? /andP []. Qed. -Lemma Mjoin_sumeet S x y z : +Lemma mprejoin_sumeet S x y z : x \in S -> y \in S -> z \in S -> - x <=_M z -> y <=_M z -> Mjoin S x y <=_M z. -Proof. by move=> xS yS zS xlez ylez; apply: rmeets_inf_seq => //; apply/andP. Qed. + x <= z -> y <= z -> mprejoin S x y <= z. +Proof. by move=> xS yS zS xlez ylez; apply: meets_inf_seq => //; apply/andP. Qed. -Lemma Mjoin_decr S S' x y : - S `<=` S' -> x \in S -> y \in S -> - Mjoin S' x y <=_M Mjoin S x y. +Lemma mprejoin_decr S U x y : + S `<=` U -> x \in S -> y \in S -> + mprejoin U x y \in S -> + mprejoin U x y <= mprejoin S x y. Proof. -move=> /fsubsetP Ssub xS yS; apply/rmeetsP_seq => z zS /andP [xlez ylez]. -apply: rmeets_inf_seq; rewrite ?xlez ?ylez //. +move=> /fsubsetP Ssub xS yS _; apply/meetsP_seq => z zS /andP [xlez ylez]. +apply: meets_inf_seq; rewrite ?xlez ?ylez //. exact: Ssub. Qed. -Definition MeetPreLatticeMixin := @PreLattice.Mixin - T (<=:M) (top M) _ _ (Mmeet_min) (Mmeet_inf) (Mmeet_incr) - (Mjoin_max) (Mjoin_sumeet) (Mjoin_decr). +Definition tMeetSemilatticeType_prelattice := + @Prelattice.Mixin _ (Order.POrder.class T) Order.top + _ _ mpremeet_min mpremeet_inf mpremeet_incr + mprejoin_max mprejoin_sumeet mprejoin_decr. -(*Canonical MeetPreLattice := - PreLattice (<=:M) _ _ _ _ MeetPreLatticeMixin. -*) -End MeetToPreLattice. +(* FIXME: introduce a tag for T (non-forgetful inheritance) *) +Canonical tMeetSemilattice_prelatticeType := + PrelatticeType T tMeetSemilatticeType_prelattice. -Section JoinToPreLattice. +End MeetToPrelattice. -Context {T: choiceType} (J : {bJoinOrder T}). +Section JoinToPrelattice. -Definition JoinPreLatticeMixin := - MeetPreLatticeMixin [tMeetOrder of rdual_rel <=:J]. +Context {disp : Order.disp_t} {T : bJoinSemilatticeType disp}. -End JoinToPreLattice. +Definition bJoinSemilatticeType_prelattice := + @tMeetSemilatticeType_prelattice _ [tMeetSemilatticeType of T^d]. +(* FIXME: introduce a tag for T (non-forgetful inheritance) *) +Canonical bJoinSemilattice_prelatticeType := + [prelatticeType of T for PrelatticeType T^d bJoinSemilatticeType_prelattice]. -Section FinLattice. +End JoinToPrelattice. -Context {T : choiceType}. +(* ========================================================================== *) -Definition premeet_closed (L: {preLattice T}) (S : {fset T}) := - [forall x : S, [forall y : S, premeet L S (fsval x) (fsval y) \in S]]. +Definition is_premeet_closed + {disp : Order.disp_t} {T : prelatticeType disp} (S : {fset T}) := + [forall x : S, [forall y : S, premeet S (fsval x) (fsval y) \in S]]. -(*TODO : Change S by a predicate*) +Definition is_prejoin_closed + {disp : Order.disp_t} {T : prelatticeType disp} (S : {fset T}) := + [forall x : S, [forall y : S, prejoin S (fsval x) (fsval y) \in S]]. -Lemma premeet_closedP (L: {preLattice T}) (S : {fset T}) : - reflect (forall x y, x \in S -> y \in S -> - premeet L S x y \in S) - (premeet_closed L S). +(*TODO : Change S by a predicate*) +Lemma premeet_closedP + {disp : Order.disp_t} {T : prelatticeType disp} (S : {fset T}) : + reflect (forall x y, x \in S -> y \in S -> premeet S x y \in S) + (is_premeet_closed S). Proof. -apply/(iffP idP). -- by move => + x y xS yS; move/forallP/(_ [`xS])/forallP/(_ [`yS]). -- move=> premeet_closedH; apply/forallP => x; apply/forallP => y. - apply: premeet_closedH; exact: fsvalP. +apply: (iffP idP) => [+ x y xS yS|]. +- by move/forallP/(_ [`xS])/forallP/(_ [`yS]). +- by move=> premeet_closedH; do 2 apply/forallP => ?; exact: premeet_closedH. Qed. -Variable (L: {preLattice T}). +Lemma prejoin_closedP + {disp : Order.disp_t} {T : prelatticeType disp} (S : {fset T}) : + reflect (forall x y, x \in S -> y \in S -> prejoin S x y \in S) + (is_prejoin_closed S). +Proof. exact: (@premeet_closedP _ [prelatticeType of T^d]). Qed. -Record finLattice := - FinLattice { elements :> {fset T}; - _ : [&& premeet_closed L elements, - premeet_closed L^~pl elements & - elements != fset0]}. +Module FinLattice. +Section ClassDef. -(*TODO: separate the conjunction into three separate fields*) +Set Primitive Projections. +Record finLattice_ (T0 : Type) (b : Prelattice.class_of T0) + (T := Prelattice.Pack Order.disp_tt b) := FinLattice { + elements_ : {fset T}; + premeet_closed : is_premeet_closed elements_; + prejoin_closed : is_prejoin_closed elements_; + fl_inhabited : elements_ != fset0; +}. +Unset Primitive Projections. -Canonical finLattice_subType := Eval hnf in [subType for elements]. +Context {disp : Order.disp_t} {T : prelatticeType disp}. -Definition finLattice_eqMixin := Eval hnf in [eqMixin of finLattice by <:]. -Canonical finLattice_eqType := Eval hnf in EqType finLattice finLattice_eqMixin. +Definition finLattice (_ : phant T) : Type := + @finLattice_ T (Prelattice.class T). -Definition finLattice_choiceMixin := [choiceMixin of finLattice by <:]. -Canonical finLattice_choiceType := - Eval hnf in ChoiceType finLattice finLattice_choiceMixin. +Context (phT : phant T). -(*Canonical finLattice_finType (S : finLattice) := [finType of S].*) +Definition elements (S : finLattice phT) : {fset T} := elements_ S. -(* FIXME: ambiguous path *) -Coercion mem_finLattice (S: finLattice) : {pred T} := - fun x : T => (x \in (elements S)). -Canonical finLattice_predType := PredType mem_finLattice. +Definition pred_finLattice (S : {fset T}) : bool := + [&& is_premeet_closed S, is_prejoin_closed S & S != fset0]. -Canonical finLattice_finPredType := - mkFinPredType finLattice (fun S => elements S) - (fun S => fset_uniq (elements S)) (fun _ _ => erefl). +Definition sub_finLattice (S : {fset T}) (w : pred_finLattice S) : + finLattice phT := + @FinLattice _ _ S (proj1 (andP w)) + (proj1 (andP (proj2 (andP w)))) (proj2 (andP (proj2 (andP w)))). -Lemma in_finLatticeE (S: finLattice) x : (x \in S) = (x \in elements S). -Proof. by []. Qed. +Lemma finLattice_rec (K : finLattice phT -> Type) : + (forall (x : {fset T}) (Px : pred_finLattice x), K (sub_finLattice Px)) -> + forall u : finLattice phT, K u. +Proof. +move=> HK [S HS1 HS2 HS3]. +have HS: pred_finLattice S by apply/and3P. +by congr (K (FinLattice _ _ _)): (HK S HS); apply: bool_irrelevance. +Qed. -Definition inE := (@in_finLatticeE, inE). +Local Canonical finLattice_subType := + SubType (finLattice phT) elements sub_finLattice finLattice_rec vrefl_rect. -Definition fmeet (S : finLattice) := (premeet L S). -Definition fjoin (S : finLattice) := (prejoin L S). +Definition finLattice_eqMixin := [eqMixin of finLattice phT by <:]. +Local Canonical finLattice_eqType := EqType (finLattice phT) finLattice_eqMixin. -Lemma finlattice_eqP (S S' : finLattice) : - S =i S' <-> S = S'. -Proof. by split => [eq |-> //];apply/val_inj/fsetP. Qed. +Definition finLattice_choiceMixin := [choiceMixin of finLattice phT by <:]. +Local Canonical finLattice_choiceType := + ChoiceType (finLattice phT) finLattice_choiceMixin. -End FinLattice. +Definition mem_finLattice (S: finLattice phT) : {pred T} := + pred_of_finset (elements S). +Local Canonical finLattice_predType := PredType mem_finLattice. -Notation "{ 'finLattice' L }" := (finLattice L) (at level 0, format "{ 'finLattice' L }"). -Notation "'\fmeet_' S" := (fmeet S) (at level 8, format "'\fmeet_' S"). -Notation "'\fjoin_' S" := (fjoin S) (at level 8, format "'\fjoin_' S"). +Local Canonical finLattice_finPredType := + mkFinPredType (finLattice phT) elements + (fun S => fset_uniq (elements S)) (fun _ _ => erefl). -(* Section Test. +End ClassDef. -Context {T: choiceType} {L : {preLattice T}} {S : {finLattice L}}. -Goal forall (f : T -> T), f @` S = S. - *) -(*Section Test. +Module Exports. +Notation finLattice := finLattice. +Notation FinLattice := FinLattice. +Notation elements := elements. +Coercion elements : finLattice >-> finset_of. +Canonical finLattice_subType. +Canonical finLattice_eqType. +Canonical finLattice_choiceType. +Canonical finLattice_predType. +Canonical finLattice_finPredType. +Notation "{ 'finLattice' T }" := + (@finLattice _ _ (Phant T)) (at level 0, format "{ 'finLattice' T }"). +End Exports. -Context {T : choiceType} {L : {preLattice T}}. -Context (S1 S2 : finLattice L) (P : T -> Prop). -Goal forall x y z, \fmeet_S1 x y = z <-> premeet L S1 x y = z. -move=> x y z; split; move=> ->. +End FinLattice. +Export FinLattice.Exports. -End Test.*) +Lemma in_finLatticeE {disp : Order.disp_t} {T : prelatticeType disp} + (S : {finLattice T}) x : (x \in S) = (x \in elements S). +Proof. by []. Qed. +Lemma finLattice_eqP {disp : Order.disp_t} {T : prelatticeType disp} + (S S' : {finLattice T}): S = S' <-> S =i S'. +Proof. split; [by move=>->|by move=> ?; apply/val_inj/fsetP]. Qed. -Section FinLatticeDual. +Definition inE := (@in_finLatticeE, inE). + +(* +Section Test. + +Context {disp : Order.disp_t} {T : prelatticeType disp} {S : {finLattice T}}. +Goal forall (f : T -> T), f @` S = S. Abort. + +Context (S1 S2 : {finLattice T}) (P : T -> Prop). +Goal forall x y z, premeet S1 x y = z. Abort. -Context {T : choiceType} (L : {preLattice T}) (S : {finLattice L}). +End Test. +*) -(* TODO: add (only parsing) notation for [preLattice of (<=:(L^~))] *) -(* TODO: same for semilattices and lattice *) +Section FinLatticeDual. -Lemma premeet_closedDual : - [&& premeet_closed L^~pl S, - (premeet_closed L S) & - S != fset0 :> {fset _}]. -Proof. by case: S => S0 premeet_closedS0; rewrite andbCA. Defined. +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). -Canonical FinLatticeDual := FinLattice premeet_closedDual. +(* FIXME: introduce a key *) +Canonical dual_finLattice : {finLattice T^d} := + @FinLattice.FinLattice _ + (Prelattice.class [prelatticeType of T^d]) _ + (FinLattice.prejoin_closed S) (FinLattice.premeet_closed S) + (FinLattice.fl_inhabited S). -Lemma dual_fjoinE: - \fjoin_(FinLatticeDual)= \fmeet_S. +Lemma dual_fjoinE: prejoin dual_finLattice = premeet S. Proof. by []. Qed. -Lemma dual_fmeetE: \fmeet_(FinLatticeDual) = \fjoin_S. +Lemma dual_fmeetE: premeet dual_finLattice = prejoin S. Proof. by []. Qed. End FinLatticeDual. -Notation "S ^~s" := (FinLatticeDual S) - (at level 8, format "S ^~s"). - +Notation "S ^fd" := (dual_finLattice S) (at level 8, format "S ^fd"). (* TODO: Module FinLatticeStructure *) (* use a lifting function : @@ -519,51 +506,45 @@ Notation "S ^~s" := (FinLatticeDual S) Module FinLatticeStructure. Section FinLatticeStructure. -Context {T : choiceType} {L : {preLattice T}} {S : {finLattice L}}. +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). Lemma finLattice_prop0 : S != fset0 :> {fset _}. -Proof. by case: S => S0 /= /and3P []. Qed. +Proof. by case: S. Qed. Definition witness := [`xchooseP (fset0Pn S finLattice_prop0)]. -Lemma mem_meet : forall x y, x \in S -> y \in S -> \fmeet_S x y \in S. -Proof. -case: S => S0 i x y; rewrite !inE /fmeet /=. -case/and3P: i => /premeet_closedP + _ _; exact. -Qed. +Lemma mem_meet : {in S &, forall x y, premeet S x y \in S}. +Proof. by case: S => S0 ? ? ?; apply/premeet_closedP. Qed. -Lemma mem_join : forall x y, x \in S -> y \in S -> \fjoin_S x y \in S. -Proof. -case: S => S0 i x y; rewrite !inE /fjoin /=. -case/and3P: i => _ /premeet_closedP + _; exact. -Qed. +Lemma mem_join : {in S &, forall x y, prejoin S x y \in S}. +Proof. by case: S => S0 ? ? ?; apply/prejoin_closedP. Qed. (* ------------------------------------------------------------------ *) -Definition finle (x y : S) := (val x <=_L val y). -Definition finlt (x y : S) := (val x <_L val y). +Definition finle (x y : S) := (val x <= val y). +Definition finlt (x y : S) := (val x < val y). Lemma finlexx : reflexive finle. Proof. by rewrite /finle. Qed. Lemma finle_anti : antisymmetric finle. -Proof. by move=> x y ?; apply/val_inj/(@rle_anti _ L). Qed. +Proof. by move=> x y ?; apply/val_inj/le_anti. Qed. Lemma finle_trans : transitive finle. -Proof. by move=> y x z; rewrite /finle; exact: rle_trans. Qed. +Proof. by move=> y x z; rewrite /finle; exact: le_trans. Qed. Lemma finlt_def : forall (x y : S), finlt x y = (y != x) && finle x y. -Proof. by move=> x y; rewrite /finle /finlt rlt_def; congr (_ && _). Qed. +Proof. by move=> x y; rewrite /finle /finlt lt_def; congr (_ && _). Qed. Definition finle_mixin := LePOrderMixin finlt_def finlexx finle_anti finle_trans. -Local Canonical fin_pOrder := POrder finle finlt finle_mixin. +Local Canonical fin_porderType := POrderType disp S finle_mixin. (* --------------------------------------------------------------- *) -Definition finmeet (x y : S) := fun2_val witness (\fmeet_S) x y. -Definition finjoin (x y : S) := fun2_val witness (\fjoin_S) x y. +Definition finmeet (x y : S) := fun2_val witness (premeet S) x y. +Definition finjoin (x y : S) := fun2_val witness (prejoin S) x y. Lemma finmeet_minl : forall x y, finle (finmeet x y) x. Proof. by move=> x y; rewrite /finle insubdK ?mem_meet ?premeet_minl ?fsvalP. Qed. @@ -667,39 +648,40 @@ by move=> x y z; apply: finle_anti; rewrite ?finjoin_sup ?finjoinAl ?finjoinAr ?in_fsetE ?eq_refl ?orbT. Qed. -Lemma lefinjoin : forall x y : S, rdual_rel finle x y = (finjoin x y == x). +Lemma lefinjoin : forall x y : S, dual_rel finle x y = (finjoin x y == x). Proof. move=> x y; apply/idP/eqP => [leyx | <-]; last by exact: finjoin_maxr. by apply/finle_anti; rewrite finjoin_maxl finjoin_sup ?finlexx. Qed. (* TODO: Would using MeetJoinMixin be better? *) -Definition fin_meetMixin := MeetRelMixin finmeetC finmeetA lefinmeet. -Definition fin_joinMixin := JoinRelMixin finjoinC finjoinA lefinjoin. +Definition fin_meetMixin := MeetMixin finmeetC finmeetA lefinmeet. +Definition fin_joinMixin := JoinMixin finjoinC finjoinA lefinjoin. -Local Canonical fin_meetOrder := MeetOrder finle finlt finmeet fin_meetMixin. -Local Canonical fin_joinOrder := JoinOrder finle finlt finjoin fin_joinMixin. -Local Canonical fin_lattice := [lattice of finle]. -(* TODO : are these canonical declarations mandatory ?*) +Local Canonical fin_meetSemilatticeType := MeetSemilatticeType S fin_meetMixin. +Local Canonical fin_joinSemilatticeType := JoinSemilatticeType S fin_joinMixin. +Local Canonical fin_latticeType := [latticeType of S]. End FinLatticeStructure. Module Exports. -Arguments finle {T L S} x y. -Arguments finlt {T L S} x y. -Arguments finmeet {T L S} x y. -Arguments finjoin {T L S} x y. +Arguments finle {disp T S} x y. +Arguments finlt {disp T S} x y. +Arguments finmeet {disp T S} x y. +Arguments finjoin {disp T S} x y. Notation finle := finle. Notation finlt := finlt. Notation finmeet := finmeet. Notation finjoin := finjoin. -Coercion fin_pOrder : finLattice >-> POrder.order. -Coercion fin_meetOrder : finLattice >-> Meet.order. -Coercion fin_joinOrder : finLattice >-> Join.order. -Coercion fin_lattice : finLattice >-> Lattice.order. -Canonical fin_pOrder. -Canonical fin_meetOrder. -Canonical fin_joinOrder. -Canonical fin_lattice. +(* FIXME: non-uniform coercion *) +(* FIXME: these instances should be reimplemented as builders *) +Coercion fin_porderType : finLattice >-> Order.POrder.type. +Coercion fin_meetSemilatticeType : finLattice >-> Order.MeetSemilattice.type. +Coercion fin_joinSemilatticeType : finLattice >-> Order.JoinSemilattice.type. +Coercion fin_latticeType : finLattice >-> Order.Lattice.type. +Canonical fin_porderType. +Canonical fin_meetSemilatticeType. +Canonical fin_joinSemilatticeType. +Canonical fin_latticeType. End Exports. End FinLatticeStructure. Import FinLatticeStructure.Exports. @@ -708,207 +690,199 @@ Import FinLatticeStructure.Exports. Section FinLatticeTheory. -Context {T: choiceType}. -Implicit Type L : {preLattice T}. - -Lemma sub_pred1 (K : {fset T}) (P : T -> Prop) : +(* TODO: move it *) +Lemma sub_pred1 (T : choiceType) (K : {fset T}) (P : T -> Prop) : (forall x : K, P (fsval x)) -> {in K, forall x, P x}. Proof. move=> Pval x xK; exact: (Pval [`xK]). Qed. -Lemma sub_pred2 (K : {fset T}) (P : T -> T -> Prop) : +Lemma sub_pred2 (T : choiceType) (K : {fset T}) (P : T -> T -> Prop) : (forall x y : K, P (fsval x) (fsval y)) -> {in K &, forall x y, P x y}. Proof. move=> Pval x y xS yS; exact: (Pval [`xS] [`yS]). Qed. -Lemma sub_pred3 (K : {fset T}) (P : T -> T -> T -> Prop) : +Lemma sub_pred3 (T : choiceType) (K : {fset T}) (P : T -> T -> T -> Prop) : (forall x y z: K, P (fsval x) (fsval y) (fsval z)) -> {in K & &, forall x y z, P x y z}. Proof. move=> Pval x y z xS yS zS; exact: (Pval [`xS] [`yS] [`zS]). Qed. -Lemma fmeetE L (S : {finLattice L}) : - \fmeet_S =2 premeet L S. +(* Lemma fmeetE (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : + premeet S =2 premeet S. Proof. by []. Qed. -Lemma fjoinE L (S : {finLattice L}) : - \fjoin_S =2 prejoin L S. -Proof. by []. Qed. +Lemma fjoinE (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : + prejoin S =2 prejoin S. +Proof. by []. Qed. *) -Lemma mem_fmeet L (S : {finLattice L}) : {in S &, forall x y, \fmeet_S x y \in S}. +Lemma mem_fmeet (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : + {in S &, forall x y, premeet S x y \in S}. Proof. -move=> x y; case: S => S premeet_closeds; rewrite !inE fmeetE /= => xS yS. -by case/andP: premeet_closeds => /premeet_closedP/(_ x y xS yS). +case: S => S premeet_closed ?? x y; rewrite !inE /=. +exact/premeet_closedP. Qed. -Lemma mem_fjoin L (S: {finLattice L}): {in S &, forall x y, \fjoin_S x y \in S}. -Proof. exact: (@mem_fmeet _ S^~s). Qed. +Lemma mem_fjoin (disp : Order.disp_t) (T : prelatticeType disp) (S: {finLattice T}) : + {in S &, forall x y, prejoin S x y \in S}. +Proof. exact: mem_fmeet S^fd. Qed. -Lemma finLattice_prop0 L (S : {finLattice L}): S != fset0 :> {fset _}. -Proof. by case: S => S /= /and3P []. Qed. +Lemma finLattice_prop0 (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}): S != fset0 :> {fset _}. +Proof. by case: S. Qed. -Lemma finLattice_leE L (S : {finLattice L}) : forall x y : S, - x <=_S y = fsval x <=_L fsval y. +Lemma finLattice_leE (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : forall x y : S, + x <= y = (fsval x <= fsval y). Proof. by []. Qed. -Lemma finLattice_meetE L (S : {finLattice L}) : forall x y : S, - fsval (meet S x y) = \fmeet_S (fsval x) (fsval y). +Lemma finLattice_meetE (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : forall x y : S, + fsval (Order.meet x y) = premeet S (fsval x) (fsval y). Proof. by move=> x y; rewrite insubdK ?mem_fmeet ?fsvalP. Qed. -Lemma finLattice_joinE L (S : {finLattice L}) : forall x y : S, - fsval (join S x y) = \fjoin_S (fsval x) (fsval y). +Lemma finLattice_joinE (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : forall x y : S, + fsval (Order.join x y) = prejoin S (fsval x) (fsval y). Proof. by move=> x y; rewrite insubdK ?mem_fjoin ?fsvalP. Qed. -Lemma finLattice_funE L (S : {finLattice L}) (f : T -> T): - f @` S = f @` (elements S). -Proof. -apply/fsetP => x; apply/idP/idP => /imfsetP [x' xS ->]; exact: in_imfset. -Qed. - - -(*Goal forall L, forall S : {finLattice L}, forall x y, join S x y = meet (S^~s) x y. +(*Goal forall L, forall S : {finLattice L}, forall x y, join S x y = meet (S^fd) x y. Proof. by move=> L S x y; apply/val_inj; rewrite !insubdK ?mem_fmeet ?fsvalP.*) Section FMeetTheory. -Lemma leIfl L (S : {finLattice L}) : {in S &, forall x y, \fmeet_S x y <=_L x}. +Context {disp : Order.disp_t} {T : prelatticeType disp}. + +Lemma leIfl (S : {finLattice T}) : {in S &, forall x y, premeet S x y <= x}. Proof. -apply: sub_pred2 => x y; move: (@rleIl _ S x y). +apply: sub_pred2 => x y; move: (@leIl _ S x y). by rewrite finLattice_leE finLattice_meetE. Qed. - -Lemma leIfr L (S : {finLattice L}) : {in S &, forall x y, \fmeet_S y x <=_L x}. +Lemma leIfr (S : {finLattice T}) : {in S &, forall x y, premeet S y x <= x}. Proof. -apply: sub_pred2 => x y; move: (@rleIr _ S x y). +apply: sub_pred2 => x y; move: (@leIr _ S x y). by rewrite finLattice_leE finLattice_meetE. Qed. -Lemma lefI L (S : {finLattice L}) : - {in S & &, forall x y z, (x <=_L \fmeet_S y z) = (x <=_L y) && (x <=_L z)}. +Lemma lefI (S : {finLattice T}) : + {in S & &, forall x y z, (x <= premeet S y z) = (x <= y) && (x <= z)}. Proof. -apply: sub_pred3 => x y z; move: (@rlexI _ S x y z). +apply: sub_pred3 => x y z; move: (@lexI _ S x y z). by rewrite !finLattice_leE finLattice_meetE. Qed. -Lemma fmeetC L (S : {finLattice L}) : {in S &, commutative (\fmeet_S)}. +Lemma fmeetC (S : {finLattice T}) : {in S &, commutative (premeet S)}. Proof. -apply: sub_pred2=> x y; move: (@rmeetC _ S x y). +apply: sub_pred2=> x y; move: (@meetC _ S x y). by move/(@congr1 _ _ (@fsval _ S)); rewrite !finLattice_meetE. Qed. -Lemma lefIl L (S : {finLattice L}) : - {in S & &, forall x y z, y <=_L x -> \fmeet_S y z <=_L x}. +Lemma lefIl (S : {finLattice T}) : + {in S & &, forall x y z, y <= x -> premeet S y z <= x}. Proof. -apply: sub_pred3 => x y z; move: (@rleIxl _ S x y z). +apply: sub_pred3 => x y z; move: (@leIxl _ S x y z). by rewrite !finLattice_leE !finLattice_meetE. Qed. -Lemma lefIr L (S : {finLattice L}) : - {in S & &, forall x y z, z <=_L x -> \fmeet_S y z <=_L x}. +Lemma lefIr (S : {finLattice T}) : + {in S & &, forall x y z, z <= x -> premeet S y z <= x}. Proof. move=> x y z xS yS zS zlex; rewrite fmeetC //; exact: lefIl. Qed. -Lemma fmeetA L (S : {finLattice L}) : {in S & &, associative (\fmeet_S) }. +Lemma fmeetA (S : {finLattice T}) : {in S & &, associative (premeet S) }. Proof. -apply: sub_pred3=> x y z; move:(@rmeetA _ S x y z). +apply: sub_pred3=> x y z; move:(@meetA _ S x y z). by move/(@congr1 _ _ (@fsval _ S)); rewrite !finLattice_meetE. Qed. -Lemma fmeetxx L (S : {finLattice L}) : {in S, idempotent (\fmeet_S)}. +Lemma fmeetxx (S : {finLattice T}) : {in S, idempotent (premeet S)}. Proof. -apply: sub_pred1=> x; move:(@rmeetxx _ S x). +apply: sub_pred1=> x; move:(@meetxx _ S x). by move/(@congr1 _ _ (@fsval _ S)); rewrite finLattice_meetE. Qed. -Lemma leEfmeet L (S : {finLattice L}) : - {in S &, forall x y, (x <=_L y) = (\fmeet_S x y == x)}. +Lemma leEfmeet (S : {finLattice T}) : + {in S &, forall x y, (x <= y) = (premeet S x y == x)}. Proof. -apply: sub_pred2 => x y; move:(@rleEmeet _ S x y). +apply: sub_pred2 => x y; move:(@leEmeet _ S x y). by rewrite finLattice_leE -val_eqE /= finLattice_meetE. Qed. -Lemma fmeetAC L (S : {finLattice L}) : - {in S & &, right_commutative (\fmeet_S)}. +Lemma fmeetAC (S : {finLattice T}) : + {in S & &, right_commutative (premeet S)}. Proof. -apply: sub_pred3=> x y z; move:(@rmeetAC _ S x y z). +apply: sub_pred3=> x y z; move:(@meetAC _ S x y z). by move/(@congr1 _ _ (@fsval _ S)); rewrite !finLattice_meetE. Qed. -Lemma fmeetCA L (S : {finLattice L}) : - {in S & &, left_commutative (\fmeet_S)}. +Lemma fmeetCA (S : {finLattice T}) : + {in S & &, left_commutative (premeet S)}. Proof. -apply: sub_pred3=> x y z; move:(@rmeetCA _ S x y z). +apply: sub_pred3=> x y z; move:(@meetCA _ S x y z). by move/(@congr1 _ _ (@fsval _ S)); rewrite !finLattice_meetE. Qed. - -Lemma fmeetACA L (S : {finLattice L}) x y z t: +Lemma fmeetACA (S : {finLattice T}) x y z t: x \in S -> y \in S -> z \in S -> t \in S -> - \fmeet_S (\fmeet_S x y) (\fmeet_S z t) = - \fmeet_S (\fmeet_S x z) (\fmeet_S y t). + premeet S (premeet S x y) (premeet S z t) = + premeet S (premeet S x z) (premeet S y t). Proof. -move=> xS yS zS tS; move:(@rmeetACA _ S [`xS] [`yS] [`zS] [`tS]). +move=> xS yS zS tS; move:(@meetACA _ S [`xS] [`yS] [`zS] [`tS]). by move/(@congr1 _ _ (@fsval _ S)); rewrite ?finLattice_meetE. Qed. -Lemma fmeetKI L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S x (\fmeet_S x y) = \fmeet_S x y}. +Lemma fmeetKI (S : {finLattice T}) : + {in S &, forall x y, premeet S x (premeet S x y) = premeet S x y}. Proof. by move=> x y xS yS; rewrite fmeetA ?fmeetxx. Qed. -Lemma fmeetIK L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S (\fmeet_S x y) y = \fmeet_S x y}. +Lemma fmeetIK (S : {finLattice T}) : + {in S &, forall x y, premeet S (premeet S x y) y = premeet S x y}. Proof. by move=> x y xS yS; rewrite -fmeetA ?fmeetxx. Qed. -Lemma fmeetKIC L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S x (\fmeet_S y x) = \fmeet_S x y}. +Lemma fmeetKIC (S : {finLattice T}) : + {in S &, forall x y, premeet S x (premeet S y x) = premeet S x y}. Proof. by move=> ? ? ? ?; rewrite fmeetC ?mem_fmeet ?fmeetIK // fmeetC. Qed. -Lemma fmeetIKC L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S (\fmeet_S y x) y = \fmeet_S x y}. +Lemma fmeetIKC (S : {finLattice T}) : + {in S &, forall x y, premeet S (premeet S y x) y = premeet S x y}. Proof. by move=> ? ? ? ?; rewrite fmeetC ?mem_fmeet ?fmeetKI // fmeetC. Qed. -Lemma leIf2 L (S : {finLattice L}) : - {in S & &, forall x y z, (y <=_L x) || (z <=_L x) -> - \fmeet_S y z <=_L x}. +Lemma leIf2 (S : {finLattice T}) : + {in S & &, forall x y z, (y <= x) || (z <= x) -> + premeet S y z <= x}. Proof. move=> x y z xS yS zS /orP [ylex | zlex]; [exact: lefIl | exact: lefIr]. Qed. - -Lemma fmeet_idPl L (S : {finLattice L}) {x y} : x \in S -> y \in S -> - reflect (\fmeet_S x y = x) (x <=_L y). +Lemma fmeet_idPl (S : {finLattice T}) {x y} : x \in S -> y \in S -> + reflect (premeet S x y = x) (x <= y). Proof. move=> xS yS; rewrite (leEfmeet xS yS) //; exact: eqP. Qed. -Lemma fmeet_idPr L (S : {finLattice L}) {x y} : x \in S -> y \in S -> - reflect (\fmeet_S y x = x) (x <=_L y). +Lemma fmeet_idPr (S : {finLattice T}) {x y} : x \in S -> y \in S -> + reflect (premeet S y x = x) (x <= y). Proof. by move=> xS yS; rewrite fmeetC //; apply/fmeet_idPl. Qed. -Lemma fmeet_l L (S : {finLattice L}) : - {in S &, forall x y, x <=_L y -> \fmeet_S x y = x}. +Lemma fmeet_l (S : {finLattice T}) : + {in S &, forall x y, x <= y -> premeet S x y = x}. Proof. move=> x y xS yS; exact/fmeet_idPl. Qed. -Lemma fmeet_r L (S : {finLattice L}) : - {in S &, forall x y, y <=_L x -> \fmeet_S x y = y}. +Lemma fmeet_r (S : {finLattice T}) : + {in S &, forall x y, y <= x -> premeet S x y = y}. Proof. move=> x y xS yS; exact/fmeet_idPr. Qed. -Lemma lefIidl L (S : {finLattice L}) : - {in S &, forall x y, (x <=_L \fmeet_S x y) = (x <=_L y)}. +Lemma lefIidl (S : {finLattice T}) : + {in S &, forall x y, (x <= premeet S x y) = (x <= y)}. Proof. by move=> x y xS yS; rewrite !(leEfmeet xS) ?mem_fmeet ?fmeetKI. Qed. -Lemma lefIidr L (S : {finLattice L}) : - {in S &, forall x y, (x <=_L \fmeet_S y x) = (x <=_L y)}. +Lemma lefIidr (S : {finLattice T}) : + {in S &, forall x y, (x <= premeet S y x) = (x <= y)}. Proof. by move=> x y xS yS; rewrite !(leEfmeet xS) ?mem_fmeet ?fmeetKIC. Qed. -Lemma eq_fmeetl L (S : {finLattice L}) : - {in S &, forall x y, (\fmeet_S x y == x) = (x <=_L y)}. +Lemma eq_fmeetl (S : {finLattice T}) : + {in S &, forall x y, (premeet S x y == x) = (x <= y)}. Proof. by move=> ????; apply/esym/leEfmeet. Qed. -Lemma eq_fmeetr L (S: {finLattice L}) : - {in S &, forall x y, (\fmeet_S x y == y) = (y <=_L x)}. +Lemma eq_fmeetr (S: {finLattice T}) : + {in S &, forall x y, (premeet S x y == y) = (y <= x)}. Proof. by move=> ????; rewrite fmeetC ?eq_fmeetl. Qed. -Lemma lefI2 L (S : {finLattice L}) x y z t : +Lemma lefI2 (S : {finLattice T}) x y z t : x \in S -> y \in S -> z \in S -> t \in S -> - x <=_L z -> y <=_L t -> \fmeet_S x y <=_L \fmeet_S z t. + x <= z -> y <= t -> premeet S x y <= premeet S z t. Proof. -move=> xS yS zS tS; move:(@rleI2 _ S [`xS] [`yS] [`zS] [`tS]). +move=> xS yS zS tS; move:(@leI2 _ S [`xS] [`yS] [`zS] [`tS]). by rewrite !finLattice_leE !finLattice_meetE. Qed. @@ -917,157 +891,168 @@ End FMeetTheory. (* -------------------------------------------------------------------- *) Section FJoinTheory. -Lemma fjoinC L (S : {finLattice L}) : {in S &, commutative (\fjoin_S)}. -Proof. exact: (@fmeetC _ S^~s). Qed. +Context {disp : Order.disp_t} {T : prelatticeType disp}. + +Lemma fjoinC (S : {finLattice T}) : {in S &, commutative (prejoin S)}. +Proof. exact: (@fmeetC _ _ S^fd). Qed. -Lemma lefUr L (S: {finLattice L}) : {in S &, forall x y, x <=_L \fjoin_S y x}. -Proof. exact: (@leIfr _ S^~s). Qed. +Lemma lefUr (S: {finLattice T}) : {in S &, forall x y, x <= prejoin S y x}. +Proof. exact: (@leIfr _ _ S^fd). Qed. -Lemma lefUl L (S : {finLattice L}) : {in S &, forall x y, x <=_L \fjoin_S x y}. -Proof. exact: (@leIfl _ S^~s). Qed. +Lemma lefUl (S : {finLattice T}) : {in S &, forall x y, x <= prejoin S x y}. +Proof. exact: (@leIfl _ _ S^fd). Qed. -Lemma leUf L (S : {finLattice L}) : {in S & &, forall x y z, - (\fjoin_S y z <=_L x) = (y <=_L x) && (z <=_L x)}. -Proof. exact: (@lefI _ S^~s). Qed. +Lemma leUf (S : {finLattice T}) : {in S & &, forall x y z, + (prejoin S y z <= x) = (y <= x) && (z <= x)}. +Proof. exact: (@lefI _ _ S^fd). Qed. -Lemma fjoinA L (S : {finLattice L}) : {in S & &, associative (\fjoin_S)}. -Proof. exact: (@fmeetA _ S^~s). Qed. +Lemma fjoinA (S : {finLattice T}) : {in S & &, associative (prejoin S)}. +Proof. exact: (@fmeetA _ _ S^fd). Qed. -Lemma fjoinxx L (S : {finLattice L}) : {in S, idempotent (\fjoin_S)}. -Proof. exact: (@fmeetxx _ S^~s). Qed. +Lemma fjoinxx (S : {finLattice T}) : {in S, idempotent (prejoin S)}. +Proof. exact: (@fmeetxx _ _ S^fd). Qed. -Lemma leEfjoin L (S : {finLattice L}) : - {in S &, forall x y, (x <=_L y) = (\fjoin_S y x == y)}. +Lemma leEfjoin (S : {finLattice T}) : + {in S &, forall x y, (x <= y) = (prejoin S y x == y)}. Proof. -move=> ????; exact: (@leEfmeet _ S^~s). +move=> ????; exact: (@leEfmeet _ _ S^fd). Qed. -Lemma fjoinAC L (S : {finLattice L}) : - {in S & &, right_commutative (\fjoin_S)}. -Proof. exact: (@fmeetAC _ S^~s). Qed. +Lemma fjoinAC (S : {finLattice T}) : + {in S & &, right_commutative (prejoin S)}. +Proof. exact: (@fmeetAC _ _ S^fd). Qed. -Lemma fjoinCA L (S : {finLattice L}) : - {in S & &, left_commutative (\fjoin_S)}. -Proof. exact: (@fmeetCA _ S^~s). Qed. +Lemma fjoinCA (S : {finLattice T}) : + {in S & &, left_commutative (prejoin S)}. +Proof. exact: (@fmeetCA _ _ S^fd). Qed. -Lemma fjoinACA L (S : {finLattice L}) x y z t : +Lemma fjoinACA (S : {finLattice T}) x y z t : x \in S -> y \in S -> z \in S -> t \in S -> - \fjoin_S (\fjoin_S x y) (\fjoin_S z t) = - \fjoin_S (\fjoin_S x z) (\fjoin_S y t). -Proof. exact: (@fmeetACA _ S^~s). Qed. + prejoin S (prejoin S x y) (prejoin S z t) = + prejoin S (prejoin S x z) (prejoin S y t). +Proof. exact: (@fmeetACA _ _ S^fd). Qed. -Lemma fjoinKU L (S: {finLattice L}) : - {in S &, forall x y, \fjoin_S x (\fjoin_S x y) = \fjoin_S x y}. -Proof. exact: (@fmeetKI _ S^~s). Qed. +Lemma fjoinKU (S: {finLattice T}) : + {in S &, forall x y, prejoin S x (prejoin S x y) = prejoin S x y}. +Proof. exact: (@fmeetKI _ _ S^fd). Qed. -Lemma fjoinUK L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S (\fjoin_S x y) y = \fjoin_S x y}. -Proof. exact: (@fmeetIK _ S^~s). Qed. +Lemma fjoinUK (S : {finLattice T}) : + {in S &, forall x y, prejoin S (prejoin S x y) y = prejoin S x y}. +Proof. exact: (@fmeetIK _ _ S^fd). Qed. -Lemma fjoinKUC L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S x (\fjoin_S y x) = \fjoin_S x y}. -Proof. exact: (@fmeetKIC _ S^~s). Qed. +Lemma fjoinKUC (S : {finLattice T}) : + {in S &, forall x y, prejoin S x (prejoin S y x) = prejoin S x y}. +Proof. exact: (@fmeetKIC _ _ S^fd). Qed. -Lemma fjoinUKC L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S (\fjoin_S y x) y = \fjoin_S x y}. -Proof. exact: (@fmeetIKC _ S^~s). Qed. +Lemma fjoinUKC (S : {finLattice T}) : + {in S &, forall x y, prejoin S (prejoin S y x) y = prejoin S x y}. +Proof. exact: (@fmeetIKC _ _ S^fd). Qed. -Lemma leUfl L (S: {finLattice L}) : - {in S & &, forall x y z, x <=_L y -> x <=_L \fjoin_S y z}. -Proof. exact: (@lefIl _ S^~s). Qed. +Lemma leUfl (S: {finLattice T}) : + {in S & &, forall x y z, x <= y -> x <= prejoin S y z}. +Proof. exact: (@lefIl _ _ S^fd). Qed. -Lemma leUfr L (S : {finLattice L}) : - {in S & &, forall x y z, x <=_L z -> x <=_L \fjoin_S y z}. -Proof. exact: (@lefIr _ S^~s). Qed. +Lemma leUfr (S : {finLattice T}) : + {in S & &, forall x y z, x <= z -> x <= prejoin S y z}. +Proof. exact: (@lefIr _ _ S^fd). Qed. -Lemma lefU2 L (S : {finLattice L}) : - {in S & &, forall x y z, (x <=_L y) || (x <=_L z) -> - x <=_L \fjoin_S y z}. -Proof. exact: (@leIf2 _ S^~s). Qed. +Lemma lefU2 (S : {finLattice T}) : + {in S & &, forall x y z, (x <= y) || (x <= z) -> + x <= prejoin S y z}. +Proof. exact: (@leIf2 _ _ S^fd). Qed. -Lemma fjoin_idPr L (S : {finLattice L}) {x y}: x \in S -> y \in S -> - reflect (\fjoin_S y x = x) (y <=_L x). -Proof. exact: (@fmeet_idPr _ S^~s). Qed. +Lemma fjoin_idPr (S : {finLattice T}) {x y}: x \in S -> y \in S -> + reflect (prejoin S y x = x) (y <= x). +Proof. exact: (@fmeet_idPr _ _ S^fd). Qed. -Lemma fjoin_idPl L (S: {finLattice L}) {x y} : x \in S -> y \in S -> - reflect (\fjoin_S x y = x) (y <=_L x). -Proof. exact: (@fmeet_idPl _ S^~s). Qed. +Lemma fjoin_idPl (S: {finLattice T}) {x y} : x \in S -> y \in S -> + reflect (prejoin S x y = x) (y <= x). +Proof. exact: (@fmeet_idPl _ _ S^fd). Qed. -Lemma fjoin_l L (S : {finLattice L}) : - {in S &, forall x y, y <=_L x -> \fjoin_S x y = x}. -Proof. exact: (@fmeet_l _ S^~s). Qed. +Lemma fjoin_l (S : {finLattice T}) : + {in S &, forall x y, y <= x -> prejoin S x y = x}. +Proof. exact: (@fmeet_l _ _ S^fd). Qed. -Lemma fjoin_r L (S : {finLattice L}) : - {in S &, forall x y, x <=_L y -> \fjoin_S x y = y}. -Proof. exact: (@fmeet_r _ S^~s). Qed. +Lemma fjoin_r (S : {finLattice T}) : + {in S &, forall x y, x <= y -> prejoin S x y = y}. +Proof. exact: (@fmeet_r _ _ S^fd). Qed. -Lemma leUfidl L (S: {finLattice L}) : - {in S &, forall x y, (\fjoin_S x y <=_L x) = (y <=_L x)}. -Proof. exact: (@lefIidl _ S^~s). Qed. +Lemma leUfidl (S: {finLattice T}) : + {in S &, forall x y, (prejoin S x y <= x) = (y <= x)}. +Proof. exact: (@lefIidl _ _ S^fd). Qed. -Lemma leUfidr L (S : {finLattice L}) : - {in S &, forall x y, (\fjoin_S y x <=_L x) = (y <=_L x)}. -Proof. exact: (@lefIidr _ S^~s). Qed. +Lemma leUfidr (S : {finLattice T}) : + {in S &, forall x y, (prejoin S y x <= x) = (y <= x)}. +Proof. exact: (@lefIidr _ _ S^fd). Qed. -Lemma eq_fjoinl L (S : {finLattice L}) : - {in S &, forall x y, (\fjoin_S x y == x) = (y <=_L x)}. -Proof. exact: (@eq_fmeetl _ S^~s). Qed. +Lemma eq_fjoinl (S : {finLattice T}) : + {in S &, forall x y, (prejoin S x y == x) = (y <= x)}. +Proof. exact: (@eq_fmeetl _ _ S^fd). Qed. -Lemma eq_fjoinr L (S : {finLattice L}) : - {in S &, forall x y, (\fjoin_S x y == y) = (x <=_L y)}. -Proof. exact: (@eq_fmeetr _ S^~s). Qed. +Lemma eq_fjoinr (S : {finLattice T}) : + {in S &, forall x y, (prejoin S x y == y) = (x <= y)}. +Proof. exact: (@eq_fmeetr _ _ S^fd). Qed. -Lemma leUf2 L (S: {finLattice L}) x y z t : +Lemma leUf2 (S: {finLattice T}) x y z t : x \in S -> y \in S -> z \in S -> t \in S -> - x <=_L z -> y <=_L t -> \fjoin_S x y <=_L \fjoin_S z t. + x <= z -> y <= t -> prejoin S x y <= prejoin S z t. Proof. -move=> ????; exact: (@lefI2 _ S^~s). +move=> ????; exact: (@lefI2 _ _ S^fd). Qed. End FJoinTheory. Section FMeetJoinTheory. -Lemma fmeetUK L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S (\fmeet_S x y) y = y}. +Section FMeet. +Context {disp : Order.disp_t} {T : prelatticeType disp}. + +Lemma fmeetUK (S : {finLattice T}) : + {in S &, forall x y, prejoin S (premeet S x y) y = y}. Proof. by move=> x y xS yS; apply/eqP; rewrite eq_fjoinr ?leIfr ?mem_fmeet. Qed. -Lemma fmeetUKC L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S (\fmeet_S y x) y = y}. +Lemma fmeetUKC (S : {finLattice T}) : + {in S &, forall x y, prejoin S (premeet S y x) y = y}. Proof. by move=> ????; rewrite fmeetC ?fmeetUK. Qed. -Lemma fmeetKUC L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S x (\fmeet_S y x) = x}. +Lemma fmeetKUC (S : {finLattice T}) : + {in S &, forall x y, prejoin S x (premeet S y x) = x}. Proof. by move=> ????; rewrite fjoinC ?fmeetUK ?mem_fmeet. Qed. -Lemma fmeetKU L (S : {finLattice L}) : - {in S &, forall x y, \fjoin_S x (\fmeet_S x y) = x}. +Lemma fmeetKU (S : {finLattice T}) : + {in S &, forall x y, prejoin S x (premeet S x y) = x}. Proof. by move=> ????; rewrite fmeetC ?fmeetKUC. Qed. -Lemma fjoinIK L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S (\fjoin_S x y) y = y}. -Proof. exact: (@fmeetUK _ S^~s). Qed. +End FMeet. + +Section FJoin. +Context {disp : Order.disp_t} {T : prelatticeType disp}. + +Lemma fjoinIK (S : {finLattice T}) : + {in S &, forall x y, premeet S (prejoin S x y) y = y}. +Proof. exact: (@fmeetUK _ _ S^fd). Qed. -Lemma fjoinIKC L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S (\fjoin_S y x) y = y}. -Proof. exact: (@fmeetUKC _ S^~s). Qed. +Lemma fjoinIKC (S : {finLattice T}) : + {in S &, forall x y, premeet S (prejoin S y x) y = y}. +Proof. exact: (@fmeetUKC _ _ S^fd). Qed. -Lemma fjoinKIC L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S x (\fjoin_S y x) = x}. -Proof. exact: (@fmeetKUC _ S^~s). Qed. +Lemma fjoinKIC (S : {finLattice T}) : + {in S &, forall x y, premeet S x (prejoin S y x) = x}. +Proof. exact: (@fmeetKUC _ _ S^fd). Qed. -Lemma fjoinKI L (S : {finLattice L}) : - {in S &, forall x y, \fmeet_S x (\fjoin_S x y) = x}. -Proof. exact: (@fmeetKU _ S^~s). Qed. +Lemma fjoinKI (S : {finLattice T}) : + {in S &, forall x y, premeet S x (prejoin S x y) = x}. +Proof. exact: (@fmeetKU _ _ S^fd). Qed. +End FJoin. End FMeetJoinTheory. (*Section FBigTheory. -Lemma mem_bigfmeet L (S: {finLattice L}) +Lemma mem_bigfmeet (S: {finLattice L}) (r : seq T) (P : pred T) (F : T -> T) x : x \in r -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> - \big[\fmeet_S / x]_(i <- r | P i) F i \in S. + \big[premeet S / x]_(i <- r | P i) F i \in S. Proof. move=> xr FS rS; rewrite big_seq_cond; apply: (big_ind (fun x => x \in S)). - exact: rS. @@ -1075,57 +1060,57 @@ move=> xr FS rS; rewrite big_seq_cond; apply: (big_ind (fun x => x \in S)). - by move=> i /andP [/rS /FS]. Qed. -Lemma mem_bigfjoin L (S: {finLattice L}) +Lemma mem_bigfjoin (S: {finLattice L}) (r : seq T) (P : pred T) (F : T -> T) x : x \in r -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> - \big[\fjoin_S / x]_(i <- r | P i) F i \in S. + \big[prejoin S / x]_(i <- r | P i) F i \in S. Proof. -exact: (@mem_bigfmeet _ S^~s). +exact: (@mem_bigfmeet _ S^fd). Qed. (* TODO : new lemma names *) -Lemma fmeet_inf_seq_idx L (S : {finLattice L}) +Lemma fmeet_inf_seq_idx (S : {finLattice L}) (r : seq T) (P : {pred T}) (F : T -> T) x : x \in r -> P x -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> - \big[\fmeet_S / F x]_(i <- r | P i) F i <=_L F x. + \big[premeet S / F x]_(i <- r | P i) F i <=_L F x. Proof. move=> xr Px FS rS. -suff: (\big[\fmeet_S / F x]_(i <- r | P i) F i <=_L F x) && -(\big[\fmeet_S / F x]_(i <- r | P i) F i \in S) by case/andP. +suff: (\big[premeet S / F x]_(i <- r | P i) F i <=_L F x) && +(\big[premeet S / F x]_(i <- r | P i) F i \in S) by case/andP. rewrite big_seq_cond; apply: (big_rec (fun y => (y <=_L F x) && (y \in S))). - by rewrite lexx FS ?rS. - move=> a b /andP [/rS aS _] /andP [bleFx bS]. by rewrite lefIr ?mem_fmeet ?FS // rS. Qed. -Lemma fmeet_max_seq L (S : {finLattice L}) +Lemma fmeet_max_seq (S : {finLattice L}) (r : seq T) (P : {pred T}) (F : T -> T) x u: x \in r -> P x -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> F x <=_L u -> u \in S -> - \big[\fmeet_S / F x]_(i <- r | P i) F i <=_L u. + \big[premeet S / F x]_(i <- r | P i) F i <=_L u. Proof. move=> xr Px FS rS Fxleu uS. -suff: (\big[\fmeet_S / F x]_(i <- r | P i) F i <=_L u) && -(\big[\fmeet_S / F x]_(i <- r | P i) F i \in S) by case/andP. +suff: (\big[premeet S / F x]_(i <- r | P i) F i <=_L u) && +(\big[premeet S / F x]_(i <- r | P i) F i \in S) by case/andP. rewrite big_seq_cond; apply: (big_rec (fun y => (y <=_L u) && (y \in S))). - by rewrite Fxleu FS ?rS. - move=> a b /andP [/rS aS _] /andP [bleFx bS]. by rewrite lefIr ?mem_fmeet ?FS //. Qed. -Lemma fjoin_sumeet_seq L (S : {finLattice L}) +Lemma fjoin_sumeet_seq (S : {finLattice L}) (r : seq T) (P : {pred T}) (F : T -> T) x : x \in r -> P x -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> - \big[\fjoin_S / F x]_(i <- r | P i) F i >=_L F x. -Proof. exact : (@fmeet_inf_seq _ S^~s). Qed. + \big[prejoin S / F x]_(i <- r | P i) F i >=_L F x. +Proof. exact : (@fmeet_inf_seq _ S^fd). Qed. -Lemma fjoin_min_seq L (S : {finLattice L}) +Lemma fjoin_min_seq (S : {finLattice L}) (r : seq T) (P : {pred T}) (F : T -> T) x u: x \in r -> P x -> {in S, forall y, F y \in S} -> {in r, forall y, y \in S} -> F x >=_L u -> u \in S -> - \big[\fjoin_S / F x]_(i <- r | P i) F i >=_L u. -Proof. exact: (@fmeet_max_seq _ S^~s). Qed. + \big[prejoin S / F x]_(i <- r | P i) F i >=_L u. +Proof. exact: (@fmeet_max_seq _ S^fd). Qed. End FBigTheory.*) @@ -1134,9 +1119,11 @@ End FinLatticeTheory. (* -------------------------------------------------------------------- *) Section TBDefs. -Context {T: choiceType}. -Implicit Type L : {preLattice T}. +Section FPick. +Context {T : choiceType}. + +(* TODO: move it *) Definition fpick (S : {fset T}) := omap val (@pick [finType of S] xpredT). @@ -1158,57 +1145,62 @@ Lemma fpickS (S : {fset T}) : S != fset0 -> exists2 x0, x0 \in S & fpick S = Some x0. Proof. by case: fpickP => [->|] // x0 x0_in_S _; exists x0. Qed. -Definition fbot L (S : {finLattice L}) := +End FPick. + +Definition fbot {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}) : T := if fpick S is Some x0 then - \big[\fmeet_S/x0]_(x <- S) x + \big[premeet S/x0]_(x <- S) x else - PreLattice.witness L. + witness. -Definition ftop L (S : {finLattice L}) := fbot (S^~s). +Definition ftop {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}) : T := + if fpick S is Some x0 then + \big[prejoin S/x0]_(x <- S) x + else + witness. End TBDefs. -Notation "\fbot_ S" := (fbot S) (at level 2, S at next level, format "\fbot_ S"). -Notation "\ftop_ S" := (ftop S) (at level 2, S at next level, format "\ftop_ S"). +Notation "\fbot_ S" := (@fbot _ _ S) (at level 2, S at next level, format "\fbot_ S"). +Notation "\ftop_ S" := (@ftop _ _ S) (at level 2, S at next level, format "\ftop_ S"). Section TBFinLatticeTheory. -Context {T: choiceType}. -Implicit Type L : {preLattice T}. +Implicit Type (disp : Order.disp_t). -Lemma fbot_def L (S : {finLattice L}) x0 : - x0 \in S -> \fbot_S = \big[\fmeet_S/x0]_(x <- S) x. +Lemma fbot_def {disp} {T : prelatticeType disp} (S : {finLattice T}) x0 : + x0 \in S -> \fbot_S = \big[premeet S/x0]_(x <- S) x. Proof. rewrite inE /fbot; case: fpickP => [->//|y0 y0_in_S x0_in_S]. rewrite big_seq [RHS]big_seq; apply: (big_idxx (Q := mem S)) => //; [exact: fmeetC| exact: fmeetA| exact: mem_fmeet| exact: fmeetxx]. Qed. -Lemma ftop_def L (S : {finLattice L}) x0 : - x0 \in S -> \ftop_S = \big[\fjoin_S/x0]_(x <- S) x. -Proof. exact: (@fbot_def _ S^~s). Qed. +Lemma ftop_def {disp} {T : prelatticeType disp} (S : {finLattice T}) x0 : + x0 \in S -> \ftop_S = \big[prejoin S/x0]_(x <- S) x. +Proof. exact: (@fbot_def _ _ S^fd). Qed. -Lemma mem_fbot L (S : {finLattice L}) : \fbot_S \in S. +Lemma mem_fbot {disp} {T : prelatticeType disp} (S : {finLattice T}) : \fbot_S \in S. Proof. case/fset0Pn: (finLattice_prop0 S) => x0 x0S. rewrite (fbot_def x0S) big_seq. by apply/big_stable => //; apply/mem_fmeet. Qed. -Lemma mem_ftop L (S : {finLattice L}) : \ftop_S \in S. -Proof. exact: (@mem_fbot _ S^~s). Qed. +Lemma mem_ftop {disp} {T : prelatticeType disp} (S : {finLattice T}) : \ftop_S \in S. +Proof. exact: (@mem_fbot _ _ S^fd). Qed. -Lemma fbotE L (S: {finLattice L}) : - \fbot_S = \big[\fmeet_S / \ftop_S]_(i <- S) i. +Lemma fbotE {disp} {T : prelatticeType disp} (S: {finLattice T}) : + \fbot_S = \big[premeet S / \ftop_S]_(i <- S) i. Proof. by rewrite (fbot_def (mem_ftop S)). Qed. -Lemma ftopE L (S: {finLattice L}) : - \ftop_S = \big[\fjoin_S / \fbot_S]_(i <- S) i. -Proof. exact: (@fbotE _ S^~s). Qed. +Lemma ftopE {disp} {T : prelatticeType disp} (S: {finLattice T}) : + \ftop_S = \big[prejoin S / \fbot_S]_(i <- S) i. +Proof. exact: (@fbotE _ _ S^fd). Qed. (* ----------------------------------------------------------------- *) -Lemma le0f L (S : {finLattice L}) : {in S, forall x, \fbot_S <=_L x}. +Lemma le0f {disp} {T : prelatticeType disp} (S : {finLattice T}) : {in S, forall x, \fbot_S <= x}. Proof. move => x xS; rewrite (fbot_def xS) big_seq. rewrite (big_mem_sub _ _ _ _ xS xS) ?leIfl //. (* TODO: FIX IT *) @@ -1218,64 +1210,64 @@ apply/big_stable => //; apply/mem_fmeet. - exact: mem_fmeet. Qed. -Lemma fjoinf0 L (S : {finLattice L}) : {in S, right_id \fbot_S (\fjoin_S)}. +Lemma fjoinf0 {disp} {T : prelatticeType disp} (S : {finLattice T}) : {in S, right_id \fbot_S (prejoin S)}. Proof. by move=> x xS; apply/eqP; rewrite eq_fjoinl ?le0f ?mem_fbot. Qed. -Lemma fjoin0f L (S : {finLattice L}): {in S, left_id \fbot_S (\fjoin_S)}. +Lemma fjoin0f {disp} {T : prelatticeType disp} (S : {finLattice T}): {in S, left_id \fbot_S (prejoin S)}. Proof. by move=> x xS; apply/eqP; rewrite eq_fjoinr ?le0f ?mem_fbot. Qed. -Lemma lef1 L (S : {finLattice L}) : {in S, forall x, x <=_L \ftop_S}. -Proof. move=> ??; exact: (@le0f _ S^~s). Qed. +Lemma lef1 {disp} {T : prelatticeType disp} (S : {finLattice T}) : {in S, forall x, x <= \ftop_S}. +Proof. move=> ??; exact: (@le0f _ _ S^fd). Qed. -Lemma fmeetf1 L (S : {finLattice L}) : {in S, right_id \ftop_S (\fmeet_S)}. -Proof. exact: (@fjoinf0 _ S^~s). Qed. +Lemma fmeetf1 {disp} {T : prelatticeType disp} (S : {finLattice T}) : {in S, right_id \ftop_S (premeet S)}. +Proof. exact: (@fjoinf0 _ _ S^fd). Qed. -Lemma fmeet1f L (S : {finLattice L}) : {in S, left_id \ftop_S (\fmeet_S)}. -Proof. exact: (@fjoin0f _ S^~s). Qed. +Lemma fmeet1f {disp} {T : prelatticeType disp} (S : {finLattice T}) : {in S, left_id \ftop_S (premeet S)}. +Proof. exact: (@fjoin0f _ _ S^fd). Qed. -Lemma ltf1 L (S : {finLattice L}) : - {in S, forall x, (x <_L \ftop_S) = (x != \ftop_S)}. -Proof. by move=> x xS; rewrite rlt_neqAle ?lef1 ?andbT. Qed. +Lemma ltf1 {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, forall x, (x < \ftop_S) = (x != \ftop_S)}. +Proof. by move=> x xS; rewrite lt_neqAle ?lef1 ?andbT. Qed. -Lemma lt0f L (S : {finLattice L}) : - {in S, forall x, (\fbot_S <_L x) = (x != \fbot_S)}. -Proof. by move=> x xS; rewrite rlt_def ?le0f ?andbT // eq_sym. Qed. +Lemma lt0f {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, forall x, (\fbot_S < x) = (x != \fbot_S)}. +Proof. by move=> x xS; rewrite lt_def ?le0f ?andbT // eq_sym. Qed. -Lemma ftop_id L (S: {finLattice L}) : - {in S, forall t, (forall x, x \in S -> x <=_L t) -> \ftop_S = t}. +Lemma ftop_id {disp} {T : prelatticeType disp} (S: {finLattice T}) : + {in S, forall t, (forall x, x \in S -> x <= t) -> \ftop_S = t}. Proof. -move=> t tS ttop; apply/(@rle_anti _ L). +move=> t tS ttop; apply/le_anti. by rewrite lef1 //= andbT; apply/ttop; rewrite mem_ftop. Qed. -Lemma fbot_id L (S: {finLattice L}) : - {in S, forall t, (forall x, x \in S -> x >=_L t) -> \fbot_S = t}. -Proof. exact: (@ftop_id _ S^~s). Qed. +Lemma fbot_id {disp} {T : prelatticeType disp} (S: {finLattice T}) : + {in S, forall t, (forall x, x \in S -> x >= t) -> \fbot_S = t}. +Proof. exact: (@ftop_id _ _ S^fd). Qed. -Lemma fmeet0f L (S : {finLattice L}) : - {in S, left_zero \fbot_S \fmeet_S}. +Lemma fmeet0f {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, left_zero \fbot_S (premeet S)}. Proof. by move=> x xS; apply/eqP; rewrite -leEfmeet ?le0f ?mem_fbot. Qed. -Lemma fmeetf0 L (S : {finLattice L}) : - {in S, right_zero \fbot_S \fmeet_S}. +Lemma fmeetf0 {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, right_zero \fbot_S (premeet S)}. Proof. by move=> x xS; apply/eqP; rewrite fmeetC -?leEfmeet ?le0f ?mem_fbot. Qed. -Lemma fjoin1f L (S : {finLattice L}) : - {in S, left_zero \ftop_S \fjoin_S}. -Proof. exact: (@fmeet0f _ S^~s). Qed. +Lemma fjoin1f {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, left_zero \ftop_S (prejoin S)}. +Proof. exact: (@fmeet0f _ _ S^fd). Qed. -Lemma fjoinf1 L (S : {finLattice L}) : - {in S, right_zero \ftop_S \fjoin_S}. -Proof. exact: (@fmeetf0 _ S^~s). Qed. +Lemma fjoinf1 {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S, right_zero \ftop_S (prejoin S)}. +Proof. exact: (@fmeetf0 _ _ S^fd). Qed. (* ------------------------------------------------------------------ *) Section BigOpFinLattice. -Lemma mem_bigfmeet L (S: {finLattice L}) +Lemma mem_bigfmeet {disp : Order.disp_t} {T : prelatticeType disp} (S: {finLattice T}) (r : seq T) (P : pred T) (F : T -> T): {in S, forall y, F y \in S} -> {subset r <= S} -> - \big[\fmeet_S / \ftop_S]_(i <- r | P i) F i \in S. + \big[premeet S / \ftop_S]_(i <- r | P i) F i \in S. Proof. move=> FS rS; rewrite big_seq_cond; apply: (big_ind (fun x => x \in S)). - exact: mem_ftop. @@ -1283,16 +1275,16 @@ move=> FS rS; rewrite big_seq_cond; apply: (big_ind (fun x => x \in S)). - by move=> i /andP [/rS /FS]. Qed. -Lemma mem_bigfjoin L (S: {finLattice L}) +Lemma mem_bigfjoin {disp} {T : prelatticeType disp} (S: {finLattice T}) (r : seq T) (P : pred T) (F : T -> T): {in S, forall y, F y \in S} -> {subset r <= S} -> - \big[\fjoin_S / \fbot_S]_(i <- r | P i) F i \in S. -Proof. exact: (@mem_bigfmeet _ S^~s). Qed. + \big[prejoin S / \fbot_S]_(i <- r | P i) F i \in S. +Proof. exact: (@mem_bigfmeet _ _ S^fd). Qed. -Lemma fmeet_inf_seq L (S: {finLattice L}) +Lemma fmeet_inf_seq {disp} {T : prelatticeType disp} (S: {finLattice T}) (r: seq T) (P : pred T) (F : T -> T) x : {subset r <= S} -> {in S, forall y, F y \in S} -> x \in r -> P x -> - \big[\fmeet_S / \ftop_S]_(i <- r | P i) F i <=_L F x. + \big[premeet S / \ftop_S]_(i <- r | P i) F i <= F x. Proof. move=> rS FS xr Px; rewrite big_map_fun. have FxS: F x \in [seq F j | j <- r & P j] by @@ -1300,42 +1292,40 @@ have FxS: F x \in [seq F j | j <- r & P j] by rewrite big_seq. have filtS: forall i, i \in [seq F j | j <- r & P j] -> i \in S by move=> i /mapP [j]; rewrite mem_filter => /andP [_ jS] ->; exact/FS/rS. -rewrite (big_mem_sub _ _ _ filtS _ FxS) ?lefIl ?(filtS _ FxS) - ?(big_stable _ filtS) ?mem_ftop //. +rewrite (big_mem_sub _ _ _ filtS _ FxS) ?lefIl + ?(@big_stable _ _ _ _ _ filtS) ?mem_ftop ?mem_fmeet ?FS ?rS //. (* TODO: UGLY *) - exact: mem_fmeet. - exact: fmeetC. - exact: fmeetA. - exact: mem_fmeet. Qed. -Lemma fjoin_sumeet_seq L (S: {finLattice L}) +Lemma fjoin_sumeet_seq {disp} {T : prelatticeType disp} (S: {finLattice T}) (r : seq T) (P : pred T) (F : T -> T) x : {subset r <= S} -> {in S, forall y, F y \in S} -> x \in r -> P x -> - F x <=_L \big[\fjoin_S / \fbot_S]_(i <- r | P i) F i. -Proof. exact: (@fmeet_inf_seq _ S^~s). Qed. - -Lemma fmeetsP L (S : {finLattice L}) (P : pred T) (F : T -> T) x : - {in S, forall y, P y -> x <=_L F y} -> x <=_L \big[\fmeet_S / \ftop_S]_(y <- S | P y) F y. -Admitted. + F x <= \big[prejoin S / \fbot_S]_(i <- r | P i) F i. +Proof. exact: (@fmeet_inf_seq _ _ S^fd). Qed. -Lemma fjoin_meets L (S: {finLattice L}) x y : +Lemma fjoin_meets {disp} {T : prelatticeType disp} (S: {finLattice T}) x y : x \in S -> y \in S -> - \fjoin_S x y = \big[\fmeet_S / \ftop_S]_(i <- S | (x <=_L i) && (y <=_L i)) i. + prejoin S x y = \big[premeet S / \ftop_S]_(i <- S | (x <= i) && (y <= i)) i. Proof. -move=> xS yS; apply/(@rle_anti _ L)/andP; split; last first. +move=> xS yS; apply/le_anti/andP; split; last first. - apply/fmeet_inf_seq; rewrite ?mem_fjoin //. by apply/andP; split; rewrite ?lefUl ?lefUr. -- by apply/fmeetsP=> ???; rewrite leUf. +- set B := BigOp.bigop _ _ _. + suff: (B \in S) /\ (prejoin S x y <= B) by case. + rewrite /B big_seq_cond; apply big_rec. + + split; [exact: mem_ftop|exact/lef1/mem_fjoin]. + + move=> i j /and3P [iS xi yi] [jS j1]. + split; [exact/mem_fmeet|apply/premeet_inf=> //; first exact:mem_fjoin]. + exact/prejoin_sumeet. Qed. -Lemma fjoinsP L (S : {finLattice L}) (P : pred T) (F : T -> T) x : - {in S, forall y, P y -> F y <=_L x} -> \big[\fjoin_S / \fbot_S]_(y <- S | P y) F y <=_L x. -Proof. exact: (@fmeetsP _ S^~s). Qed. - -Lemma fmeet_joins L (S: {finLattice L}) x y : +Lemma fmeet_joins {disp} {T : prelatticeType disp} (S: {finLattice T}) x y : x \in S -> y \in S -> - \fmeet_S x y = \big[\fjoin_S / \fbot_S]_(i <- S | (x >=_L i) && (y >=_L i)) i. -Proof. exact: (@fjoin_meets _ S^~s). Qed. + premeet S x y = \big[prejoin S / \fbot_S]_(i <- S | (x >= i) && (y >= i)) i. +Proof. exact: (@fjoin_meets _ _ S^fd). Qed. End BigOpFinLattice. End TBFinLatticeTheory. @@ -1343,45 +1333,68 @@ End TBFinLatticeTheory. Module FinTBLatticeStructure. Section FinTBLatticeStructure. -Context {T: choiceType} (L : {preLattice T}) (S : {finLattice L}) (x0 : S). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}) (x0 : S). Definition finbot := [`mem_fbot S]. -Lemma finbot_mixin : BPOrder.mixin_of S finbot. +Lemma finle0x : forall x, finbot <= x. Proof. move=> x; exact/le0f/fsvalP. Qed. +Definition finBottomMixin := BottomMixin finle0x. + Definition fintop := [`mem_ftop S]. -Lemma fintop_mixin : TPOrder.mixin_of S fintop. +Lemma finlex1 : forall x, x <= fintop. Proof. move=> x; exact/lef1/fsvalP. Qed. -Local Canonical bPOrder := BPOrder finle finlt finbot finbot_mixin. - -Local Canonical tPOrder := TPOrder finle finlt fintop fintop_mixin. - -Local Canonical bMeetOrder := [bMeetOrder of finle]. -Local Canonical tMeetOrder := [tMeetOrder of finle]. -Local Canonical tbMeetOrder := [tMeetOrder of finle]. -Local Canonical bJoinOrder := [bJoinOrder of finle]. -Local Canonical tJoinOrder := [tJoinOrder of finle]. -Local Canonical tbJoinOrder := [tbJoinOrder of finle]. -Local Canonical bLattice := [bLattice of finle]. -Local Canonical tLattice := [tLattice of finle]. -Local Canonical tbLattice := [tbLattice of finle]. -(* TODO : are canonical declarations mandatory ?*) +Definition finTopMixin := TopMixin finlex1. + +Local Canonical bPOrderType := BPOrderType S finBottomMixin. +Local Canonical tPOrderType := TPOrderType S finTopMixin. +Local Canonical bMeetSemilatticeType := [bMeetSemilatticeType of S]. +Local Canonical tMeetSemilatticeType := [tMeetSemilatticeType of S]. +Local Canonical tbMeetSemilatticeType := [tbMeetSemilatticeType of S]. +Local Canonical bJoinSemilatticeType := [bJoinSemilatticeType of S]. +Local Canonical tJoinSemilatticeType := [tJoinSemilatticeType of S]. +Local Canonical tbJoinSemilatticeType := [tbJoinSemilatticeType of S]. +Local Canonical bLatticeType := [bLatticeType of S]. +Local Canonical tLatticeType := [tLatticeType of S]. +Local Canonical tbLatticeType := [tbLatticeType of S]. + +Local Canonical finPOrderType := [finPOrderType of S]. +Local Canonical finBPOrderType := [finBPOrderType of S]. +Local Canonical finTPOrderType := [finTPOrderType of S]. +Local Canonical finMeetSemilatticeType := [finMeetSemilatticeType of S]. +Local Canonical finBMeetSemilatticeType := [finBMeetSemilatticeType of S]. +Local Canonical finJoinSemilatticeType := [finJoinSemilatticeType of S]. +Local Canonical finTJoinSemilatticeType := [finTJoinSemilatticeType of S]. +Local Canonical finLatticeType := [finLatticeType of S]. +Local Canonical finTBLatticeType := [finTBLatticeType of S]. End FinTBLatticeStructure. Module Exports. Notation finbot := finbot. Notation fintop := fintop. -Coercion tbLattice : finLattice >-> TBLattice.order. -Canonical bMeetOrder. -Canonical tMeetOrder. -Canonical tbMeetOrder. -Canonical bJoinOrder. -Canonical tJoinOrder. -Canonical tbJoinOrder. -Canonical bLattice. -Canonical tLattice. -Canonical tbLattice. +Coercion tbLatticeType : finLattice >-> Order.TBLattice.type. +Canonical bPOrderType. +Canonical tPOrderType. +Canonical bMeetSemilatticeType. +Canonical tMeetSemilatticeType. +Canonical tbMeetSemilatticeType. +Canonical bJoinSemilatticeType. +Canonical tJoinSemilatticeType. +Canonical tbJoinSemilatticeType. +Canonical bLatticeType. +Canonical tLatticeType. +Canonical tbLatticeType. + +Canonical finPOrderType. +Canonical finBPOrderType. +Canonical finTPOrderType. +Canonical finMeetSemilatticeType. +Canonical finBMeetSemilatticeType. +Canonical finJoinSemilatticeType. +Canonical finTJoinSemilatticeType. +Canonical finLatticeType. +Canonical finTBLatticeType. End Exports. End FinTBLatticeStructure. @@ -1389,120 +1402,161 @@ Import FinTBLatticeStructure.Exports. Section TestTBFinLattice. -Context {T : choiceType} {L : {preLattice T}} {S : {finLattice L}}. +Context {disp : Order.disp_t} {T : prelatticeType disp} {S : {finLattice T}}. Context (a : S). Context (I : Type) (F : I -> S). Context (P : pred I). -(*Goal forall (r : seq I), -\big[\fmeet_S / \ftop_S]_(i <- r | P i) F i = -(val (\big[meet S / top S]_(i <- r | P i) insubd a (F i))). -Proof. -move=> r; rewrite (big_val a) /vop /vx0 /fun2_val. -- move=> x y z; apply/val_inj. - by rewrite ?insubdK ?mem_fmeet ?fmeetA ?fsvalP. -- move=> x; apply/val_inj. - by rewrite !insubdK ?mem_fmeet ?mem_ftop ?fmeet1f ?fsvalP. -- move=> x; apply/val_inj. - by rewrite !insubdK ?mem_fmeet ?mem_ftop ?fmeetf1 ?fsvalP. -- move=> opA op1x opx1 x y; apply/val_inj. - rewrite ?insubdK ?mem_fmeet ?fsvalP //; apply: fmeetC; exact: fsvalP. -- move=> opA op1x opx1 opC; congr fsval. - have eq_idx: insubd a \ftop_S = top S by - apply/val_inj; rewrite !insubdK ?mem_ftop. - rewrite {1}eq_idx; apply: (eq_big_op (fun x => val x \in S)). - + exact: mem_ftop. - + by move=> x y xS yS; rewrite insubdK ?mem_fmeet. - + by move=> x y xS yS; apply/val_inj; rewrite !insubdK ?mem_fmeet. - + by move=> i Pi; rewrite insubdK ?FS. -- exact: mem_ftop. -- exact: mem_fmeet. -- exact: FS. -Qed.*) - Goal forall (r : seq I), - val (\big[meet S / top S]_(i <- r | P i) F i) = - \big[\fmeet_S / \ftop_S]_(i <- r | P i) val (F i). + val (\meet_(i <- r | P i) F i) = + \big[premeet S / \ftop_S]_(i <- r | P i) val (F i). Proof. -move=> r0; rewrite big_val_foo /=. -have ->: fsval (top S) = \ftop_S by []. -rewrite (eq_big_op (fun x => x \in S) \fmeet_S) ?mem_ftop //. -- move=> ????; exact:fsvalP. +move=> r0; rewrite big_val2. +have ->: val (@Order.top _ S) = \ftop_S :> T by []. +apply: (eq_big_op (fun x => x \in S)); rewrite ?mem_ftop //. +- move=> ????; exact: fsvalP. - by move=> x y xS yS; rewrite /val_fun2 !insubdK ?mem_fmeet. - move=> ??; exact: fsvalP. Qed. End TestTBFinLattice. +(* ================================================================== *) +Section SubLattice. + +Context {disp : Order.disp_t} (T : prelatticeType disp). + +Definition sublattice (S U : {fset T}):= + [&& (S `<=` U), + [forall x : S, [forall y : S, premeet U (val x) (val y) \in S]] & + [forall x : S, [forall y : S, prejoin U (val x) (val y) \in S]]]. + +Lemma sublatticeP (S U : {fset T}): + reflect + [/\ (S `<=` U), + {in S&, forall x y, premeet U x y \in S} & + {in S&, forall x y, prejoin U x y \in S}] + (sublattice S U). +Proof. +apply/and3PP; first exact:idP. +- apply/(iffP idP). + + move=> h x y xS yS. + by move/forallP: h=> /(_ [`xS]) /forallP /(_ [`yS]). + + move=> h; apply/forallP=> x; apply/forallP=> y; apply: h; exact: valP. +- apply/(iffP idP). + + move=> h x y xS yS. + by move/forallP: h=> /(_ [`xS]) /forallP /(_ [`yS]). + + move=> h; apply/forallP=> x; apply/forallP=> y; apply: h; exact: valP. +Qed. + +Lemma sublattice_fmeet S U: + sublattice S U -> + {in S &, forall x y, premeet S x y = premeet U x y}. +Proof. +move/sublatticeP. +case=> /[dup] ? /fsubsetP SU premeet_SU _ x y xS yS; apply/le_anti/andP; split. +- apply/premeet_incr=> //; exact: premeet_SU. +- apply: premeet_inf=> //; [exact:premeet_SU| | ]. + + apply/premeet_minl; exact: SU. + + apply/premeet_minr; exact: SU. +Qed. + +Lemma sublattice_fjoin S U: + sublattice S U -> + {in S &, forall x y, prejoin S x y = prejoin U x y}. +Proof. +move/sublatticeP. +case=> /[dup] ? /fsubsetP SU _ prejoin_SU x y xS yS; apply/le_anti/andP; split. +- apply: prejoin_sumeet=> //; [exact:prejoin_SU| | ]. + + apply/prejoin_maxl; exact: SU. + + apply/prejoin_maxr; exact: SU. +- apply/prejoin_decr=> //; exact: prejoin_SU. +Qed. + +Context (S U: {fset T}) (sub_SU: sublattice S U) (S_prop0 : S != fset0). + +Lemma premeet_closed_sub: is_premeet_closed S. +Proof. +apply/premeet_closedP=> x y xS yS. +rewrite (sublattice_fmeet sub_SU) //. +case/sublatticeP: sub_SU=> _ + _; exact. +Qed. + +Lemma prejoin_closed_sub: is_prejoin_closed S. +Proof. +apply/prejoin_closedP=> x y xS yS. +rewrite (sublattice_fjoin sub_SU) //. +case/sublatticeP: sub_SU=> _ _; exact. +Qed. + +Definition sub_FinLattice:= FinLattice (premeet_closed_sub) (prejoin_closed_sub) (S_prop0). + +End SubLattice. (* ================================================================== *) Section FinLattice1. -Context {T : choiceType}. -Implicit Type (L : {preLattice T}) (a : T). - -Lemma premeet_closed1 L a : premeet_closed L [fset a]. +Lemma premeet_closed1 {disp} {T : prelatticeType disp} (a : T) : + is_premeet_closed [fset a]. Proof. apply/premeet_closedP=> ?? /fset1P-> /fset1P->; apply/fset1P. -apply/(@rle_anti _ L)/andP; split. +apply/le_anti/andP; split. - by apply/premeet_minl; rewrite fset11. - by apply/premeet_inf; rewrite ?fset11. Qed. -Lemma is_lat1 L a : - [&& premeet_closed L [fset a], - premeet_closed L^~pl [fset a] & - [fset a] != fset0]. -Proof. -apply/and3P; split; try exact/premeet_closed1. -by apply/fset0Pn; exists a; rewrite in_fsetE. -Qed. +Lemma prejoin_closed1 {disp} {T : prelatticeType disp} (a : T) : + is_prejoin_closed [fset a]. +Proof. exact: (@premeet_closed1 _ [prelatticeType of T^d]). Qed. -Definition lat1 L a := FinLattice (is_lat1 L a). +Context {disp : Order.disp_t} {T : prelatticeType disp} (a : T). + +(* Lemma is_lat1 : [&& premeet_closed [fset a], + prejoin_closed [fset a] & [fset a] != fset0]. +Proof. by rewrite premeet_closed1 prejoin_closed1 -cardfs_eq0 cardfs1. Qed. *) + +Program Definition lat1 := FinLattice (premeet_closed1 a) (prejoin_closed1 a) _. +Next Obligation. by rewrite -cardfs_gt0 cardfs1. Qed. End FinLattice1. -Notation "[ 'finlattice' a 'for' L ]" := (@lat1 _ L a). +Notation "[ 'finlattice' a 'for' T ]" := (@lat1 _ T a). (* ==================================================================== *) Section Atom. -Context {T : choiceType}. -Implicit Type (L : {preLattice T}). -Definition atom L (S : {finLattice L}) a := [&& a \in S, (\fbot_S <_L a) & - ~~[exists x : S, (\fbot_S <_L val x) && (val x <_L a)]]. +Definition atom {disp} {T : prelatticeType disp} (S : {finLattice T}) a := + [&& a \in S, (\fbot_S < a) & + ~~[exists x : S, (\fbot_S < val x) && (val x < a)]]. -Definition coatom L (S : {finLattice L}) a := @atom _ S^~s a. +Definition coatom {disp} {T : prelatticeType disp} (S : {finLattice T}) a := + atom S^fd a. -Lemma atomP {L} {S : {finLattice L}} {a} : reflect - ([/\ a \in S, (\fbot_S <_L a) & - forall x, x \in S -> \fbot_S <_L x -> ~~(x <_L a)]) - (atom S a). +Lemma atomP {disp} {T : prelatticeType disp} {S : {finLattice T}} {a} : + reflect + ([/\ a \in S, \fbot_S < a & + forall x, x \in S -> \fbot_S < x -> ~~ (x < a)]) + (atom S a). Proof. apply/(iffP idP). -- case/and3P; rewrite !inE => /= a_in_S bot_lt_a /existsPn atomic. - split => //; move=> y y_in_S bot_lt_y; move: (atomic [`y_in_S]%fset) => /=. - by rewrite negb_and bot_lt_y /=. -- case; rewrite /atom => -> -> /= atomic; apply/existsPn. - move=> x; rewrite negb_and -implybE; apply/implyP => ?. - apply/atomic => //; exact: fsvalP. +- case/and3P => /= -> -> /existsPn atomic; split => // y y_in_S bot_lt_y. + by move: (atomic [`y_in_S]%fset); rewrite negb_and bot_lt_y /=. +- rewrite /atom; case=> [-> -> atomic]; apply/existsPn => x. + by rewrite negb_and -implybE; apply/implyP/atomic/fsvalP. Qed. -Lemma coatomP {L} {S : {finLattice L}} {a} : reflect - ([/\ a \in S, (a <_L \ftop_S) & - forall x, x \in S -> x <_L \ftop_S -> ~~(a <_L x)]) - (coatom S a). -Proof. -apply/(iffP idP). -- by move/atomP. -- move=> ?; exact/atomP. -Qed. +Lemma coatomP {disp} {T : prelatticeType disp} {S : {finLattice T}} {a} : + reflect + ([/\ a \in S, (a < \ftop_S) & + forall x, x \in S -> x < \ftop_S -> ~~ (a < x)]) + (coatom S a). +Proof. exact: (@atomP _ [prelatticeType of T^d] S^fd). Qed. -Lemma mem_atom L (S : {finLattice L}) x : +Lemma mem_atom {disp} {T : prelatticeType disp} (S : {finLattice T}) x : atom S x -> x \in S. Proof. by case/atomP. Qed. -Lemma mem_coatom L (S : {finLattice L}) x : +Lemma mem_coatom {disp} {T : prelatticeType disp} (S : {finLattice T}) x : coatom S x -> x \in S. Proof. by case/coatomP. Qed. @@ -1512,25 +1566,22 @@ End Atom. Module Interval. Section Interval. -Context {T : choiceType}. -Implicit Type (L : {preLattice T}). - -Definition umeet L (S : {finLattice L}) a := - \big[\fmeet_S / \ftop_S]_(i <- S | i >=_L a) i. +Definition umeet {disp} {T : prelatticeType disp} (S : {finLattice T}) a := + \big[premeet S / \ftop_S]_(i <- S | i >= a) i. -Definition djoin L (S : {finLattice L}) b := - \big[\fjoin_S / \fbot_S]_(i <- S | i <=_L b) i. +Definition djoin {disp} {T : prelatticeType disp} (S : {finLattice T}) b := + \big[prejoin S / \fbot_S]_(i <- S | i <= b) i. -Definition interval L (S : {finLattice L}) (a b : T) := +Definition interval {disp} {T : prelatticeType disp} (S : {finLattice T}) (a b : T) := [fset x | x in S & - \fmeet_S (umeet S a) (djoin S b) <=_L x <=_L \fjoin_S (umeet S a) (djoin S b)]. + premeet S (umeet S a) (djoin S b) <= x <= prejoin S (umeet S a) (djoin S b)]. (* TODO: interval -> itv in the name of lemmas * *) -Lemma mem_itv L (S : {finLattice L}) a b x : - x \in S -> a <=_L x -> x <=_L b -> x \in interval S a b. +Lemma mem_itv {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x : + x \in S -> a <= x -> x <= b -> x \in interval S a b. Proof. move=> xS alex xleb; rewrite !inE xS /=. apply/andP; split. @@ -1540,119 +1591,96 @@ apply/andP; split. [exact: mem_bigfmeet |exact: mem_bigfjoin |exact: fjoin_sumeet_seq]. Qed. -Lemma umeetE L (S : {finLattice L}) a : a \in S -> umeet S a = a. +Lemma umeetE {disp} {T : prelatticeType disp} (S : {finLattice T}) a : a \in S -> umeet S a = a. Proof. -move=> aS; apply: (@rle_anti _ L); rewrite fmeet_inf_seq //=. -suff : ((\big[\fmeet_S/ \ftop_S]_(i <- S | le L a i) i) \in S) && - le L a (\big[\fmeet_S/ \ftop_S]_(i <- S | le L a i) i) by +move=> aS; apply/le_anti; rewrite fmeet_inf_seq //=. +suff : ((\big[premeet S/ \ftop_S]_(i <- S | a <= i) i) \in S) && + (a <= (\big[premeet S/ \ftop_S]_(i <- S | a <= i) i)) by case/andP. rewrite big_seq_cond. -rewrite (@big_stable _ _ _ (fun i => (i \in S) && (le L a i))) //. +rewrite (@big_stable _ _ _ (fun i => (i \in S) && (a <= i))) //. - move=> x y /andP [xS alex] /andP [yS aley]. by rewrite mem_fmeet //= lefI ?alex ?aley. - by rewrite mem_ftop lef1. Qed. -Lemma djoinE L (S : {finLattice L}) b : b \in S -> djoin S b = b. -Proof. exact: (@umeetE _ S^~s). Qed. +Lemma djoinE {disp} {T : prelatticeType disp} (S : {finLattice T}) b : b \in S -> djoin S b = b. +Proof. exact: (@umeetE _ _ S^fd). Qed. -Lemma mem_umeet L (S : {finLattice L}) a : umeet S a \in S. +Lemma mem_umeet {disp} {T : prelatticeType disp} (S : {finLattice T}) a : umeet S a \in S. Proof. exact: mem_bigfmeet. Qed. -Lemma mem_djoin L (S : {finLattice L}) b : djoin S b \in S. +Lemma mem_djoin {disp} {T : prelatticeType disp} (S : {finLattice T}) b : djoin S b \in S. Proof. exact: mem_bigfjoin. Qed. -Lemma itv_prop0 L (S : {finLattice L}) a b: +Lemma itv_prop0 {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : interval S a b != fset0. Proof. -apply/fset0Pn; exists (\fmeet_S (umeet S a) (djoin S b)). +apply/fset0Pn; exists (premeet S (umeet S a) (djoin S b)). rewrite !inE; apply/and3P; split => //. - apply: mem_fmeet; [exact: mem_bigfmeet |exact: mem_bigfjoin]. - by rewrite lefIl ?mem_fjoin ?lefUl ?mem_umeet ?mem_djoin. Qed. -Lemma intervalE L (S : {finLattice L}) a b x : - a \in S -> b \in S -> a <=_L b -> - x \in interval S a b = (x \in S) && (a <=_L x <=_L b). +Definition itv_prop0_ {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : + interval S a b != fset0 := @itv_prop0 disp (@Prelattice.Pack disp T (Prelattice.class T)) S a b. + +Lemma intervalE {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x : + a \in S -> b \in S -> a <= b -> + x \in interval S a b = (x \in S) && (a <= x <= b). Proof. move=> aS bS aleb; rewrite !inE umeetE ?djoinE //. by move: (fmeet_l aS bS aleb) (fjoin_r aS bS aleb) => -> ->. Qed. -Lemma intervalP L (S : {finLattice L}) a b x : - a \in S -> b \in S -> a <=_L b -> +Lemma intervalP {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x : + a \in S -> b \in S -> a <= b -> reflect - (x \in S /\ a <=_L x <=_L b) + (x \in S /\ a <= x <= b) (x \in interval S a b). Proof. by move=> aS bS aleb; rewrite intervalE //; apply/andP. Qed. -Lemma itv_subset L (S : {finLattice L}) a b : +Lemma itv_subset {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : {subset interval S a b <= S}. Proof. move=>?; by rewrite in_fsetE; case/and3P. Qed. - -Lemma itv_bound L (S : {finLattice L}) a b x: - a \in S -> b \in S -> a <=_L b -> x \in interval S a b -> - a <=_L x <=_L b. +Lemma itv_bound {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x: + a \in S -> b \in S -> a <= b -> x \in interval S a b -> + a <= x <= b. Proof. by move => aS bS aleb /intervalP []. Qed. -Lemma dual_itv_fset_eq L (S: {finLattice L}) a b: - interval S a b = interval S^~s b a :> {fset _}. +Lemma dual_itv_fset_eq {disp} {T : prelatticeType disp} (S: {finLattice T}) a b: + interval S a b = interval S^fd b a :> {fset T^d}. Proof. apply/eqP/fset_eqP=> x; rewrite !in_fsetE !inE [X in _ && X]andbC. by rewrite fmeetC ?mem_umeet ?mem_djoin // fjoinC ?mem_umeet ?mem_djoin. Qed. -Lemma itv_premeet_closed L (S : {finLattice L}) x y a b: +Lemma itv_premeet_closed {disp} {T : prelatticeType disp} (S : {finLattice T}) x y a b: x \in interval S a b -> y \in interval S a b -> - premeet L S x y \in interval S a b. + premeet S x y \in interval S a b. Proof. rewrite !in_fsetE => /and3P[xS alex xleb] /and3P[yS aley yleb]. apply/and3P; split. - exact: mem_fmeet. - by apply/premeet_inf=> //; apply/mem_fmeet; rewrite ?mem_umeet ?mem_djoin. -- by apply:(rle_trans _ xleb); rewrite premeet_min. +- by apply:(le_trans _ xleb); rewrite premeet_min. Qed. -Lemma premeet_itvE L (S : {finLattice L}) a b x y: - x \in interval S a b -> y \in interval S a b -> - premeet L S x y = premeet L (interval S a b) x y. +Lemma itv_sublattice {disp} {T : prelatticeType disp} (S : {finLattice T}) a b: + sublattice (interval S a b) S. Proof. -move=> x_in y_in. -move: (x_in); rewrite in_fsetE // => /and3P[xS alex xleb]. -move: (y_in); rewrite in_fsetE // => /and3P[yS aley yleb]. -apply/(@rle_anti _ L)/andP; split. -- by apply: premeet_inf=> //; first exact: itv_premeet_closed; - rewrite premeet_min. -- apply: premeet_incr=> //; apply/fsubsetP=> ?; exact: itv_subset. +apply/sublatticeP. +split; first exact/fsubsetP/itv_subset. +- move=> ??; exact: itv_premeet_closed. +- move=> x y; move: (@itv_premeet_closed _ _ S^fd x y b a). + by rewrite -dual_itv_fset_eq dual_fmeetE. Qed. -Lemma itv_prejoin_closed L (S : {finLattice L}) x y a b: - x \in interval S a b -> y \in interval S a b -> - prejoin L S x y \in interval S a b. -Proof. rewrite dual_itv_fset_eq -dual_premeet; exact: itv_premeet_closed. Qed. - -Lemma prejoin_itvE L (S: {finLattice L}) a b x y: - x \in interval S a b -> y \in interval S a b -> - prejoin L S x y = prejoin L (interval S a b) x y. -Proof. rewrite dual_itv_fset_eq -dual_premeet; exact: premeet_itvE. Qed. - -Lemma closed_itv L (S:{finLattice L}) a b: - [&& premeet_closed L (interval S a b), - premeet_closed [preLattice of rdual_rel <=:L] (interval S a b) & - interval S a b != fset0]. -Proof. -apply/and3P; split. -- apply/premeet_closedP; move=> ????. - by rewrite -premeet_itvE // itv_premeet_closed. -- apply/premeet_closedP; move=> ????. - by rewrite /= -prejoin_itvE // itv_prejoin_closed. -- exact: itv_prop0. -Qed. - -Definition FinLatInterval L (S: {finLattice L}) a b := +Definition FinLatInterval {disp} {T : prelatticeType disp} (S: {finLattice T}) a b : + {finLattice T} := (* TODO: lock this definition *) - FinLattice (@closed_itv L S a b). + sub_FinLattice (itv_sublattice S a b) (itv_prop0 S a b). End Interval. Module Exports. @@ -1666,118 +1694,106 @@ Import Interval.Exports. Section IntervalTheory. -Context {T : choiceType}. -Implicit Type (L : {preLattice T}). - Section UmeetDjoin. -Lemma mem_umeet L (S : {finLattice L}) a: umeet S a \in S. +Lemma mem_umeet {disp} {T : prelatticeType disp} (S : {finLattice T}) a: umeet S a \in S. Proof. exact: Interval.mem_umeet. Qed. -Lemma mem_djoin L (S : {finLattice L}) b: djoin S b \in S. +Lemma mem_djoin {disp} {T : prelatticeType disp} (S : {finLattice T}) b: djoin S b \in S. Proof. exact: Interval.mem_djoin. Qed. -Lemma umeetE L (S : {finLattice L}) a: a \in S -> umeet S a = a. +Lemma umeetE {disp} {T : prelatticeType disp} (S : {finLattice T}) a: a \in S -> umeet S a = a. Proof. exact: Interval.umeetE. Qed. -Lemma djoinE L (S : {finLattice L}) b: b \in S -> djoin S b = b. +Lemma djoinE {disp} {T : prelatticeType disp} (S : {finLattice T}) b: b \in S -> djoin S b = b. Proof. exact: Interval.djoinE. Qed. -Lemma le_umeet L (S : {finLattice L}) a b : - b \in S -> a <=_L b -> umeet S a <=_L b. -Proof. -by move=> bS aleb; apply: fmeet_inf_seq. -Qed. +Lemma le_umeet {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : + b \in S -> a <= b -> umeet S a <= b. +Proof. by move=> bS aleb; apply: fmeet_inf_seq. Qed. -Lemma le_djoin L (S : {finLattice L}) a b : - a \in S -> a <=_L b -> djoin S b >=_L a. -Proof. -by move=> aS aleb; apply: fjoin_sumeet_seq. -Qed. +Lemma le_djoin {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : + a \in S -> a <= b -> djoin S b >= a. +Proof. by move=> aS aleb; apply: fjoin_sumeet_seq. Qed. End UmeetDjoin. -Lemma fmeet_itvE L (S : {finLattice L}) a b : - {in []_S &, \fmeet_([< a ; b >]_S) =2 \fmeet_S}. -Proof. by move => x y x_in y_in; rewrite fmeetE -Interval.premeet_itvE. Qed. +Lemma itv_sublattice {disp} {T : prelatticeType disp} (S : {finLattice T}) a b: + sublattice []_S S. +Proof. exact:Interval.itv_sublattice. Qed. -Lemma fjoin_itvE L (S : {finLattice L}) a b : - {in []_S &, \fjoin_([< a ; b >]_S) =2 \fjoin_S}. -Proof. by move => x y x_in y_in; rewrite fjoinE -Interval.prejoin_itvE. Qed. - -Lemma mem_itv L (S : {finLattice L}) a b x : - x \in S -> a <=_L x -> x <=_L b -> x \in [< a ; b >]_S. +Lemma mem_itv {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x : + x \in S -> a <= x -> x <= b -> x \in [< a ; b >]_S. Proof. exact: Interval.mem_itv. Qed. -Lemma intervalE L (S : {finLattice L}) a b x : - a \in S -> b \in S -> a <=_L b -> - x \in [< a ; b >]_S = (x \in S) && (a <=_L x <=_L b). +Lemma intervalE {disp} {T : prelatticeType disp} (S : {finLattice T}) a b x : + a \in S -> b \in S -> a <= b -> + x \in [< a ; b >]_S = (x \in S) && (a <= x <= b). Proof. exact: Interval.intervalE. Qed. -Lemma intervalP L (S: {finLattice L}) a b x: - a \in S -> b \in S -> a <=_L b -> +Lemma intervalP {disp} {T : prelatticeType disp} (S: {finLattice T}) a b x: + a \in S -> b \in S -> a <= b -> reflect - (x \in S /\ a <=_L x <=_L b) + (x \in S /\ a <= x <= b) (x \in [< a ; b >]_S). Proof. exact: Interval.intervalP. Qed. -Lemma itv_subset L (S: {finLattice L}) a b x : +Lemma itv_subset {disp} {T : prelatticeType disp} (S: {finLattice T}) a b x : x \in [< a ; b >]_S -> x \in S. Proof. exact: Interval.itv_subset. Qed. - -Lemma itv_bigrange L (S: {finLattice L}) a b x : +Lemma itv_bigrange {disp} {T : prelatticeType disp} (S: {finLattice T}) a b x : x \in [< a ; b >]_S -> - \fmeet_S (umeet S a) (djoin S b) <=_L x <=_L \fjoin_S (umeet S a) (djoin S b). + premeet S (umeet S a) (djoin S b) <= x <= prejoin S (umeet S a) (djoin S b). Proof. by rewrite !inE /=; case/andP. Qed. -Lemma itv_geL L (S: {finLattice L}) a b x : - a \in S -> a <=_L b -> x \in [< a ; b >]_S -> a <=_L x. +Lemma itv_geL {disp} {T : prelatticeType disp} (S: {finLattice T}) a b x : + a \in S -> a <= b -> x \in [< a ; b >]_S -> a <= x. Proof. move=> aS aleb /itv_bigrange /andP [+ _]. by rewrite (umeetE aS) (fmeet_l aS (mem_djoin S b) (le_djoin aS aleb)). Qed. -Lemma itv_leR L (S: {finLattice L}) a b x : - b \in S -> a <=_L b -> x \in [< a ; b >]_S -> x <=_L b. +Lemma itv_leR {disp} {T : prelatticeType disp} (S: {finLattice T}) a b x : + b \in S -> a <= b -> x \in [< a ; b >]_S -> x <= b. Proof. move=> bS aleb /itv_bigrange /andP [_]. by rewrite (djoinE bS) (fjoin_r (mem_umeet S a) bS (le_umeet bS aleb)). Qed. (*Proof. by move=> bS; rewrite !inE Interval.join_bar // => /and3P []. Qed.*) -Lemma itv_id L (S: {finLattice L}) : [<\fbot_S; \ftop_S>]_S = S. +Lemma itv_id {disp} {T : prelatticeType disp} (S: {finLattice T}) : [<\fbot_S; \ftop_S>]_S = S. Proof. apply/eqP/fset_eqP => x. rewrite !inE; apply: andb_idr => xS. -rewrite ?Interval.umeetE ?Interval.djoinE ?mem_ftop ?mem_fbot //. -by rewrite fmeet_l ?fjoin_r ?le0f ?lef1 ?mem_fbot. +rewrite ?Interval.umeetE ?Interval.djoinE ?mem_fbot ?mem_ftop //. +by rewrite fmeet_l ?fjoin_r ?le0f ?lef1 ?mem_fbot ?mem_ftop. Qed. -Lemma mono_itv L (S : {finLattice L}) (A B a b : T) : - A \in S -> B \in S -> A <=_L B -> - a \in [< A; B >]_S -> b \in []_S -> a <=_L b -> +Lemma mono_itv {disp} {T : prelatticeType disp} (S : {finLattice T}) (A B a b : T) : + A \in S -> B \in S -> A <= B -> + a \in [< A; B >]_S -> b \in []_S -> a <= b -> [< a; b >]_[< A; B >]_S = [< a; b >]_S. Proof. move=> AS BS AleB; rewrite intervalE // => /and3P [aS Alea aleB]. rewrite intervalE // => /and3P [bS Aleb bleB] aleb. apply/eqP/fset_eqP => z; apply/(sameP idP)/(iffP idP). - case/intervalP => // zS /andP [alez zleb]; rewrite !mem_itv //. - + exact: (rle_trans Alea). - + exact: (rle_trans zleb). + + exact: (le_trans Alea). + + exact: (le_trans zleb). - case/intervalP => //; rewrite !intervalE ?aS ?Alea ?aleB ?bS ?Aleb ?bleB //. by case/andP => -> _ /andP [-> ->]. Qed. -Lemma sub_itv L (S : {finLattice L}) a b c d: +Lemma sub_itv {disp} {T : prelatticeType disp} (S : {finLattice T}) a b c d: a \in S -> b \in S -> c \in S -> d \in S -> - a <=_L b -> c <=_L d -> - ([]_S `<=` []_S)%fset = (c <=_L a) && (b <=_L d). + a <= b -> c <= d -> + ([]_S `<=` []_S)%fset = (c <= a) && (b <= d). Proof. move=> aS bS cS dS aleb cled; apply/(sameP idP)/(iffP idP). - case/andP => clea bled; apply/fsubsetP => z. case/intervalP => // zS /andP [alez zleb]. - by rewrite intervalE // zS (rle_trans clea alez) (rle_trans zleb bled). + by rewrite intervalE // zS (le_trans clea alez) (le_trans zleb bled). - move/fsubsetP => sub. have/intervalP: a \in []_S by apply/sub; rewrite mem_itv ?aS ?aleb. @@ -1786,106 +1802,114 @@ move=> aS bS cS dS aleb cled; apply/(sameP idP)/(iffP idP). by case/(_ cS dS) => // _ /andP [_ ->] /(_ cS dS cled) [_ /andP [->]]. Qed. -Lemma dual_itv_r L (S : {finLattice L}) a b : - ([]_S)^~s = [< b ; a>]_(S^~s). -Proof. by apply/val_inj/Interval.dual_itv_fset_eq. Qed. +Lemma dual_itv_r {disp} {T : prelatticeType disp} (S : {finLattice T}) a b : + ([]_S)^fd = [< b ; a>]_S^fd. +Proof. exact/val_inj/Interval.dual_itv_fset_eq. Qed. Definition dual_itv := - (@dual_itv_r, fun L => @dual_itv_r [preLattice of rdual_rel <=:L]). + (@dual_itv_r, fun {disp} {T : prelatticeType disp} => @dual_itv_r _ [prelatticeType of T^d]). -Lemma mem_itvL L (S : {finLattice L}) (x y : T) : - x \in S -> x <=_L y -> x \in [< x; y >]_S. +Lemma mem_itvL {disp} {T : prelatticeType disp} (S : {finLattice T}) (x y : T) : + x \in S -> x <= y -> x \in [< x; y >]_S. Proof. by move=> xS xy; apply/Interval.mem_itv. Qed. -Lemma mem_itvR L (S : {finLattice L}) (x y : T) : - y \in S -> x <=_L y -> y \in [< x; y >]_S. +Lemma mem_itvR {disp} {T : prelatticeType disp} (S : {finLattice T}) (x y : T) : + y \in S -> x <= y -> y \in [< x; y >]_S. Proof. -have -> : S = (S^~s)^~s by exact/val_inj. -rewrite -dual_itv => ??; exact: mem_itvL. +by move/(@mem_itvL _ _ (S^fd))/[apply]; rewrite -dual_itv. Qed. +(* TODO: compare with the previous proof * + * have -> : S = (S^fd)^fd by exact/val_inj. + rewrite -dual_itv => ??; exact: mem_itvL. *) -Lemma mem_0itv L (S : {finLattice L}) (y : T) : +Lemma mem_0itv {disp} {T : prelatticeType disp} (S : {finLattice T}) (y : T) : y \in S -> \fbot_S \in [< \fbot_S; y >]_S. Proof. by move=> yS; rewrite mem_itv ?le0f ?mem_fbot. Qed. - -Lemma mem_itv1 L (S : {finLattice L}) (x : T) : +Lemma mem_itv1 {disp} {T : prelatticeType disp} (S : {finLattice T}) (x : T) : x \in S -> \ftop_S \in [< x; \ftop_S >]_S. Proof. -have -> : S = (S^~s)^~s by exact/val_inj. -rewrite -dual_itv => ?. exact: mem_0itv. +by move/(@mem_0itv _ _ (S^fd)); rewrite -dual_itv. Qed. +(* TODO: compare with + * have -> : S = (S^fd)^fd by exact/val_inj. + rewrite -dual_itv => ?. exact: mem_0itv. *) -Lemma itvE0 L (S : {finLattice L}) : - {in S &, forall a b, a <=_L b -> \fbot_([]_S) = a}. +Lemma itvE0 {disp} {T : prelatticeType disp} (S : {finLattice T}) : + {in S &, forall a b, a <= b -> \fbot_([]_S) = a}. Proof. move=> a b aS bS aleb; apply: fbot_id; rewrite ?mem_itv //. move=> x; exact: itv_geL. Qed. - -Lemma itvE1 L (S : {finLattice L}): - {in S &, forall a b, a <=_L b -> \ftop_([]_S) = b}. +Lemma itvE1 {disp} {T : prelatticeType disp} (S : {finLattice T}): + {in S &, forall a b, a <= b -> \ftop_([]_S) = b}. Proof. -move=> a b aS bS aleb. -have -> : S = (S^~s)^~s by exact/val_inj. -rewrite -dual_itv; exact : itvE0. +move=> a b /[swap]. +by move/(itvE0 (S := S^fd))/[apply]/[apply]; rewrite -dual_itv. Qed. +(* TODO: compare with + * move=> a b aS bS aleb. + have -> : S = (S^fd)^fd by exact/val_inj. + rewrite -dual_itv; exact : itvE0. *) -Lemma sub_atomic L (S: {finLattice L}) x: - x \in S -> \fbot_S <_L x -> - exists2 y, atom S y & y <=_L x. +Lemma sub_atomic {disp} {T : prelatticeType disp} (S: {finLattice T}) x: + x \in S -> \fbot_S < x -> + exists2 y, atom S y & y <= x. Proof. -set S' := ([< \fbot_S; x >]_S `\` [fset \fbot_S; x]). +set S' : {fset T} := ([< \fbot_S; x >]_S `\` [fset \fbot_S; x])%fset. move=> xS botltx. case/boolP: (S' == fset0). - rewrite fsetD_eq0 => /fsubsetP intv_sub. exists x => //; apply/atomP; rewrite xS botltx; split=> //. move=> y yS; apply: contraTN => yltx. have/intv_sub : y \in [< \fbot_S; x >]_S by - rewrite mem_itv ?le0f ?(rltW yltx). - by rewrite !inE (rlt_eqF yltx) orbF; move/eqP => ->; rewrite rltxx. -- case/(minset_neq0 L)/fset0Pn => y /mem_minsetE. + rewrite mem_itv ?le0f ?(ltW yltx). + by rewrite !inE (lt_eqF yltx) orbF; move/eqP => ->; rewrite ltxx. +(* QC : minset_neq0 -> minset_neq0 T *) +- case/(minset_neq0 T)/fset0Pn => y /mem_minsetE. rewrite in_fsetD intervalE ?mem_fbot //; [|rewrite le0f //]. case => /and3P []. rewrite !inE negb_or => /andP [ynbot ynx] yS /andP [boty ylex] miny. exists y=> //. - apply/atomP; rewrite yS rlt_neqAle boty eq_sym ynbot; split => //. + apply/atomP; rewrite yS lt_neqAle boty eq_sym ynbot; split => //. move=> z zS botltz; apply: contraT; rewrite negbK => zlty. - suff/miny: z \in S' by rewrite zlty. + (* QC : TODO : minset still use relorder structures, so we need to unfold Order.lt here *) + suff/miny: z \in S' by rewrite [z <_T y]zlty. rewrite in_fsetD intervalE ?le0f ?zS ?mem_fbot //= ?inE. - rewrite negb_or eq_sym (rlt_eqF botltz). - have zltx := (rlt_le_trans zlty ylex). - by rewrite (rlt_eqF zltx) (rltW zltx). + rewrite negb_or eq_sym (lt_eqF botltz). + have zltx := (lt_le_trans zlty ylex). + by rewrite (lt_eqF zltx) (ltW zltx). Qed. -Lemma sub_coatomic L (S: {finLattice L}) x: - x \in S -> x <_L \ftop_S -> exists2 y, coatom S y & x <=_L y. -Proof. exact: (@sub_atomic _ S^~s). Qed. +Lemma sub_coatomic {disp} {T : prelatticeType disp} (S: {finLattice T}) x: + x \in S -> x < \ftop_S -> exists2 y, coatom S y & x <= y. +Proof. exact: (@sub_atomic _ _ S^fd). Qed. (* -------------------------------------------------------------------- *) Section IndIncr. -Context (L : {preLattice T}). -Variable (P : {finLattice L} -> Prop). + +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Variable (P : {finLattice T} -> Prop). Hypothesis (P_incr : forall S, forall x, atom S x -> P S -> P []_S). -Lemma ind_incr (S : {finLattice L}) (x : T) : +Lemma ind_incr (S : {finLattice T}) (x : T) : x \in S -> P S -> P []_S. Proof. move=> xS PS. move: {2}#|`_| (leqnn #|`[< \fbot_S; x >]_S|) => n. elim: n S xS PS => [|n ih] S xS PS. - rewrite leqn0 => /eqP /cardfs0_eq /(congr1 (fun S => x \in S)). - by rewrite in_fset0 intervalE ?le0f ?rlexx + by rewrite in_fset0 intervalE ?le0f ?lexx ?mem_fbot ?xS. case/boolP: (atom S x) => [atom_Sx|atomN_Sx]; first by move=> _; apply: P_incr. case: (x =P \fbot_S) => [-> _|/eqP neq0_x]; first by rewrite itv_id. -have bot_lt_x: \fbot_S <_L x by rewrite rlt_def neq0_x le0f. +have bot_lt_x: \fbot_S < x by rewrite lt_def neq0_x le0f. move=> sz; case: (sub_atomic xS bot_lt_x) => y atom_Sy ylex. have yS: y \in S by case/atomP: atom_Sy. @@ -1907,52 +1931,65 @@ apply/fsubsetD1P; split. - rewrite sub_itv ?le0f ?mem_fbot ?xS ?yS //=. apply: contraL atom_Sy; rewrite intervalE //. case/and3P => _ ylebot _; apply/negP => /atomP[]. -by rewrite (rle_gtF ylebot). +by rewrite (le_gtF ylebot). Qed. End IndIncr. +(* TODO: this is where things stop working *) + (* -------------------------------------------------------------------- *) Section IndDecr. -Lemma dualK (L : {preLattice T}) (S : {finLattice L}) : (S^~s)^~s = S. + +Lemma dualK (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : + (S^fd)^fd = S. Proof. by exact/val_inj. Qed. -Lemma fbot_dual_r (L : {preLattice T}) (S : {finLattice L}) : - \fbot_(S^~s) = \ftop_S. +(*Variable (disp : Order.disp_t) (T : prelatticeType disp). +Check ([prelatticeType of T^d]). +Variable (S : {finLattice [prelatticeType of T^d]}). +*) + +Lemma fbot_dual_r (disp : Order.disp_t) (T : prelatticeType disp) (S : {finLattice T}) : + \fbot_(S^fd) = \ftop_S. Proof. by []. Qed. -Notation dualize := (fun f => (@f, fun L => @f [preLattice of rdual_rel <=:L])). +Notation dualize := (fun f => (@f, fun d' (L : prelatticeType d') => @f (Order.dual_display d') [prelatticeType of L^d])). Definition fbot_dual := dualize fbot_dual_r. -Context (L : {preLattice T}). -Variable (P : {finLattice L} -> Prop). +Context {disp : Order.disp_t} {T : prelatticeType disp}. +(* Variable (P : {finLattice T} -> Prop). *) -Hypothesis (P_decr : forall S, forall x, - coatom S x -> P S -> P [<\fbot_S; x>]_S). +(* Hypothesis (P_decr : forall S, forall x, + coatom S x -> P S -> P [<\fbot_S; x>]_S). *) + +Let eta_T := @Prelattice.Pack disp T (Prelattice.class T). +Lemma eta_TP: eta_T = T. +Proof. rewrite /eta_T; by case:T. Qed. -Lemma ind_decr (S : {finLattice L}) (x : T) : +Lemma ind_decr (P : {finLattice T} -> Prop) (P_decr : forall S, forall x, +coatom S x -> P S -> P [<\fbot_S; x>]_S) (S : {finLattice T}) (x : T): x \in S -> P S -> P [<\fbot_S; x>]_S. Proof. -move=> x_in_S PS. +elim/eq_ind: T/eta_TP in P P_decr S x * => x_in_S PS. rewrite -[S]dualK -dual_itv fbot_dual. -apply: (ind_incr (P := fun S' : finLattice [preLattice of rdual_rel <=:L] => P S'^~s)) => //. -- by move=> S' x' ??; rewrite dual_itv; apply: P_decr. -- by rewrite dualK. +apply: (ind_incr (P := fun S' : {finLattice T^d} => P S'^fd)) => //. +by move=> S' x' ??; rewrite dual_itv; apply: P_decr. Qed. End IndDecr. (* -------------------------------------------------------------------- *) Section Ind. -Context (L : {preLattice T}). -Variable (P : {finLattice L} -> Prop). +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Variable (P : {finLattice T} -> Prop). -Hypothesis (P_incr : forall (S: {finLattice L}), forall x, +Hypothesis (P_incr : forall (S: {finLattice T}), forall x, atom S x -> P S -> P []_S). -Hypothesis (P_decr : forall (S:{finLattice L}), forall x, +Hypothesis (P_decr : forall (S:{finLattice T}), forall x, coatom S x -> P S -> P [<\fbot_S; x>]_S). -Lemma ind_id (S : {finLattice L}) (x y : T) : - x \in S -> y \in S -> x <=_L y -> P S -> P []_S. +Lemma itv_induction (S : {finLattice T}) (x y : T) : + x \in S -> y \in S -> x <= y -> P S -> P []_S. Proof. move=> xS yS xley PS; have h: P [< x; \ftop_S >]_S by apply: ind_incr. have Sprop0 : S != fset0 :> {fset _} by apply/fset0Pn; exists x. @@ -1968,11 +2005,11 @@ End IntervalTheory. (* -------------------------------------------------------------------- *) Module Morphism. Section ClassDef. -Context (T : choiceType) (L : {preLattice T}) (S: {fset T}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S: {fset T}). Definition axiom (f : T -> T) := - {in S&, {morph f : x y / premeet L S x y >-> premeet L (f @` S) x y}} - /\ {in S&, {morph f : x y / prejoin L S x y >-> prejoin L (f @` S) x y}}. + {in S&, {morph f : x y / premeet S x y >-> premeet (f @` S) x y}} + /\ {in S&, {morph f : x y / prejoin S x y >-> prejoin (f @`S) x y}}. Structure map (phS : phant S) := Pack {apply; _ : axiom apply}. @@ -1990,8 +2027,8 @@ Module Exports. Notation fmorphism f := (axiom f). Coercion apply : map >-> Funclass. Notation FMorphism fM := (Pack (Phant _) fM). -Notation "{ 'fmorphism' S 'on' L }" := (map L (Phant S)) - (at level 0, L at level 0, format "{ 'fmorphism' S 'on' L }"). +Notation "{ 'fmorphism' S }" := (map (Phant S)) + (at level 0, format "{ 'fmorphism' S }"). End Exports. End Morphism. Import Morphism.Exports. @@ -2000,25 +2037,27 @@ Import Morphism.Exports. Section FinLatticeImg. -Context {T : choiceType} {L : {preLattice T}}. -Context {S : {finLattice L}} (f : {fmorphism S on L}). +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Context {S : {finLattice T}} (f : {fmorphism S}). + +Notation finLatImg := (f @`(S : {fset _})). -Lemma finLatImg_prop0 : f @` S != fset0. +Lemma finLatImg_prop0 : finLatImg != fset0. Proof. case/fset0Pn : (finLattice_prop0 S) => x xS; apply/fset0Pn; exists (f x). exact: in_imfset. Qed. Lemma fmorph_premeet : - {in S&, {morph f : x y / premeet L S x y >-> premeet L (f @` S) x y}}. -Proof. by rewrite finLattice_funE; case: f => ? []. Qed. + {in S&, {morph f : x y / premeet S x y >-> premeet finLatImg x y}}. +Proof. by case: f => ? []. Qed. Lemma fmorph_prejoin : - {in S&, {morph f : x y / prejoin L S x y >-> prejoin L (f @` S) x y}}. -Proof. by rewrite finLattice_funE; case: f => ? []. Qed. + {in S&, {morph f : x y / prejoin S x y >-> prejoin finLatImg x y}}. +Proof. by case: f => ? []. Qed. -Lemma finLatImg_premeet_closed : premeet_closed L (f @` S). +Lemma finLatImg_premeet_closed : is_premeet_closed finLatImg. Proof. apply/premeet_closedP => x y /imfsetP + /imfsetP. case => x' x'S -> [y' y'S ->]. @@ -2026,24 +2065,16 @@ rewrite -fmorph_premeet ?in_imfset //. exact : (mem_fmeet x'S y'S). Qed. -Lemma finLatImg_prejoin_closed : premeet_closed (L^~pl) (f @` S). +Lemma finLatImg_prejoin_closed : is_prejoin_closed finLatImg. Proof. -apply/premeet_closedP => x y /imfsetP + /imfsetP /=. +apply/prejoin_closedP => x y /imfsetP + /imfsetP /=. case => x' x'S -> [y' y'S ->]. rewrite -fmorph_prejoin ?in_imfset //. exact : (mem_fjoin x'S y'S). Qed. -Lemma finLatImg_finLat : - [&& premeet_closed L (f @` S), - premeet_closed (L^~pl) (f @` S) & - (f @` S) != fset0]. -Proof. -by rewrite finLatImg_prop0 finLatImg_premeet_closed - finLatImg_prejoin_closed. -Qed. - -Canonical finLatImg_finLattice := FinLattice finLatImg_finLat. +Canonical finLatImg_finLattice : {finLattice T} := + FinLattice finLatImg_premeet_closed finLatImg_prejoin_closed finLatImg_prop0. End FinLatticeImg. @@ -2051,107 +2082,25 @@ Notation "'\codom' f" := (@finLatImg_finLattice _ _ _ f) (at level 24, format "'\codom' f"). Section MorphismTheory. -Context (T : choiceType). +Context {disp : Order.disp_t} {T : prelatticeType disp}. -Implicit Type (L : {preLattice T}). - -Lemma fmorphismP L (S : {fset T}) (f : {fmorphism S on L}) : - fmorphism L S f. +Lemma fmorphismP (S : {fset T}) (f : {fmorphism S}) : + fmorphism S f. Proof. by case : f. Qed. +Lemma fmorphI (S : {finLattice T}) (f : {fmorphism S}) : + {in S &, {morph f : x y / premeet S x y >-> premeet (\codom f) x y}}. +Proof. by case: (fmorphismP f). Qed. -Lemma fmorphI L (S : {finLattice L}) (f : {fmorphism S on L}) : - {in S &, {morph f : x y / \fmeet_S x y >-> \fmeet_(\codom f) x y}}. -Proof. by move=> ????; rewrite !fmeetE fmorph_premeet. Qed. - -Lemma fmorphU L (S : {finLattice L}) (f : {fmorphism S on L}) : - {in S &, {morph f : x y / \fjoin_S x y >-> \fjoin_(\codom f) x y}}. -Proof. by move=> ????; rewrite !fjoinE fmorph_prejoin. Qed. +Lemma fmorphU (S : {finLattice T}) (f : {fmorphism S}) : + {in S &, {morph f : x y / prejoin S x y >-> prejoin (\codom f) x y}}. +Proof. by case: (fmorphismP f). Qed. -Lemma codomP L (S1 S2 : {finLattice L}) (f : {fmorphism S1 on L}) : - f @` S1 = S2 -> \codom f = S2. +Lemma codomP (S1 S2 : {finLattice T}) (f : {fmorphism S1}) : + f @` (S1 : {fset _}) = S2 -> \codom f = S2. Proof. move=> ?; exact: val_inj. Qed. -(* ------------------------------------------------------------------- *) - -(*Lemma meet_morph_homo L (S: {finLattice L}) f : - {in S &, {morph f : x y / premeet L S x y >-> - premeet L (f @` (S : {fset _})) x y}} -> - {in S &, {homo f : x y / x <=_L y}}. -Proof. -move=> f_morph x y xS yS xley. -suff <-: premeet L (f @` (S : {fset _})) (f x) (f y) = f x by - rewrite premeet_minr // in_imfset. -rewrite -f_morph //; congr f. apply: (@le_anti _ L). -by rewrite premeet_minl ?premeet_inf. -Qed. - -Lemma meet_morph_mono L (S : {finLattice L}) f : - {in S &, {morph f : x y / premeet L S x y >-> - premeet L (f @` (S : {fset _})) x y}} -> - {in S &, injective f} -> {in S &, {mono f : x y / x <=_L y}}. -Proof. -move=> f_morph f_inj x y xS yS. -apply/(sameP idP)/(iffP idP); first exact: (meet_morph_homo f_morph). -move=> fxlefy. -suff: premeet L (f @` (S : {fset _})) (f x) (f y) == (f x). -- rewrite -f_morph ?(inj_in_eq f_inj) ?(mem_fmeet xS) //. - move/eqP => <-; exact: premeet_minr. -by apply/eqP/(@le_anti _ L); rewrite premeet_minl ?premeet_inf ?in_imfset. -Qed. - -Lemma meet_fmorphism L (S : {finLattice L}) f : - {in S &, {morph f : x y / premeet L S x y >-> - premeet L (f @` (S : {fset _})) x y}} -> - {in S &, injective f} -> fmorphism L S f. -Proof. -move=> f_morph f_inj; rewrite /(fmorphism _). -have f_mono := (meet_morph_mono f_morph f_inj). -split; first exact: f_morph. -move=> x y xS yS; apply/(@le_anti _ L)/andP; split. -Admitted. - -(*Lemma meet_fmorphism L (S1 S2 : {finLattice L}) (f : T -> T) : - {in S1, forall x, f x \in S2} -> - {in S1&, {morph f : x y / \fmeet_S1 x y >-> \fmeet_S2 x y}} -> - {in S1 & on S2, bijective f} -> fmorphism L S1 S2 f. -Proof. -move=> f_im f_morph [g] [g_im fgK gfK]. -have f_mono := (meet_morph_mono f_im f_morph (can_in_inj fgK)). -split => //. -+ move=> x y xS yS. - apply/(@le_anti _ L)/andP; split. - - rewrite -[X in (_ <=__ X)]gfK ?f_mono ?leUf ?g_im ?mem_fjoin ?f_im //. - rewrite -f_mono ?g_im ?mem_fjoin ?f_im //. - rewrite -[X in _ && X]f_mono ?g_im ?mem_fjoin ?f_im //. - by rewrite gfK ?lefUl ?lefUr ?mem_fjoin ?f_im. - - by rewrite leUf ?f_mono ?lefUl ?lefUr ?f_im ?mem_fjoin. -+ apply/(@le_anti _ L)/andP; split; rewrite ?le0f ?f_im ?mem_fbot //. - by rewrite -[X in (_ <=__ X)]gfK ?f_mono ?le0f ?g_im ?mem_fbot. -+ apply/(@le_anti _ L)/andP; split; rewrite ?lef1 ?f_im ?mem_fbot //. - by rewrite -[X in (X <=__ _)]gfK ?f_mono ?lef1 ?g_im ?mem_fbot. -Qed.*) - -Lemma dual_fmorphism L (S : {finLattice L}) (f : T -> T) : - fmorphism L S f <-> fmorphism L S^~s f. -Proof. by split; case; split. Qed. - -Lemma join_fmorphism L (S : {finLattice L}) (f : T -> T) : - {in S &, {morph f : x y / prejoin L S x y >-> - prejoin L (f @` (S : {fset _})) x y}} -> - {in S &, injective f} -> fmorphism L S f. -Proof. -move=> morph_join inj; apply/dual_fmorphism. -by move: (@meet_fmorphism _ S^~s f) => /(_ morph_join inj) []. -Qed.*) - -(* ----------------------------------------------------------------- *) -(*Context (L : {preLattice T}) (S : {finLattice L}). -Context (f g : {fmorphism S on L}).*) - - - -Lemma fmorph0 L (S : {finLattice L}) (f : {fmorphism S on L}): +Lemma fmorph0 (S : {finLattice T}) (f : {fmorphism S}): f \fbot_S = \fbot_(\codom f). Proof. symmetry; apply: fbot_id; first exact/in_imfset/mem_fbot. @@ -2160,41 +2109,41 @@ have fxfS: f x \in (\codom f) by rewrite in_imfset. by rewrite (leEfmeet _ fxfS) ?in_imfset -?fmorphI ?mem_fbot ?fmeet0f. Qed. -Lemma fmorph1 L (S : {finLattice L}) (f : {fmorphism S on L}): +Lemma fmorph1 (S : {finLattice T}) (f : {fmorphism S}): f \ftop_S = \ftop_(\codom f). Proof. -symmetry; apply: ftop_id; first exact/in_imfset/mem_fbot. +symmetry; apply: ftop_id; first exact/in_imfset/mem_ftop. move=> y /imfsetP [x xS ->]. have fxfS: f x \in (\codom f) by rewrite in_imfset. by rewrite (leEfmeet fxfS) ?in_imfset -?fmorphI ?mem_ftop ?fmeetf1. Qed. -Lemma fmorph_homo L (S : {finLattice L}) (f : {fmorphism S on L}): - {in S&, {homo f : x y / x <=_L y}}. +Lemma fmorph_homo (S : {finLattice T}) (f : {fmorphism S}): + {in S&, {homo f : x y / x <= y}}. Proof. move=> x y xS yS; rewrite (leEfjoin xS) // => /eqP. move/(congr1 f); rewrite fmorphU // => <-. by apply/lefUr; rewrite in_imfset. Qed. -Lemma fmorph_mono L (S : {finLattice L}) (f : {fmorphism S on L}): - {in S&, injective f} -> {in S&, {mono f : x y / x <=_L y}}. +Lemma fmorph_mono (S : {finLattice T}) (f : {fmorphism S}): + {in S&, injective f} -> {in S&, {mono f : x y / x <= y}}. Proof. move=> f_inj x y xS yS; rewrite (leEfjoin xS) //. rewrite (@leEfjoin _ _ (\codom f)) ?in_imfset //. by rewrite -fmorphU //; apply/(inj_in_eq f_inj)=> //; apply: mem_fjoin. Qed. -Lemma fmorph_monolt L (S : {finLattice L}) (f : {fmorphism S on L}): - {in S&, injective f} -> {in S&, {mono f : x y / x <_L y}}. +Lemma fmorph_monolt (S : {finLattice T}) (f : {fmorphism S}): + {in S&, injective f} -> {in S&, {mono f : x y / x < y}}. Proof. -move=> f_inj x y xS yS; rewrite !rlt_def; congr (_ && _). +move=> f_inj x y xS yS; rewrite !lt_def; congr (_ && _). - apply/(sameP idP)/(iffP idP); first exact/contra_neq/f_inj. by apply/contra_neq => ->. - exact: fmorph_mono. Qed. -Lemma mem_fmorphP L (S : {finLattice L}) (f : {fmorphism S on L}) x: +Lemma mem_fmorphP (S : {finLattice T}) (f : {fmorphism S}) x: reflect (exists2 y, y \in S & f y = x) (x \in (\codom f)). Proof. apply/(iffP idP). @@ -2202,7 +2151,7 @@ apply/(iffP idP). - by case => y yS <-; rewrite in_imfset. Qed. -Lemma mem_fmorph L (S : {finLattice L}) (f : {fmorphism S on L}) x: +Lemma mem_fmorph (S : {finLattice T}) (f : {fmorphism S}) x: x \in S -> f x \in (\codom f). Proof. by move=> xS; rewrite in_imfset. Qed. @@ -2210,18 +2159,18 @@ End MorphismTheory. Section IsoFMorph. -Context {T : choiceType} (L : {preLattice T}). +Context {disp : Order.disp_t} {T : prelatticeType disp}. Context (S1 S2 : {fset T}). Definition morphic_fmeet (f : T -> T) := [forall x: S1, [forall y : S1, - f (premeet L S1 (fsval x) (fsval y)) == - premeet L (f @` (S1 : {fset _})) (f (fsval x)) (f (fsval y))]]. + f (premeet S1 (fsval x) (fsval y)) == + premeet (f @` (S1 : {fset _})) (f (fsval x)) (f (fsval y))]]. Definition morphic_fjoin (f : T -> T) := [forall x: S1, [forall y : S1, - f (prejoin L S1 (fsval x) (fsval y)) == - prejoin L (f @` (S1 : {fset _})) (f (fsval x)) (f (fsval y))]]. + f (prejoin S1 (fsval x) (fsval y)) == + prejoin (f @` (S1 : {fset _})) (f (fsval x)) (f (fsval y))]]. Definition morphic (f : T -> T) := morphic_fmeet f && morphic_fjoin f. @@ -2238,7 +2187,7 @@ Definition misof f := [&& morphic f, injf f & surjf f]. Definition isof := exists f : T -> T, misof f. -Lemma morphicP (f : T -> T): reflect (fmorphism L S1 f) (morphic f). +Lemma morphicP (f : T -> T): reflect (fmorphism S1 f) (morphic f). Proof. rewrite /morphic /morphic_fmeet /morphic_fjoin /(fmorphism _). apply/andPP; apply/(iffP idP). @@ -2264,7 +2213,7 @@ Qed. Lemma misofP (f : T -> T): reflect - ([/\ fmorphism L S1 f, {in S1&, injective f} & f @` S1 = S2]) + ([/\ fmorphism S1 f, {in S1&, injective f} & f @` (S1 : {fset _}) = S2]) (misof f). Proof. apply/and3PP; [exact/morphicP | exact/injfP |exact/eqP]. Qed. @@ -2273,14 +2222,14 @@ Lemma misof_isof (f : T -> T): Proof. by move=> ?; exists f. Qed. Lemma misof_fmorph (f : T -> T) : - misof f -> exists2 g : {fmorphism S1 on L}, misof g & f =1 g. + misof f -> exists2 g : {fmorphism S1}, misof g & f =1 g. Proof. case/misofP => f_morph f_inj f_surj. by exists (FMorphism f_morph) => //; apply/misofP. Qed. Lemma isofP : - (exists f, [/\ fmorphism L S1 f, {in S1&, injective f} & f @` S1 = S2]) <-> + (exists f, [/\ fmorphism S1 f, {in S1&, injective f} & f @` S1 = S2]) <-> (isof). Proof. split. @@ -2292,54 +2241,68 @@ End IsoFMorph. Section IsoFmorphTheory. -Context {T : choiceType}. +Context {disp : Order.disp_t} {T : prelatticeType disp}. -Lemma misof0 (L : {preLattice T}) (S1 S2: {finLattice L}) +Lemma misof0 (S1 S2: {finLattice T}) (f : T -> T) : - misof L S1 S2 f -> f \fbot_S1 = \fbot_S2. + misof S1 S2 f -> f \fbot_S1 = \fbot_S2. Proof. case/misofP => [[f_morphI f_morphU] f_inj f_surj]. symmetry; apply: fbot_id; rewrite ?inE -?f_surj ?in_imfset ?mem_fbot //. move=> x; rewrite inE -f_surj => /imfsetP [y /= yS1 ->]. rewrite (leEfmeet (S:=S2)) ?inE ?fmeetE -?f_surj ?in_imfset ?mem_fbot //. rewrite -f_morphI ?mem_fbot //; apply/eqP; congr f. -by rewrite -fmeetE fmeet0f. +by rewrite fmeet0f. Qed. -Lemma misof1 (L : {preLattice T}) (S1 S2: {finLattice L}) +Lemma misof1 (S1 S2: {finLattice T}) (f : T -> T) : - misof L S1 S2 f -> f \ftop_S1 = \ftop_S2. + misof S1 S2 f -> f \ftop_S1 = \ftop_S2. Proof. case/misofP => [[f_morphI f_morphU] f_inj f_surj]. symmetry; apply: ftop_id; rewrite ?inE -?f_surj ?in_imfset ?mem_ftop //. move=> x; rewrite inE -f_surj => /imfsetP [y /= yS1 ->]. rewrite (leEfjoin (S:=S2)) ?inE ?fjoinE -?f_surj ?in_imfset ?mem_ftop //. rewrite -f_morphU ?mem_ftop //; apply/eqP; congr f. -by rewrite -fjoinE fjoin1f. +by rewrite fjoin1f. Qed. -Lemma misof_codom (L : {preLattice T}) (S1 S2 : {finLattice L}) - (f: {fmorphism S1 on L}): - misof L S1 S2 f -> \codom f = S2. -Proof. case/misofP => _ _; rewrite -finLattice_funE; exact: codomP. Qed. - -Lemma misof_inj (L : {preLattice T}) (S1 S2 : {finLattice L}) - (f: T -> T): - misof L S1 S2 f -> {in S1&, injective f}. -Proof. by case/misofP. Qed. +(* QC : elements presence makes proof easier *) +Lemma misof_sublattice {S1 U1 U2: {finLattice T}} (f : T -> T): + misof U1 U2 f-> sublattice S1 U1-> sublattice (f @` elements S1) U2. +Proof. +move=> /misofP [-[meet_morph join_morph] f_inj U2_eq]. +case/sublatticeP=> /fsubsetP SU1 meet_S1 join_S1. +apply/sublatticeP; split. +- apply/fsubsetP=> ? /imfsetP /= [x xS1 ->]. + rewrite -U2_eq; apply: in_imfset=> /=; exact: SU1. +- move=> x y /imfsetP [/= x' x'S1 ->] /imfsetP [/= y' y'S1 ->]. + rewrite -U2_eq -meet_morph; try exact: SU1. + exact/in_imfset/meet_S1. +- move=> x y /imfsetP [/= x' x'S1 ->] /imfsetP [/= y' y'S1 ->]. + rewrite -U2_eq -join_morph; try exact: SU1. + exact/in_imfset/join_S1. +Qed. -Lemma misof_surj (L : {preLattice T}) (S1 S2 : {finLattice L}) - (f: T -> T): - misof L S1 S2 f -> f @`S1 = S2. -Proof. by case/misofP; rewrite finLattice_funE. Qed. +Lemma sublattice_misof {S1 U1 U2: {finLattice T}} (f : T -> T): + misof U1 U2 f-> sublattice S1 U1-> misof S1 (f @` elements S1) f. +Proof. +move=> /[dup] U12 /misofP [[f_meet f_join] f_inj U2_eq]. +move=> /[dup] SU1 /sublatticeP [/fsubsetP SU1_sub sub_meet sub_join]. +move: (misof_sublattice U12 SU1)=> sub_fS1U2. +apply/misofP; split=> //; first split. +- move=> x y xS1 yS1; rewrite (sublattice_fmeet SU1) //. + by rewrite f_meet ?SU1_sub // U2_eq -(sublattice_fmeet sub_fS1U2) // ?in_imfset. +- move=> x y xS1 yS1; rewrite (sublattice_fjoin SU1) //. + by rewrite f_join ?SU1_sub // U2_eq -(sublattice_fjoin sub_fS1U2) // ?in_imfset. +- move=> x y xS1 yS1; apply: f_inj; exact: SU1_sub. +Qed. Section ItvMorph. -Implicit Type L : {preLattice T}. - -Lemma fmorph_itv L (S : {finLattice L}) (f: {fmorphism S on L}) a b : - a \in S -> b \in S -> a <=_L b -> {in S&, injective f} -> - f @` [< a; b>]_S = [< f a; f b>]_(\codom f). +Lemma fmorph_itv (S : {finLattice T}) (f: {fmorphism S}) a b : + a \in S -> b \in S -> a <= b -> {in S&, injective f} -> + f @` ([< a; b>]_S : {fset _}) = [< f a; f b>]_(\codom f). Proof. move=> aS bS aleb f_inj; apply/eqP/fset_eqP => x. apply/(sameP idP)/(iffP idP). @@ -2352,57 +2315,9 @@ apply/(sameP idP)/(iffP idP). rewrite intervalE ?mem_fmorph ?fmorph_homo //. Qed. -Lemma fmorph_memitv L (S : {finLattice L}) (f: {fmorphism S on L}) a b: - a \in S -> b \in S -> a <=_L b -> {in S&, injective f} -> - forall x, x \in []_S -> (f x) \in []_(\codom f). -Proof. -by move=> ??????; rewrite inE -fmorph_itv // in_imfset. -Qed. - -Lemma itv_isomorph L (S1 S2: {finLattice L}) - (f : T -> T) a b: - a \in S1 -> b \in S1 -> a <=_L b -> - misof L S1 S2 f -> - misof L []_S1 (f @` ([< a ; b >]_S1)) f. -Proof. -move=> aS1 bS1 aleb /misof_fmorph [g]. -case/misofP => _ g_inj g_surj g_eq. -have g_fset: forall S: {fset _}, f @` S = g @` S - by move=> S; apply/fsetP => z; apply/idP/idP => /imfsetP [x xS ->]; - rewrite -?g_eq ?in_imfset ?g_eq ?in_imfset. -apply/misofP; split; first split. -- move=> x y x_itv y_itv. - rewrite !g_eq g_fset -finLattice_funE fmorph_itv //. - rewrite -!fmeetE !fmeet_itvE ?fmorphI ?fmorph_memitv //. - exact: (itv_subset x_itv). - exact: (itv_subset y_itv). -- move=> x y x_itv y_itv. - rewrite !g_eq g_fset -finLattice_funE fmorph_itv //. - rewrite -!fjoinE !fjoin_itvE ?fmorphU ?fmorph_memitv //. - exact: (itv_subset x_itv). - exact: (itv_subset y_itv). -- move=> ?? /itv_subset ? /itv_subset ?; rewrite !g_eq; exact: g_inj. -- by rewrite finLattice_funE. -Qed. - -Lemma isomorph_itv L (S1 S2: {finLattice L}) - (f : T -> T) a b: - a \in S1 -> b \in S1 -> a <=_L b -> - misof L S1 S2 f -> - misof L []_S1 [< f a ; f b >]_S2 f. -Proof. -move=> aS1 bS1 aleb miso_f. -move/misof_fmorph: (miso_f)=> [g miso_g]. -move/misof_codom: (miso_g)=> <- g_eq. -rewrite !g_eq -fmorph_itv //; last exact: (misof_inj miso_g). -have ->: g @` [< a; b >]_S1 = f @` [< a; b >]_S1 by - apply: eq_imfset. -exact: (itv_isomorph (S2:=S2)). -Qed. - -Lemma fmorph_atom L (S1 S2 : {finLattice L}) +Lemma fmorph_atom (S1 S2 : {finLattice T}) (f : T -> T) x : - misof L S1 S2 f -> atom S1 x -> atom S2 (f x). + misof S1 S2 f -> atom S1 x -> atom S2 (f x). Proof. case/misof_fmorph => g misof_g ->. case/misofP : (misof_g) => [_ g_inj g_surj]. @@ -2420,17 +2335,15 @@ End ItvMorph. Section BijMorphism. -Implicit Type (L : {preLattice T}). - -Lemma isof_refl L (S : {finLattice L}): isof L S S. +Lemma isof_refl (S : {finLattice T}): isof S S. Proof. -have idmorph: fmorphism L S id by +have idmorph: fmorphism S id by split => x y xS yS /=; rewrite imfset_id. by apply/isofP; exists id; split=> //=; rewrite imfset_id. Qed. -Lemma isof_sym L (S1 S2 : {finLattice L}): - isof L S1 S2 -> isof L S2 S1. +Lemma isof_sym (S1 S2 : {finLattice T}): + isof S1 S2 -> isof S2 S1. Proof. case/isofP => f [[f_morphI f_morphU] f_inj f_surj]. have [g]: {in S1& on S2, bijective f}. @@ -2450,16 +2363,15 @@ apply/misofP; split; first split. rewrite cancel_r ?f_surj ?mem_fmeet ?f_morphI ?cancel_r ?gS1 //. by congr premeet; rewrite -f_surj. - move=> x y xS2 yS2; apply: f_inj; - rewrite ?gS1 ?mem_fmeet // -?f_surj -?imfset_comp /= - ?gfS1 ?mem_fmeet ?gS1 //. - rewrite cancel_r ?f_surj ?mem_fmeet ?f_morphU ?cancel_r ?gS1 //. + rewrite ?gS1 ?mem_fjoin // -?f_surj -?imfset_comp /= ?gfS1 ?mem_fjoin ?gS1 //. + rewrite cancel_r ?f_surj ?mem_fjoin ?f_morphU ?cancel_r ?gS1 //. by congr prejoin; rewrite -f_surj. - by move=> x y xS2 yS2; move/(congr1 f); rewrite !cancel_r. - by rewrite -f_surj -imfset_comp /=. Qed. -Lemma isof_trans L (S1 S2 S3 : {finLattice L}) : - isof L S1 S2 -> isof L S2 S3 -> isof L S1 S3. +Lemma isof_trans (S1 S2 S3 : {finLattice T}) : + isof S1 S2 -> isof S2 S3 -> isof S1 S3. Proof. case/isofP => f [[f_morphI f_morphU] f_inj f_surj]. case/isofP => g [[g_morphI g_morphU] g_inj g_surj]. @@ -2476,40 +2388,45 @@ exists (g \o f); apply/misofP; split; first split. - by rewrite imfset_comp /= -g_surj f_surj. Qed. -Lemma meet_isof L (S1 S2 : {finLattice L}) (f : T -> T) : +Lemma meet_isof (S1 S2 : {finLattice T}) (f : T -> T) : {in S1&, injective f} -> f @` (S1 : {fset _}) = S2 -> - {in S1&, {morph f : x y / \fmeet_S1 x y >-> \fmeet_S2 x y}} -> - misof L S1 S2 f. + {in S1&, {morph f : x y / premeet S1 x y >-> premeet S2 x y}} -> + misof S1 S2 f. Proof. move=> f_inj f_surj f_meetmorph; apply/misofP; split => //. split; rewrite f_surj //. -move=> x y xS1 yS1; rewrite -!fjoinE. -rewrite !fjoin_meets ?inE -?f_surj ?in_imfset // f_surj big_seq_cond. -rewrite (big_morph_sub f_meetmorph); - [ |by move=> ?; case/and3P |exact: mem_fmeet |exact: mem_ftop]. -rewrite -f_surj. +move=> x y xS1 yS1. +rewrite !fjoin_meets; try by (rewrite ?inE -?f_surj ?in_imfset). +rewrite big_seq_cond [RHS]big_seq_cond (big_morph_sub f_meetmorph); + [ |by move=> ? /and3P []|exact:mem_fmeet|exact:mem_ftop]. +rewrite -{2}f_surj. have f_surj_perm : perm_eq (f @` (S1 : {fset _})) [seq f x | x <- S1] by exact: enum_imfset. -rewrite [RHS]big_seq_cond. rewrite (big_perm_sub (fmeetC (S := S2)) (fmeetA (S := S2)) (mem_fmeet (S := S2)) _ (mem_ftop S2) _ f_surj_perm); last first. - by move=> ? /and3P []; rewrite f_surj. -rewrite big_map_id [RHS]big_seq_cond. + by move=> ? /and3P []. have <-: \ftop_S2 = f \ftop_S1. - apply: ftop_id; rewrite ?inE -?f_surj ?in_imfset ?mem_ftop //. move=> z; rewrite inE -f_surj => /imfsetP [z' /= z'S1 ->]. - by apply/(fmeet_idPl (S := S2)); - rewrite ?inE -?f_surj ?in_imfset -?f_meetmorph ?mem_ftop ?fmeetf1. -apply: congr_big => //; move=> z; apply: andb_id2l => zS1. -by rewrite in_imfset //=; congr (_ && _); - rewrite -[RHS](eq_fmeetl (S:=S2)) -?f_meetmorph - ?(inj_in_eq f_inj) ?eq_fmeetl ?mem_fmeet ?inE -?f_surj ?in_imfset. + apply/(fmeet_idPl (S := S2)); + rewrite ?inE -?f_surj ?in_imfset ?mem_ftop //. + by rewrite f_surj -f_meetmorph ?mem_ftop ?fmeetf1. +rewrite big_map [RHS]big_seq_cond; apply:congr_big=> // i; apply/idP/idP. +- case/and3P=> iS1 xi yi; rewrite -f_surj in_imfset ?iS1 //=. + rewrite -!(eq_fmeetl (S:=S2)) -?f_meetmorph ?inE -?f_surj ?in_imfset //. + move: (eq_fmeetl (S:=S1) xS1 iS1) (eq_fmeetl (S:=S1) yS1 iS1). + by rewrite xi yi=> /eqP -> /eqP ->; rewrite !eq_refl. +- case/and4P=> iS1 _; rewrite iS1 /=. + rewrite -2?(eq_fmeetl (S:=S2)) -?f_meetmorph ?inE -?f_surj ?in_imfset //. + move/eqP/f_inj=> /(_ (mem_fmeet xS1 iS1) xS1) <-. + move/eqP/f_inj=> /(_ (mem_fmeet yS1 iS1) yS1) <-. + by rewrite !leIfr. Qed. -(*Lemma comp_fmorphism L (S1 S2 S3 : {finLattice L}) +(*Lemma comp_fmorphism L (S1 S2 S3 : {finLattice T}) (f : {L : fmorphism S1 >-> S2}) (g : {L : fmorphism S2 >-> S3}) : fmorphism L S1 S2 f -> fmorphism L S2 S3 g -> fmorphism L S1 S3 (g \o f). Proof. @@ -2521,30 +2438,30 @@ move=> fm gm; split. - by rewrite /= !fmorph1.*) -(*Canonical fcomp L (S1 S2 S3 : {finLattice L}) +(*Canonical fcomp L (S1 S2 S3 : {finLattice T}) (f : {L : fmorphism S1 >-> S2}) (g : {L : fmorphism S2 >-> S3}) := FMorphism (comp_fmorphism (fmorphismP f) (fmorphismP g)).*) -(*Lemma fmorphism_id L (S : {finLattice L}) : +(*Lemma fmorphism_id L (S : {finLattice T}) : fmorphism L S S id. Proof. by split. Qed. -Canonical fmorph_id L (S : {finLattice L}) := FMorphism (fmorphism_id S).*) +Canonical fmorph_id L (S : {finLattice T}) := FMorphism (fmorphism_id S).*) (*Section Test. -Definition fmorph_of L (S1 S2 : {finLattice L}) +Definition fmorph_of L (S1 S2 : {finLattice T}) (f : {L : fmorphism S1 >-> S2}) & (phantom (T -> T) f) : {L : fmorphism S1 >-> S2} := f. Notation "f %:fmorph" := (fmorph_of (Phantom (T -> T) f)) (at level 0). -Variable (L : {preLattice T}) (S1 S2 S3 : {finLattice L}). +Variable (L : {prelattice T}) (S1 S2 S3 : {finLattice T}). Variable (f : {L : fmorphism S1 >-> S2}) (g : {L : fmorphism S2 >-> S3}). (*Check ((g \o f)%:fmorph : { L : fmorphism S1 >-> S3}).*) (*Check (id %:fmorph : {fmorphism S1 >-> S1}).*) End Test.*) -(*Lemma fcomp_bij L (S1 S2 S3 : {finLattice L}) +(*Lemma fcomp_bij L (S1 S2 S3 : {finLattice T}) (f : {L : fmorphism S1 >-> S2}) (g : {L : fmorphism S2 >-> S3}) : {in S1 & on S2, bijective f} -> {in S2 & on S3, bijective g} -> {in S1 & on S3, bijective (fcomp f g)}. @@ -2559,7 +2476,7 @@ Qed.*) End BijMorphism. (*Section ImMorphism. -Context {T: choiceType} {L : {preLattice T}} (S1 S2 : {finLattice L}). +Context {T: choiceType} {L : {prelattice T}} (S1 S2 : {finLattice T}). Context (f : {L : fmorphism S1 >-> S2}). Definition fmorph_img := f @` (S1 : {fset _}). @@ -2619,13 +2536,13 @@ End IsoFmorphTheory. (* -------------------------------------------------------------------- *) Module Rank. Section ClassDef. -Context (T : choiceType) (L : {preLattice T}) (S : {finLattice L}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). Definition axiom (rank : T -> nat) := [/\ rank \fbot_S = 0%N - , {in S&, {homo rank : x y / x <_L y >-> (x < y)%N}} - & {in S&, forall x z, x <=_L z -> ((rank x).+1 < rank z)%N -> - exists2 y, y \in S & x <_L y <_L z}]. + , {in S&, {homo rank : x y / x < y >-> (x < y)%N}} + & {in S&, forall x z, x <= z -> ((rank x).+1 < rank z)%N -> + exists2 y, y \in S & x < y < z}]. Structure map (phS : phant S) := Pack {apply; _ : axiom apply}. Local Coercion apply : map >-> Funclass. @@ -2650,22 +2567,22 @@ Import Rank.Exports. (* -------------------------------------------------------------------- *) Section RankTheory. -Context (T : choiceType) (L : {preLattice T}) (S : {finLattice L}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). Implicit Types (rk : {rank S}). Lemma rank0 rk : rk \fbot_S = 0%N. Proof. by case: rk => ? []. Qed. -Lemma homo_rank_lt rk : {in S&, {homo rk : x y / x <_L y >-> (x < y)%N}}. +Lemma homo_rank_lt rk : {in S&, {homo rk : x y / x < y >-> (x < y)%N}}. Proof. by case: rk => ? []. Qed. -Lemma homo_rank_le rk : {in S&, {homo rk : x y / x <=_L y >-> (x <= y)%N}}. +Lemma homo_rank_le rk : {in S&, {homo rk : x y / x <= y >-> (x <= y)%N}}. Proof. by apply/(ltW_homo_in_as (f := rk))/homo_rank_lt. Qed. Lemma graded_rank rk : - {in S&, forall x z, x <=_L z -> ((rk x).+1 < rk z)%N -> - exists2 y, y \in S & x <_L y <_L z}. + {in S&, forall x z, x <= z -> ((rk x).+1 < rk z)%N -> + exists2 y, y \in S & x < y < z}. Proof. by case: rk => ? []. Qed. Lemma rank_eq0 rk x : x \in S -> (rk x == 0%N) = (x == \fbot_S). @@ -2683,19 +2600,19 @@ apply: contraTT; rewrite -ltf1 // => /(homo_rank_lt rk xS (mem_ftop S)). by rewrite neq_ltn => ->. Qed. -Lemma rank_gt0 rk x : x \in S -> (0 < rk x)%N = (\fbot_S <_L x). +Lemma rank_gt0 rk x : x \in S -> (0 < rk x)%N = (\fbot_S < x). Proof. move=> xS; rewrite lt0n lt0f //; congr (~~ _); exact: rank_eq0. Qed. Lemma rank_le1 rk x : x \in S -> (rk x <= rk \ftop_S)%N. Proof. by move=> xS; apply/homo_rank_le/lef1 => //; apply/(mem_ftop S). Qed. -Lemma rank_gt1 rk x : x \in S -> (rk x < rk \ftop_S)%N = (x <_L \ftop_S). +Lemma rank_gt1 rk x : x \in S -> (rk x < rk \ftop_S)%N = (x < \ftop_S). Proof. by move=> xS; rewrite ltn_neqAle rank_le1 // andbT ltf1 // rank_eq1. Qed. Lemma rankI rk (x y : T) : x \in S -> y \in S -> - (rk (\fmeet_S x y) <= minn (rk x) (rk y))%N. + (rk (premeet S x y) <= minn (rk x) (rk y))%N. Proof. move=> xS yS; rewrite leq_min !homo_rank_le ?(leIfl, leIfr) //; by apply: mem_fmeet. @@ -2704,7 +2621,7 @@ End RankTheory. (* -------------------------------------------------------------------- *) Section RankInd. -Context (T : choiceType) (L : {preLattice T}) (S : {finLattice L}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). Context (rk : {rank S}) (P : T -> Prop). Hypothesis PH : @@ -2726,11 +2643,11 @@ Arguments rank_ind [_ _ _] _ [_]. (* -------------------------------------------------------------------- *) Section GradedRankS. -Context (T : choiceType) (L : {preLattice T}). -Context (S : {finLattice L}) (rk : {rank S}). +Context {disp : Order.disp_t} {T : prelatticeType disp}. +Context (S : {finLattice T}) (rk : {rank S}). Lemma graded_rankS (x : T) : x \in S -> - (0 < rk x)%N -> exists y : T, [/\ y \in S, y <_L x & (rk y).+1 = rk x]. + (0 < rk x)%N -> exists y : T, [/\ y \in S, y < x & (rk y).+1 = rk x]. Proof. move=> xS; rewrite lt0n rank_eq0 // => nz_x; case/boolP: (rk x < 2)%N. + rewrite ltnS leq_eqVlt ltnS leqn0 rank_eq0 // (negbTE nz_x) orbF. @@ -2750,10 +2667,10 @@ move=> h; have {h}: rk x = ((rk y).+1 + n)%N. case: (n =P 0)%N => [{ih}-> rkxE yS /andP[_ lt_yx]|/eqP nz_n rkxE yS]. + by exists y => //; rewrite rkxE addn0. case/andP => [gt0_y lt_yx]; case: (@graded_rank _ _ _ rk y x) => //. -+ by apply/rltW. + by rewrite rkxE -[X in (X < _)%N]addn0 ltn_add2l lt0n. ++ by apply/ltW. + by rewrite rkxE -[X in (X < _)%N]addn0 ltn_add2l lt0n. move=> z zS /andP[lt_yz lt_zx]; case: (ih z) => //. + by rewrite rkxE leq_subCl addnK; apply: homo_rank_lt. -+ by rewrite (rlt_trans gt0_y lt_yz) lt_zx. ++ by rewrite (lt_trans gt0_y lt_yz) lt_zx. by move=> t [tS lt_tx <-]; exists t. Qed. End GradedRankS. @@ -2761,11 +2678,11 @@ End GradedRankS. (* -------------------------------------------------------------------- *) Section FMorphismRank. -Context (T : choiceType) (L : {preLattice T}) (S1 S2 : {finLattice L}). -Context (f : {fmorphism S1 on L}) (rk1 : {rank S1}) (rk2 : {rank S2}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S1 S2 : {finLattice T}). +Context (f : {fmorphism S1}) (rk1 : {rank S1}) (rk2 : {rank S2}). Lemma rank_morph x : - x \in S1 -> misof L S1 S2 f -> (rk1 x <= rk2 (f x))%N. + x \in S1 -> misof S1 S2 f -> (rk1 x <= rk2 (f x))%N. Proof. move=> + /misofP [f_morph f_inj f_surj]. move: x; apply: (rank_ind rk1) => x xS1 ih. @@ -2779,12 +2696,12 @@ End FMorphismRank. (* -------------------------------------------------------------------- *) Section Atomistic. -Context (T : choiceType) (L : {preLattice T}) (S : {finLattice L}). +Context {disp : Order.disp_t} {T : prelatticeType disp} (S : {finLattice T}). Definition atomistic_r (a : S) := [exists A : {fset S}, [forall x in A, atom S (val x)] - && (a == (\big[join S/bottom S]_(x in A) x))]. + && (a == (\join_(x in A) x))]. Definition atomistic (a : T) := if @idP (a \in S) is ReflectT h then atomistic_r [` h] else false. @@ -2792,7 +2709,7 @@ Definition atomistic (a : T) := Definition coatomistic_r (a : S) := [exists A : {fset S}, [forall x in A, coatom S (val x)] - && (a == (\big[meet S/top S]_(x in A) x))]. + && (a == (\meet_(x in A) x))]. Definition coatomistic (a : T) := if @idP (a \in S) is ReflectT h then coatomistic_r [` h] else false. @@ -2800,7 +2717,7 @@ Definition coatomistic (a : T) := End Atomistic. -Export PreLattice.Exports. +Export Prelattice.Exports. Export FinLatticeStructure.Exports. Export FinTBLatticeStructure.Exports. Export Interval.Exports. diff --git a/src/xbigop.v b/src/xbigop.v index bae844e..7d15f15 100644 --- a/src/xbigop.v +++ b/src/xbigop.v @@ -183,7 +183,14 @@ Hypothesis FP: forall i, P (F i). Lemma big_val (r : seq I) (Q : pred I) : \big[op / x0]_(i <- r | Q i) F i = val (\big[vcop / vx0]_(i <- r | Q i) insubd a (F i)). -Admitted. +Proof. +elim: r=> /=; rewrite ?big_nil // ?val_insubd ?Px0 //. +move=> h l IH; rewrite !big_cons IH. +case: ifP=> //= Qh; rewrite !val_insubd FP Pop //. + by rewrite /in_mem /= FP. +rewrite -IH /in_mem /=. +by apply big_rec=> // i x _; apply: Pop; rewrite /in_mem /= FP. +Qed. End BigOpVal1. @@ -200,7 +207,7 @@ Definition val_fun2 (f : S -> S -> S) (x y: T) := Context {I : Type} {F : I -> S}. -Lemma big_val_foo (r : seq I) (Q : pred I): +Lemma big_val2 (r : seq I) (Q : pred I): val (\big[op / x0]_(i <- r | Q i) F i) = \big[val_fun2 op / val x0]_(i <- r | Q i) val (F i). Proof.