1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/lattices/".
17 include "ordered_sets.ma".
19 record pre_lattice (C:Type) : Type \def
24 definition carrier_of_lattice ≝ λC:Type.λL:pre_lattice C.C.
26 coercion cic:/matita/lattices/carrier_of_lattice.con.
28 definition join : ∀C.∀L:pre_lattice C.L→L→L ≝ join_.
29 definition meet : ∀C.∀L:pre_lattice C.L→L→L ≝ meet_.
31 interpretation "Lattice meet" 'and a b =
32 (cic:/matita/lattices/meet.con _ _ a b).
34 interpretation "Lattice join" 'or a b =
35 (cic:/matita/lattices/join.con _ _ a b).
37 record is_lattice (C:Type) (L:pre_lattice C) : Prop \def
38 { (* abelian semigroup properties *)
39 l_comm_j: symmetric ? (join ? L);
40 l_associative_j: associative ? (join ? L);
41 l_comm_m: symmetric ? (meet ? L);
42 l_associative_m: associative ? (meet ? L);
43 (* other properties *)
44 l_adsorb_j_m: ∀f,g:L. (f ∨ f ∧ g) = f;
45 l_adsorb_m_j: ∀f,g:L. (f ∧ (f ∨ g)) = f
48 record lattice (C:Type) : Type \def
49 { l_pre_lattice:> pre_lattice C;
50 l_lattice_properties:> is_lattice ? l_pre_lattice
53 definition le \def λC:Type.λL:lattice C.λf,g:L. (f ∧ g) = f.
55 definition ordered_set_of_lattice: ∀C.lattice C → ordered_set C.
58 [ apply mk_pre_ordered_set;
60 | apply mk_is_order_relation;
66 change in x with (carrier_of_lattice ? l);
67 rewrite < (l_adsorb_j_m ? ? l ? x) in ⊢ (? ? (? ? ? ? %) ?);
68 rewrite > l_adsorb_m_j;
70 | apply (l_lattice_properties ? l)
78 rewrite > (l_associative_m ? ? l);
81 | unfold antisimmetric;
87 rewrite > (l_comm_m ? ? l);
93 coercion cic:/matita/lattices/ordered_set_of_lattice.con.
96 interpretation "Lattice le" 'leq a b =
97 (cic:/matita/integration_algebras/le.con _ _ a b).
99 definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g.
101 interpretation "Lattice lt" 'lt a b =
102 (cic:/matita/integration_algebras/lt.con _ _ a b).
105 (* The next coercion introduces a cycle in the coercion graph with
106 unexpected bad results
107 coercion cic:/matita/integration_algebras/carrier_of_lattice.con.