From 65e8f1ba961ef81c5604168e7f1c891063c1ec76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 17 Oct 2010 09:13:26 +0000 Subject: [PATCH] fixed many scripts that broke for various reasons --- .../matita/nlibrary/algebra/magmas.ma | 4 +-- .../software/matita/nlibrary/arithmetics/R.ma | 28 +++++++++---------- .../software/matita/nlibrary/arithmetics/Z.ma | 4 ++- .../matita/nlibrary/arithmetics/nat.ma | 7 +++-- .../matita/nlibrary/datatypes/list-theory.ma | 2 +- .../software/matita/nlibrary/logic/cologic.ma | 2 +- .../matita/nlibrary/sets/partitions.ma | 4 +-- .../matita/nlibrary/topology/cantor.ma | 7 +++-- .../matita/nlibrary/topology/igft-setoid.ma | 6 ++-- .../matita/nlibrary/topology/igft3.ma | 2 +- .../matita/nlibrary/topology/igft4.ma | 2 +- 11 files changed, 36 insertions(+), 32 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 685d62480..eac55537e 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -41,8 +41,8 @@ nrecord magma_morphism_type (A,B: magma_type) : Type[0] ≝ nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type[0] ≝ { mmmcarr:> magma_morphism_type A B; - mmclosed: ∀x:A. x ∈ mcarr ? Ma → mmmcarr x ∈ mcarr ? Mb - }. + mmclosed: ∀x:A. x ∈ mcarr ? Ma → (fun1 ?? mmmcarr x) ∈ mcarr ? Mb + }. (* XXX bug nelle coercions, fun1 non inserita *) (* ndefinition mm_image: diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma index 60de71dbd..6a74c2054 100644 --- a/helm/software/matita/nlibrary/arithmetics/R.ma +++ b/helm/software/matita/nlibrary/arithmetics/R.ma @@ -231,27 +231,25 @@ nlemma ftcoleqleft: #A; #F; #a; #H; ncases H; /2/. nqed. -alias symbol "I" (instance 7) = "I". -alias symbol "I" (instance 18) = "I". -alias symbol "I" (instance 18) = "I". -alias symbol "I" (instance 18) = "I". +(* XXX: disambiguation crazy *) +alias id "I" = "cic:/matita/ng/topology/igft/I.fix(0,0,2)". nlet corec ftfish_coind (A: Ax_pro) (F: Ω^A) (P: A → CProp[0]) - (Hcorefl: ∀a. P a → a ∈ F) - (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b) - (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x) + (Hcorefl: ∀a:A. P a → a ∈ F) + (Hcoleqleft: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → P b) + (Hcoleqinfinity: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → ∀i:I A b. ∃x:A. x ∈ C A b i ↓ {(a)} ∧ P x) : ∀a:A. P a → a ⋉ F ≝ ?. #a; #H; @ [ /2/ - | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/ + | #b; #H; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); /2/ | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3; - @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //] + @ x; @; //; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); //] nqed. -(*CSC: non serve manco questo (vedi sotto) *) +(*CSC: non serve manco questo (vedi sotto) nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A). #A; //. -nqed. +nqed.*) alias symbol "I" (instance 6) = "I". ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F). @@ -277,9 +275,9 @@ ndefinition Q_to_R: Q → Rd. | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ] ##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon] ##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/ - [ /5/ | #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i - [ #w; nnormalize; - ##| nnormalize; - ] + [ ncases daemon; ##| #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i + [ #w; nnormalize; ncases daemon; + ##| nnormalize; ncases daemon; +##] nqed. diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma index 9045a6d8a..1904f6849 100644 --- a/helm/software/matita/nlibrary/arithmetics/Z.ma +++ b/helm/software/matita/nlibrary/arithmetics/Z.ma @@ -346,6 +346,8 @@ ncut ##|#Hcut;napply Hcut;napply eqZb_to_Prop] nqed. +include "arithmetics/compare.ma". + ndefinition Z_compare : Z → Z → compare ≝ λx,y:Z. match x with @@ -508,7 +510,7 @@ ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). ##[// ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);// ##|//] -##|ncases y;// +##|ncases y;/2/; ##|ncases y ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?); nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);// diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index d4ba1135e..9c420f9ec 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -53,9 +53,10 @@ ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. ndefinition not_zero: nat → Prop ≝ λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ]. - + ntheorem not_eq_O_S : ∀n:nat. O ≠ S n. -#n; napply nmk; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //. +#n; napply nmk; #eqOS; nchange with (not_zero O); +nrewrite > eqOS; //. nqed. ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n. @@ -488,7 +489,7 @@ nelim n; ##[#q; #HleO; (* applica male *) napply (le_n_O_elim ? HleO); napply H; #p; #ltpO; - napply False_ind; /2/; (* 3 *) + napply (False_ind ??); /2/; (* 3 *) ##|#p; #Hind; #q; #HleS; napply H; #a; #lta; napply Hind; napply le_S_S_to_le;/2/; diff --git a/helm/software/matita/nlibrary/datatypes/list-theory.ma b/helm/software/matita/nlibrary/datatypes/list-theory.ma index 14bab26e3..4957feed2 100644 --- a/helm/software/matita/nlibrary/datatypes/list-theory.ma +++ b/helm/software/matita/nlibrary/datatypes/list-theory.ma @@ -20,7 +20,7 @@ ntheorem nil_cons: #A;#l;#a; @; #H; ndestruct; nqed. -ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l. +ntheorem append_nil: ∀A:Type.∀l:list A.l @ [ ] = l. #A;#l;nelim l;//; #a;#l1;#IH;nnormalize;//; nqed. diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma index ca4921607..8b9ed3c15 100644 --- a/helm/software/matita/nlibrary/logic/cologic.ma +++ b/helm/software/matita/nlibrary/logic/cologic.ma @@ -95,7 +95,7 @@ ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2. ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY; @3; - ##[ nrewrite > (ccases (cand (maybe xx) (certain true))); + rewrite > (ccases (cand (maybe xx) (certain true))); nnormalize; @3; @2; diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index b92fe9ab3..3eea50101 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -146,7 +146,7 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; // | nassumption ]##] ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E; - ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2'); + ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq0 A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2'); ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E; nlapply(disjoint … P (f i1) (f i1') ???) [##2,3: napply f_closed; // @@ -179,7 +179,7 @@ ndefinition partition_of_compatible_equivalence_relation: | napply Full_set | napply mk_unary_morphism1 [ #a; napply mk_ext_powerclass - [ napply {x | R x a} + [ napply {x | rel ? R x a} | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon] ##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##] ##| #x; #_; nnormalize; /3/ diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index d3dccb8ee..6a79dd2d8 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -78,7 +78,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)". unification hint 0 ≔ ; x ≟ axs (* -------------- *) ⊢ - S x ≡ A. + S (uax x) ≡ A. (* XXX: bug coercions/ disamb multipasso che ne fa 1 solo*) ntheorem col2_4 : ∀A:uAx.∀a:uax A. a ◃ ∅ → ¬ a ∈ 𝐂 a one. @@ -88,7 +88,8 @@ ntheorem col2_4 : ##] nqed. -ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }. +(* bug interpretazione non aggiunta per ∅ *) +ndefinition Z : Ω^axs ≝ { x | x ◃ (emptyset ?) }. ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V. #A; #a; #U; #V; #HUV; #H; nelim H; /3/; @@ -126,7 +127,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)". unification hint 0 ≔ ; x ≟ caxs (* -------------- *) ⊢ - S x ≡ nat. + S (uax x) ≡ nat. naxiom h : nat → nat. diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma index a4d833cae..276fa5480 100644 --- a/helm/software/matita/nlibrary/topology/igft-setoid.ma +++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma @@ -63,6 +63,7 @@ unification hint 0 ≔ A,B ; (* ----------------------------------- *) ⊢ unary_morphism A B ≡ carr T. +(* ndefinition TYPE : setoid1. @ setoid; @; @@ -111,7 +112,7 @@ interpretation "d" 'd a i j = (nd ? a i j). interpretation "new I" 'I a = (nI ? a). ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }. -(* + nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P. #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g; nqed. @@ -140,6 +141,7 @@ nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[ ##[ @(f e); *) +(* ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A. #A; #a; #i; @ (image … i); #x; #y; #H; @; ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption; @@ -566,4 +568,4 @@ D*) [1]: http://upsilon.cc/~zack/research/publications/notation.pdf D*) -*) +*)*) \ No newline at end of file diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma index 3c7489ba3..4ab768fce 100644 --- a/helm/software/matita/nlibrary/topology/igft3.ma +++ b/helm/software/matita/nlibrary/topology/igft3.ma @@ -214,7 +214,7 @@ ntheorem skipfact_partial: ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O). #n; nelim n; /2/; #m; nelim m; nnormalize - [ #H; @2; nnormalize; //; + [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *) #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ##| #p; #H1; #H2; @2; nnormalize; //; #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; diff --git a/helm/software/matita/nlibrary/topology/igft4.ma b/helm/software/matita/nlibrary/topology/igft4.ma index 9dbbbcf6c..f78b46e79 100644 --- a/helm/software/matita/nlibrary/topology/igft4.ma +++ b/helm/software/matita/nlibrary/topology/igft4.ma @@ -214,7 +214,7 @@ ntheorem skipfact_partial: [ @2; nnormalize; //; #y; *; #a; ncases a | #m; nelim m; nnormalize - [ #H; @2; nnormalize; //; + [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *) #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ##| #p; #H1; #H2; @2; nnormalize; //; #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; -- 2.39.2