From c12d08acf947823bbfd5909618b042c65ff107de Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 Jul 2005 12:24:53 +0000 Subject: [PATCH] **** 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. --- helm/matita/library/Z/orders.ma | 36 ++++++----- helm/matita/library/Z/times.ma | 24 ++------ helm/matita/library/Z/z.ma | 61 ++++++++++--------- helm/matita/matita.txt | 6 ++ helm/ocaml/cic_disambiguation/disambiguate.ml | 8 ++- 5 files changed, 69 insertions(+), 66 deletions(-) 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 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 = -- 2.39.2