include "ordered_sets.ma".
-record pre_lattice (C:Type) : Type \def
- { join_: C → C → C;
- meet_: C → C → C
+record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def
+ { (* abelian semigroup properties *)
+ l_comm_j: symmetric ? join;
+ l_associative_j: associative ? join;
+ l_comm_m: symmetric ? meet;
+ l_associative_m: associative ? meet;
+ (* other properties *)
+ l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
+ l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
}.
-definition carrier_of_lattice ≝ λC:Type.λL:pre_lattice C.C.
-
-coercion cic:/matita/lattices/carrier_of_lattice.con.
-
-definition join : ∀C.∀L:pre_lattice C.L→L→L ≝ join_.
-definition meet : ∀C.∀L:pre_lattice C.L→L→L ≝ meet_.
+record lattice : Type \def
+ { l_carrier:> Type;
+ l_join: l_carrier→l_carrier→l_carrier;
+ l_meet: l_carrier→l_carrier→l_carrier;
+ l_lattice_properties:> is_lattice ? l_join l_meet
+ }.
interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattices/meet.con _ _ a b).
+ (cic:/matita/lattices/l_meet.con _ a b).
interpretation "Lattice join" 'or a b =
- (cic:/matita/lattices/join.con _ _ a b).
-
-record is_lattice (C:Type) (L:pre_lattice C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? (join ? L);
- l_associative_j: associative ? (join ? L);
- l_comm_m: symmetric ? (meet ? L);
- l_associative_m: associative ? (meet ? L);
- (* other properties *)
- l_adsorb_j_m: ∀f,g:L. (f ∨ f ∧ g) = f;
- l_adsorb_m_j: ∀f,g:L. (f ∧ (f ∨ g)) = f
- }.
-
-record lattice (C:Type) : Type \def
- { l_pre_lattice:> pre_lattice C;
- l_lattice_properties:> is_lattice ? l_pre_lattice
- }.
+ (cic:/matita/lattices/l_join.con _ a b).
-definition le \def λC:Type.λL:lattice C.λf,g:L. (f ∧ g) = f.
+definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-definition ordered_set_of_lattice: ∀C.lattice C → ordered_set C.
- intros;
+definition ordered_set_of_lattice: lattice → ordered_set.
+ intros (L);
apply mk_ordered_set;
- [ apply mk_pre_ordered_set;
- apply (le ? l)
+ [2: apply (le L)
+ | skip
| apply mk_is_order_relation;
[ unfold reflexive;
intros;
unfold;
- simplify;
- unfold le;
- change in x with (carrier_of_lattice ? l);
- rewrite < (l_adsorb_j_m ? ? l ? x) in ⊢ (? ? (? ? ? ? %) ?);
+ rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
rewrite > l_adsorb_m_j;
[ reflexivity
- | apply (l_lattice_properties ? l)
+ | apply (l_lattice_properties L)
]
| intros;
unfold transitive;
- simplify;
unfold le;
intros;
rewrite < H;
- rewrite > (l_associative_m ? ? l);
+ rewrite > (l_associative_m ? ? ? L);
rewrite > H1;
reflexivity
| unfold antisimmetric;
- unfold os_le;
- simplify;
unfold le;
intros;
rewrite < H;
- rewrite > (l_comm_m ? ? l);
+ rewrite > (l_comm_m ? ? ? L);
assumption
]
]
qed.
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-
-(*
-interpretation "Lattice le" 'leq a b =
- (cic:/matita/integration_algebras/le.con _ _ a b).
-
-definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g.
-
-interpretation "Lattice lt" 'lt a b =
- (cic:/matita/integration_algebras/lt.con _ _ a b).
-*)
-
-(* The next coercion introduces a cycle in the coercion graph with
- unexpected bad results
-coercion cic:/matita/integration_algebras/carrier_of_lattice.con.
-*)
+coercion cic:/matita/lattices/ordered_set_of_lattice.con.
\ No newline at end of file