From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 16 Nov 2007 20:49:49 +0000 (+0000)
Subject: Some notes for Enrico.
X-Git-Tag: make_still_working~5807
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ab8f327eb6f492a7780b2309beb495e22f2bba0;p=helm.git

Some notes for Enrico.
---

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 735fe2262..950639fed 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -21,7 +21,7 @@ include "constructive_higher_order_relations.ma".
 
 record excedence : Type ≝ {
   exc_carr:> Type;
-  exc_relation: exc_carr → exc_carr → Prop;
+  exc_relation: exc_carr → exc_carr → Type; (* Big bug: era in Prop!!! *)
   exc_coreflexive: coreflexive ? exc_relation;
   exc_cotransitive: cotransitive ? exc_relation 
 }.
@@ -63,7 +63,7 @@ intros (E); apply (mk_apartness E (apart E));
     intros (H1); apply (H x); cases H1; assumption;
 |2: unfold; intros(x y H); cases H; clear H; [right|left] assumption;
 |3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy);
-    cases Axy (H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
+    cases Axy (H H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
     [left; left|right; left|right; right|left; right] assumption]
 qed.
 
@@ -127,12 +127,14 @@ intros (E a b Lab); cases Lab (LEab Aab);
 cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)  
 qed.
 
+(* CSC: lo avevi gia' dimostrato; ho messo apply! *)
 theorem le_le_to_eq: ∀E:excedence.∀x,y:E. x ≤ y → y ≤ x → x ≈ y.
-intros 6 (E x y L1 L2 H); cases H; [apply (L1 H1)|apply (L2 H1)]
+apply le_antisymmetric;
 qed.
 
+(* CSC: perche' quel casino: bastava intros; assumption! *)
 lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y.
-unfold apart_of_excedence; unfold apart; simplify; intros; assumption;
+intros; assumption;
 qed.
 
 lemma le_rewl: ∀E:excedence.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
@@ -153,4 +155,4 @@ qed.
 lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x.
 intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy);
 apply ap_symmetric; assumption;
-qed.
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma
index cff205ce9..cc7e73928 100644
--- a/helm/software/matita/dama/ordered_groups.ma
+++ b/helm/software/matita/dama/ordered_groups.ma
@@ -32,7 +32,9 @@ qed.
 
 coercion cic:/matita/ordered_groups/og_abelian_group.con.
 
-
+(* CSC: NO! Cosi' e' nel frammento negativo. Devi scriverlo con l'eccedenza!
+   Tutto il resto del file e' da rigirare nel frammento positivo.
+*)
 record ogroup : Type ≝ { 
   og_carr:> pre_ogroup;
   fle_plusr: ∀f,g,h:og_carr. f≤g → f+h≤g+h