X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Flattices.ma;h=8f2aa763da3eb35aba1e8521c24f7bc06ec19f46;hb=a3f4c0a8b4328cb9a9fe3b4c2e577be2a258675c;hp=0af365d00c662061440a2bc381b1fa646cc1c0c1;hpb=dd3157d36216486d914a97cfff7a9cd34f009ffe;p=helm.git

diff --git a/matita/dama/lattices.ma b/matita/dama/lattices.ma
index 0af365d00..8f2aa763d 100644
--- a/matita/dama/lattices.ma
+++ b/matita/dama/lattices.ma
@@ -16,93 +16,62 @@ set "baseuri" "cic:/matita/lattices/".
 
 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