more work on dama

diff --git a/helm/software/matita/contribs/dama/Makefile b/helm/software/matita/contribs/dama/Makefile
index c2cc976d41bef6da55f04323c35a6b136326cf26..7054f4ef0f4eb4a3b9d478205aa2818492f641c5 100644 (file)
--- a/helm/software/matita/contribs/dama/Makefile
+++ b/helm/software/matita/contribs/dama/Makefile
@@ -1,6 +1,6 @@
 GOALS = all opt clean clean.opt
 
-DEVELS = dama dama_didactic
+DEVELS = dama dama_didactic dama_duality
 
 $(GOALS): 
        @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) 

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index c84382e85cd1fa1205e64e1ca35f1d2933b42943..743803cd6c439e781f127672db726540592bb43f 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -30,13 +30,7 @@ interpretation "constructive and" 'and x y =
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
-inductive ex (A:Type) (P:A→Prop) : Type ≝ (* ??? *)
-  ex_intro: ∀w:A. P w → ex A P.
-
-interpretation "constructive exists" 'exists \eta.x =
-  (cic:/matita/dama/cprop_connectives/ex.ind#xpointer(1/1) _ x).
-  
-interpretation "constructive exists (Type)" 'exists \eta.x =
+interpretation "CProp exists" 'exists \eta.x =
   (cic:/matita/dama/cprop_connectives/exT.ind#xpointer(1/1) _ x).
 
 inductive False : CProp ≝ .

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 3e255f79263ca5eb5785a2a1e6a8e347ca98ada0..77abdf673f7476c52228c9f071408fab4eed6d8b 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -4,6 +4,6 @@ ordered_set.ma cprop_connectives.ma
 cprop_connectives.ma logic/equality.ma
 bishop_set_rewrite.ma bishop_set.ma
 sequence.ma nat/nat.ma
-supremum.ma ordered_set.ma sequence.ma
+supremum.ma bishop_set.ma ordered_set.ma sequence.ma
 logic/equality.ma 
 nat/nat.ma 

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 757de3e3bf6bc9bfa2bf71b81476291c21d97c8b..715fb5bdbcd5f50f87afaef34b4d27ce48a4222c 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -48,6 +48,12 @@ include "bishop_set.ma".
   
 lemma uniq_supremum: 
   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
-    t1 is_upper_bound s → t2 is_upper_bound s → t1 ≈ t2.
-intros (O s t1 t2 Ht1 Ht2); apply le_le_eq; cases Ht1; cases Ht2;
+    t1 is_strong_sup s → t2 is_strong_sup s → t1 ≈ t2.
+intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2); 
+apply le_le_eq; intro X;
+[1: cases (H1 ? X); apply (U2 w); assumption
+|2: cases (H2 ? X); apply (U1 w); assumption]
+qed.
+
+