From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Jul 2005 12:24:53 +0000 (+0000)
Subject: **** Experimental: ****
X-Git-Tag: V_0_7_2~67
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c12d08acf947823bbfd5909618b042c65ff107de;p=helm.git

**** Experimental: ****

After the disambiguation, if the term is no longer ambiguous, we forget the
environment. In this way we are forced to do more work later (since we have
less aliases), but we have more freedom (since we have less aliases) in the
future disambiguations.
---

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 60c727ceb..756d02271 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -27,18 +27,16 @@ definition Zle : Z \to Z \to Prop \def
   | (pos n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow False
-    | (pos m) \Rightarrow (le n m)
+    | (pos m) \Rightarrow n \leq m
     | (neg m) \Rightarrow False ]
   | (neg n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow True
     | (pos m) \Rightarrow True
-    | (neg m) \Rightarrow (le m n) ]].
+    | (neg m) \Rightarrow m \leq n ]].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
-(*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
-alias symbol "leq" (instance 0) = "integer 'less or equal to'".
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -51,18 +49,16 @@ definition Zlt : Z \to Z \to Prop \def
   | (pos n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow False
-    | (pos m) \Rightarrow (lt n m)
+    | (pos m) \Rightarrow n<m
     | (neg m) \Rightarrow False ]
   | (neg n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow True
     | (pos m) \Rightarrow True
-    | (neg m) \Rightarrow (lt m n) ]].
+    | (neg m) \Rightarrow m<n ]].
     
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
-(*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
-alias symbol "lt" (instance 0) = "integer 'less than'".
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with \forall x:Z. x < x \to False.
@@ -95,21 +91,25 @@ definition Z_compare : Z \to Z \to compare \def
     | (pos m) \Rightarrow LT
     | (neg m) \Rightarrow nat_compare m n ]].
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_neg_neg_to_lt: 
 \forall n,m:nat. neg n < neg m \to lt m n.
 intros.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
 intros.
 simplify.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_pos_pos_to_lt: 
 \forall n,m:nat. pos n < pos m \to lt n m.
 intros.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
 intros.
 simplify.apply H.
@@ -127,13 +127,15 @@ simplify.exact I.
 simplify.exact I.
 elim y. simplify.exact I.
 simplify. 
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+  per via delle coercions! *)
 cut match (nat_compare n1 n) with
-[ LT \Rightarrow (lt n1 n)
-| EQ \Rightarrow (eq nat n1 n)
-| GT \Rightarrow (lt n n1)] \to 
+[ LT \Rightarrow n1<n
+| EQ \Rightarrow n1=n
+| GT \Rightarrow n<n1] \to 
 match (nat_compare n1 n) with
 [ LT \Rightarrow (le (S n1) n)
-| EQ \Rightarrow (eq Z (neg n) (neg n1))
+| EQ \Rightarrow neg n = neg n1
 | GT \Rightarrow (le (S n) n1)]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n1 n).
@@ -144,13 +146,15 @@ simplify.exact I.
 elim y.simplify.exact I.
 simplify.exact I.
 simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+  per via delle coercions! *)
 cut match (nat_compare n n1) with
-[ LT \Rightarrow (lt n n1)
-| EQ \Rightarrow (eq nat n n1)
-| GT \Rightarrow (lt n1 n)] \to 
+[ LT \Rightarrow n<n1
+| EQ \Rightarrow n=n1
+| GT \Rightarrow n1<n] \to 
 match (nat_compare n n1) with
 [ LT \Rightarrow (le (S n) n1)
-| EQ \Rightarrow (eq Z (pos n) (pos n1))
+| EQ \Rightarrow pos n = pos n1
 | GT \Rightarrow (le (S n1) n)]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n n1).
diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index bb5ed67c5..1352988df 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -31,14 +31,17 @@ definition Ztimes :Z \to Z \to Z \def
          | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
          | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
          
-theorem Ztimes_z_OZ:  \forall z:Z. eq Z (Ztimes z OZ) OZ.
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
+
+theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-
+(*CSC: da qui in avanti niente notazione *)
 (*
 theorem symmetric_Ztimes : symmetric Z Ztimes.
 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
@@ -251,21 +254,4 @@ qed.
 
 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
 \def associative_Zplus.
-
-definition Zopp : Z \to Z \def
-\lambda x:Z. match x with
-[ OZ \Rightarrow OZ
-| (pos n) \Rightarrow (neg n)
-| (neg n) \Rightarrow (pos n) ].
-
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
-intro.elim x.
-apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-qed.
 *)
diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index da249902b..118cdd55e 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -51,8 +51,8 @@ match z with
 
 theorem OZ_test_to_Prop :\forall z:Z.
 match OZ_test z with
-[true \Rightarrow eq Z z OZ 
-|false \Rightarrow \lnot (eq Z z OZ)].
+[true \Rightarrow z=OZ 
+|false \Rightarrow \lnot (z=OZ)].
 intros.elim z.
 simplify.reflexivity.
 simplify.intros.
@@ -87,14 +87,14 @@ definition Zpred \def
 	  | (S p) \Rightarrow pos p]
 | (neg n) \Rightarrow neg (S n)].
 
-theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
+theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
 intros.elim z.reflexivity.
 elim n.reflexivity.
 reflexivity.
 reflexivity.
 qed.
 
-theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
+theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
 intros.elim z.reflexivity.
 reflexivity.
 elim n.reflexivity.
@@ -127,7 +127,7 @@ definition Zplus :Z \to Z \to Z \def
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).
          
-theorem Zplus_z_OZ:  \forall z:Z. Zplus z OZ = z.
+theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
@@ -136,7 +136,7 @@ qed.
 
 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
 
-theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
+theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
 elim y.simplify.reflexivity.
 simplify.
@@ -154,7 +154,7 @@ simplify. reflexivity.
 simplify.rewrite < sym_plus.reflexivity.
 qed.
 
-theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
+theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
 intros.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
@@ -162,7 +162,7 @@ elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
+theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
 intros.elim z.
 simplify.reflexivity.
 elim n.simplify.reflexivity.
@@ -171,7 +171,7 @@ simplify.reflexivity.
 qed.
 
 theorem Zplus_pos_pos:
-\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
+\forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
 intros.
 elim n.elim m.
 simplify.reflexivity.
@@ -184,12 +184,12 @@ rewrite < plus_n_Sm.reflexivity.
 qed.
 
 theorem Zplus_pos_neg:
-\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
+\forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 intros.reflexivity.
 qed.
 
 theorem Zplus_neg_pos :
-\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
+\forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
 intros.
 elim n.elim m.
 simplify.reflexivity.
@@ -200,7 +200,7 @@ simplify.reflexivity.
 qed.
 
 theorem Zplus_neg_neg:
-\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
+\forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
 intros.
 elim n.elim m.
 simplify.reflexivity.
@@ -211,7 +211,7 @@ simplify.rewrite > plus_n_Sm.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_Zpred:
-\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
+\forall x,y. x+y = (Zsucc x)+(Zpred y).
 intros.
 elim x. elim y.
 simplify.reflexivity.
@@ -230,15 +230,15 @@ apply Zplus_pos_pos.
 qed.
 
 theorem Zplus_Zsucc_pos_pos : 
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
+\forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
 intros.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_pos_neg: 
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
+\forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
 intros.
 apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
+(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -252,10 +252,10 @@ elim H.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
+\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)).
 intros.
 apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
+(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -269,10 +269,10 @@ reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_pos: 
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
+\forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 intros.
 apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
+(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))).
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -286,7 +286,7 @@ rewrite < (Zplus_neg_pos ? (S m1)).
 reflexivity.
 qed.
 
-theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
+theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
 intros.elim x.elim y.
 simplify. reflexivity.
 rewrite < Zsucc_Zplus_pos_O.reflexivity.
@@ -300,9 +300,9 @@ apply Zplus_Zsucc_pos_neg.
 apply Zplus_Zsucc_pos_pos.
 qed.
 
-theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
+theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
 intros.
-cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
+cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y).
 rewrite > Hcut.
 rewrite > Zplus_Zsucc.
 rewrite > Zpred_Zsucc.
@@ -313,16 +313,16 @@ qed.
 
 
 theorem associative_Zplus: associative Z Zplus.
-change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). 
+change with \forall x,y,z:Z. (x + y) + z = x + (y + z). 
 (* simplify. *)
 intros.elim x.simplify.reflexivity.
-elim n.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
+elim n.rewrite < (Zpred_Zplus_neg_O (y+z)).
 rewrite < (Zpred_Zplus_neg_O y).
 rewrite < Zplus_Zpred.
 reflexivity.
 rewrite > Zplus_Zpred (neg n1).
 rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred (Zplus (neg n1) y).
+rewrite > Zplus_Zpred ((neg n1)+y).
 apply eq_f.assumption.
 elim n.rewrite < Zsucc_Zplus_pos_O.
 rewrite < Zsucc_Zplus_pos_O.
@@ -330,11 +330,11 @@ rewrite > Zplus_Zsucc.
 reflexivity.
 rewrite > Zplus_Zsucc (pos n1).
 rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc (Zplus (pos n1) y).
+rewrite > Zplus_Zsucc ((pos n1)+y).
 apply eq_f.assumption.
 qed.
 
-variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
+variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
 \def associative_Zplus.
 
 (* Zopp *)
@@ -344,7 +344,10 @@ definition Zopp : Z \to Z \def
 | (pos n) \Rightarrow (neg n)
 | (neg n) \Rightarrow (pos n) ].
 
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/z/Zopp.con x).
+
+theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ.
 intro.elim x.
 apply refl_eq.
 simplify.
diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index cddf73684..c2510c9c3 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -71,6 +71,12 @@ TODO
   - riattaccare hbugs (brrr...) -> Zack
 
   GUI LOGICA
+  - disambiguazione: attualmente io (CSC) ho committato la versione di
+    disambiguate.ml che NON ricorda gli alias in caso di disambiguazione
+    univoca (senza scelte per l'utente). [ cercare commento "Experimental" ]
+    Il problema di questa soluzione e' che rallenta in maniera significativa
+    l'esecuzione degli script. DOMANDA: quanto costano le fasi di
+    fetch/decode/execute delle linee dello script?
   - matitamake foo/a.ma non funziona; bisogna chiamarlo con
     matitamake /x/y/z/foo/a.ma
   - notazione -> Luca e Zack
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 026f9ebd1..c33462f8f 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -822,9 +822,13 @@ module Make (C: Callbacks) =
         let res =
          match aux current_env todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
-         | [ e,me,t,u ] as l ->
+         | [ e,me,t,u ] ->
              debug_print "UNA SOLA SCELTA";
-             [ e,me,t,u]
+             (* Experimental: we forget the environment [e] since we are able
+                to recompute it. In this way we are forced to do more work
+                later (since we have less aliases), but we have more freedom
+                (since we have less aliases) in the future disambiguations. *)
+             [ current_env,me,t,u]
          | l ->
              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
              let choices =