From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 May 2008 14:27:41 +0000 (+0000)
Subject: more work on dama
X-Git-Tag: make_still_working~5098
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=730b049302205da43d5fbe8c4450460d85e1ece5;p=helm.git

more work on dama
---

diff --git a/helm/software/matita/contribs/dama/Makefile b/helm/software/matita/contribs/dama/Makefile
index c2cc976d4..7054f4ef0 100644
--- 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 c84382e85..743803cd6 100644
--- 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 3e255f792..77abdf673 100644
--- 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 757de3e3b..715fb5bdb 100644
--- 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.
+
+