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.
| (pos n) \Rightarrow
match y with
[ OZ \Rightarrow False
| (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 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: 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.
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
| (pos n) \Rightarrow
match y with
[ OZ \Rightarrow False
| (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 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: 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.
theorem irreflexive_Zlt: irreflexive Z Zlt.
change with \forall x:Z. x < x \to False.
| (pos m) \Rightarrow LT
| (neg m) \Rightarrow nat_compare m n ]].
| (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.
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.
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.
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.
theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m.
intros.
simplify.apply H.
simplify.exact I.
elim y. simplify.exact I.
simplify.
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
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)
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).
| GT \Rightarrow (le (S n) n1)].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n1 n).
elim y.simplify.exact I.
simplify.exact I.
simplify.
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
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)
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).
| GT \Rightarrow (le (S n1) n)].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n n1).
| (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
| (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
| (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.
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).
(*
theorem symmetric_Ztimes : symmetric Z Ztimes.
change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
\def associative_Zplus.
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.
theorem OZ_test_to_Prop :\forall z:Z.
match OZ_test 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.
intros.elim z.
simplify.reflexivity.
simplify.intros.
| (S p) \Rightarrow pos p]
| (neg n) \Rightarrow neg (S n)].
| (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.
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.
intros.elim z.reflexivity.
reflexivity.
elim n.reflexivity.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).
(*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.
intro.elim z.
simplify.reflexivity.
simplify.reflexivity.
(* theorem symmetric_Zplus: symmetric Z Zplus. *)
(* 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.
intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
elim y.simplify.reflexivity.
simplify.
simplify.rewrite < sym_plus.reflexivity.
qed.
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.
intros.elim z.
simplify.reflexivity.
simplify.reflexivity.
simplify.reflexivity.
qed.
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.
intros.elim z.
simplify.reflexivity.
elim n.simplify.reflexivity.
qed.
theorem Zplus_pos_pos:
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.
intros.
elim n.elim m.
simplify.reflexivity.
qed.
theorem Zplus_pos_neg:
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 :
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.
intros.
elim n.elim m.
simplify.reflexivity.
qed.
theorem Zplus_neg_neg:
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.
intros.
elim n.elim m.
simplify.reflexivity.
qed.
theorem Zplus_Zsucc_Zpred:
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.
intros.
elim x. elim y.
simplify.reflexivity.
qed.
theorem Zplus_Zsucc_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:
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))).
-(\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.
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
qed.
theorem Zplus_Zsucc_neg_neg :
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)).
-(\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.
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
qed.
theorem Zplus_Zsucc_neg_pos:
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)).
-(\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.
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
-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.
intros.elim x.elim y.
simplify. reflexivity.
rewrite < Zsucc_Zplus_pos_O.reflexivity.
apply Zplus_Zsucc_pos_pos.
qed.
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).
-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.
rewrite > Hcut.
rewrite > Zplus_Zsucc.
rewrite > Zpred_Zsucc.
theorem associative_Zplus: associative Z Zplus.
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.
(* 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 < (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.
apply eq_f.assumption.
elim n.rewrite < Zsucc_Zplus_pos_O.
rewrite < Zsucc_Zplus_pos_O.
reflexivity.
rewrite > Zplus_Zsucc (pos n1).
rewrite > Zplus_Zsucc (pos n1).
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.
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 *)
\def associative_Zplus.
(* Zopp *)
| (pos n) \Rightarrow (neg n)
| (neg n) \Rightarrow (pos n) ].
| (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.
intro.elim x.
apply refl_eq.
simplify.
- riattaccare hbugs (brrr...) -> Zack
GUI LOGICA
- 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
- matitamake foo/a.ma non funziona; bisogna chiamarlo con
matitamake /x/y/z/foo/a.ma
- notazione -> Luca e Zack
let res =
match aux current_env todo_dom base_univ with
| [] -> raise NoWellTypedInterpretation
let res =
match aux current_env todo_dom base_univ with
| [] -> raise NoWellTypedInterpretation
debug_print "UNA SOLA SCELTA";
debug_print "UNA SOLA SCELTA";
+ (* 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 =
| l ->
debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
let choices =