yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

[helm.git] / helm / software / matita / dama / metric_lattice.ma

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 40f3d41eb8f32fa057cf46faf463fe2f045f5381..a2d25734217ead71fd14871f92b2264dd0987d01 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -12,18 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 include "metric_space.ma".
 include "lattice.ma".
 
 record mlattice_ (R : todgroup) : Type ≝ {
   ml_mspace_: metric_space R;
-  ml_lattice_: lattice;
-  ml_with_: ms_carr ? ml_mspace_ = l_carr ml_lattice_;
-  ml_with2_: l_carr ml_lattice_ = apart_of_metric_space ? ml_mspace_ 
+  ml_lattice:> lattice;
+  ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice) 
 }.
 
+(*
 lemma ml_lattice: ∀R.mlattice_ R → lattice.
 intros (R ml); apply (mk_lattice (apart_of_metric_space ? (ml_mspace_ ? ml))); try unfold eq;
 cases (ml_with2_ ? ml);
@@ -36,13 +34,15 @@ cases (ml_with2_ ? ml);
 qed.
 
 coercion cic:/matita/metric_lattice/ml_lattice.con.
+*)
 
 lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
-intros (R ml); apply (mk_metric_space R ml);
+intros (R ml); apply (mk_metric_space R (apart_of_excess ml)); 
+unfold apartness_OF_mlattice_; 
+[rewrite < (ml_with_ ? ml); apply (metric ? (ml_mspace_ ? ml))]
 cases (ml_with_ ? ml); simplify;
-[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml));
-|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml));
-|apply (mtineq ? (ml_mspace_ ? ml))]
+[apply (mpositive ? (ml_mspace_ ? ml));|apply (mreflexive ? (ml_mspace_ ? ml));
+|apply (msymmetric ? (ml_mspace_ ? ml));|apply (mtineq ? (ml_mspace_ ? ml))]
 qed.
 
 coercion cic:/matita/metric_lattice/ml_mspace.con.