**** 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 60c727cebe9ff7967f2971b1916eb34f8c24cd4b..756d02271a62705317140ec464f0c6591b316e75 100644 (file)
--- 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 bb5ed67c5bdeb31bc2a98b000e1e92477eba3c9c..1352988df32cd32d2dcf77699db265a8c4f4c523 100644 (file)
--- 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 da249902bc3a251b80c7c0e445a8785b39fb52e5..118cdd55eaaa3eb8e0f6b5eb35e1461d12dd8e1b 100644 (file)
--- 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 cddf73684d0f6dd3bc7db318fca95afa6d745404..c2510c9c3eff81b1dbf84f6274ce18e3d057a1aa 100644 (file)
--- 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 026f9ebd1ee238ad6e7b7de248fa2f4f415bec30..c33462f8fd90269eedabefac815c2af3f6c1c5c2 100644 (file)
--- 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 =