X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fexcess.ma;h=f29c5a362bca6ed324cdba86949c2f406f2d7f37;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=9068d297b215aea05faa417f2f3e365146a994c8;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/excess.ma b/helm/software/matita/contribs/dama/dama_duality/excess.ma
index 9068d297b..f29c5a362 100644
--- a/helm/software/matita/contribs/dama/dama_duality/excess.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/excess.ma
@@ -26,7 +26,7 @@ record excess_base : Type ≝ {
   exc_cotransitive: cotransitive ? exc_excess 
 }.
 
-interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). 
+interpretation "Excess base excess" 'nleq a b = (exc_excess _ a b). 
 
 (* E(#,≰) → E(#,sym(≰)) *)
 lemma make_dual_exc: excess_base → excess_base.
@@ -62,7 +62,7 @@ record apartness : Type ≝ {
 }.
 
 notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "apartness" 'apart x y = (cic:/matita/excess/ap_apart.con _ x y).
+interpretation "apartness" 'apart x y = (ap_apart _ x y).
 
 definition apartness_of_excess_base: excess_base → apartness.
 intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));  
@@ -90,7 +90,7 @@ qed.
 coercion cic:/matita/excess/exc_ap.con.
 
 interpretation "Excess excess_" 'nleq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b).
+ (exc_excess (excess_base_OF_excess_1 _) a b).
 
 record excess : Type ≝ {
   excess_carr:> excess_;
@@ -99,20 +99,20 @@ record excess : Type ≝ {
 }.
 
 interpretation "Excess excess" 'nleq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+ (exc_excess (excess_base_OF_excess1 _) a b).
  
 interpretation "Excess (dual) excess" 'ngeq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+ (exc_excess (excess_base_OF_excess _) a b).
 
 definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
 
 definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b).
 
 interpretation "Excess less or equal than" 'leq a b = 
- (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+ (le (excess_base_OF_excess1 _) a b).
 
 interpretation "Excess less or equal than" 'geq a b = 
- (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+ (le (excess_base_OF_excess _) a b).
 
 lemma le_reflexive: ∀E.reflexive ? (le E).
 unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
@@ -126,9 +126,9 @@ qed.
 definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
 
 notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.    
-interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b). 
-interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). 
-interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). 
+interpretation "Apartness alikeness" 'napart a b = (eq _ a b). 
+interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 _) a b). 
+interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess _) a b). 
 
 lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
 intros (E); unfold; intros (x); apply ap_coreflexive; 
@@ -153,7 +153,7 @@ lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
   λE,x,y,z.eq_trans_ E x z y.
 
 notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
-interpretation "eq_rew" 'eqrewrite = (cic:/matita/excess/eq_trans.con _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
 
 alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
 lemma le_antisymmetric: 
@@ -164,7 +164,7 @@ qed.
 
 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
 
-interpretation "ordered sets less than" 'lt a b = (cic:/matita/excess/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
 
 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
@@ -197,9 +197,9 @@ intro Xyz; apply Exy; apply exc2ap; left; assumption;
 qed.
 
 notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (cic:/matita/excess/le_rewl.con _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
 notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (cic:/matita/excess/le_rewr.con _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
 
 lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
 intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
@@ -212,9 +212,9 @@ apply ap_symmetric; assumption;
 qed.
 
 notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (cic:/matita/excess/ap_rewl.con _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (cic:/matita/excess/ap_rewr.con _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
 
 alias symbol "napart" = "Apartness alikeness".
 lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
@@ -228,9 +228,9 @@ elim (Exy); apply exc2ap; left; assumption;
 qed.
 
 notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}.
-interpretation "exc_rewl" 'excessrewritel = (cic:/matita/excess/exc_rewl.con _ _ _).
+interpretation "exc_rewl" 'excessrewritel = (exc_rewl _ _ _).
 notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}.
-interpretation "exc_rewr" 'excessrewriter = (cic:/matita/excess/exc_rewr.con _ _ _).
+interpretation "exc_rewr" 'excessrewriter = (exc_rewr _ _ _).
 
 lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
 intros (A x y z E H); split; elim H; 
@@ -243,9 +243,9 @@ intros (A x y z E H); split; elim H;
 qed.
 
 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/excess/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/excess/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
 
 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]