From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Jan 2010 11:46:06 +0000 (+0000)
Subject: // in place of nauto everywhere
X-Git-Tag: make_still_working~3109
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34311f3f810eb893b865d1893eae1cf62cd490b4;p=helm.git

// in place of nauto everywhere
---

diff --git a/helm/software/matita/nlibrary/algebra/bool.ma b/helm/software/matita/nlibrary/algebra/bool.ma
index 0e171fc58..c3a7c6781 100644
--- a/helm/software/matita/nlibrary/algebra/bool.ma
+++ b/helm/software/matita/nlibrary/algebra/bool.ma
@@ -24,7 +24,7 @@ nlemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a
 nqed.
 
 nlemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
-#A; #a; #P; #p; #b; #E; ncases E in p; nauto;
+#A; #a; #P; #p; #b; #E; ncases E in p; //;
 nqed. 
 
 nlemma csc : 
diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 6ccfa6259..73abc9f09 100644
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -23,13 +23,13 @@ ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
 //; nqed.
 
 ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
-//; nqed.
+#A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
 
 ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
-/2/; nqed.
+#A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
 
 ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
-//; nqed.
+#A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
 
 (*
 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
@@ -39,4 +39,5 @@ qed. *)
 
 ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
-//; nqed.
\ No newline at end of file
+#A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
+nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 2e5130c4c..9f5c28b24 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,34 +1,40 @@
-algebra/bool.ma logic/connectives.ma
 overlap/o-algebra.ma sets/categories2.ma
+algebra/bool.ma logic/connectives.ma
 algebra/abelian_magmas.ma algebra/magmas.ma
-logic/destruct_bb.ma logic/equality.ma
+basics/functions.ma Plogic/connectives.ma Plogic/equality.ma
+Plogic/connectives.ma Plogic/equality.ma
+arithmetics/nat.ma basics/eq.ma basics/functions.ma
 datatypes/bool.ma logic/pts.ma
+logic/destruct_bb.ma logic/equality.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
 sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
 logic/cprop.ma hints_declaration.ma sets/setoids1.ma
 topology/igft.ma logic/equality.ma sets/sets.ma
-algebra/magmas.ma sets/sets.ma
 nat/minus.ma nat/order.ma
+algebra/magmas.ma sets/sets.ma
 hints_declaration.ma logic/pts.ma
 Plogic/equality.ma logic/pts.ma
 properties/relations1.ma logic/pts.ma
-sets/categories.ma sets/sets.ma
 algebra/unital_magmas.ma algebra/magmas.ma
 nat/compare.ma datatypes/bool.ma nat/order.ma
+sets/categories.ma sets/sets.ma
 properties/relations2.ma logic/pts.ma
 nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
 logic/connectives.ma logic/pts.ma
+basics/relations.ma Plogic/connectives.ma
 topology/igft-setoid.ma sets/sets.ma
 sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma
 sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-logic/pts.ma 
-nat/order.ma nat/nat.ma sets/sets.ma
-nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
 datatypes/pairs.ma logic/pts.ma
-sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma
+nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
+nat/order.ma nat/nat.ma sets/sets.ma
+logic/pts.ma 
 topology/cantor.ma nat/nat.ma topology/igft.ma
-sets/setoids2.ma properties/relations2.ma sets/setoids1.ma
+sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma
 nat/big_ops.ma algebra/magmas.ma nat/order.ma
-topology/igft2.ma topology/igft.ma
+sets/setoids2.ma properties/relations2.ma sets/setoids1.ma
+topology/igft2.ma arithmetics/nat.ma topology/igft.ma
+topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
 properties/relations.ma logic/pts.ma
-sets/setoids.ma logic/connectives.ma properties/relations.ma
+basics/eq.ma basics/relations.ma
+sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma
diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index c64b65118..269cfc765 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -14,6 +14,12 @@
 
 include "logic/equality.ma".
 
+ninductive unit: Type[0] ≝ k: unit.
+
+ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
+
+nlemma foo: true = false → False. #H; ndestruct;
+
 (* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
                ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
 #T;#a;#b;#e;#P;#H;
diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 115d1f643..49d259d5d 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -69,7 +69,7 @@ ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
  #s; #s1; @ (unary_morphism1 s s1); @
      [ #f; #g; napply (∀a:s. f a = g a)
      | #x; #a; napply refl1
-     | #x; #y; #H; #a; napply sym1; nauto
+     | #x; #y; #H; #a; napply sym1; //
      | #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##]
 nqed.
 
diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index bd8a04a22..e7f9a5a15 100644
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -7,14 +7,14 @@ ntheorem axiom_cond: ∀A:Ax.∀a:A.∀i:𝐈 a.a ◃ 𝐂 a i.
 nqed.
 
 nlemma hint_auto1 : ∀A,U,V. (∀x.x ∈ U → x ◃ V) → cover_set cover A U V.
-nnormalize; nauto.
+nnormalize; /2/.
 nqed.
 
 alias symbol "covers" (instance 1) = "covers".
 alias symbol "covers" (instance 2) = "covers set".
 alias symbol "covers" (instance 3) = "covers".
 ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
-#A; #a; #U; #V; #aU; #UV; nelim aU; nauto depth=4;
+#A; #a; #U; #V; #aU; #UV; nelim aU; /3/;
 nqed.
 
 ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
@@ -29,7 +29,7 @@ ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
 ##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); nauto;
+##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); /2/;
 ##] 
 nqed.
 
@@ -50,7 +50,7 @@ nrecord uAx : Type[1] ≝ {
 
 ndefinition uax : uAx → Ax.
 #A; @ (uax_ A) (λx.unit); #a; #_; 
-napply (𝐂 a ?);  nlapply one; ncases (with_ A a); nauto; 
+napply (𝐂 a ?);  nlapply one; ncases (with_ A a); //; 
 nqed.
 
 ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
@@ -73,14 +73,14 @@ ntheorem col2_4 :
   ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a one. 
 #A; #a; #H; nelim H;
 ##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); nauto;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); //;
 ##] 
 nqed.
 
 ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
 
 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
-#A; #a; #U; #V; #HUV; #H; nelim H; nauto depth=4; 
+#A; #a; #U; #V; #HUV; #H; nelim H; //; 
 nqed.
 
 ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
@@ -88,10 +88,10 @@ ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
 ncut (a ◃ Z); ##[
   nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a);
   napply (cover_monotone … AxCon); nassumption; ##] #H; 
-ncut (a ◃ ∅); ##[ napply (transitivity … H); nwhd in match Z; nauto; ##] #H1;
+ncut (a ◃ ∅); ##[ napply (transitivity … H); nwhd in match Z; //; ##] #H1;
 ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2;
 ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3;
-nauto;
+//;
 nqed.
 
 include "nat/nat.ma".
@@ -127,20 +127,20 @@ naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 
 nlemma replace_char:
   ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V.
-#A; #U; #V;  #UV; #VU; #a; #aU; nelim aU; nauto;
+#A; #U; #V;  #UV; #VU; #a; #aU; nelim aU; //;
 nqed.
 
 ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
 *; #a; #H;
 ncut (a ◃ { x | x ◃ ∅}); ##[
-  napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); nauto; ##]
-  napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); nauto; ##]
+  napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); //; ##]
+  napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); //; ##]
   napply (axiom_cond … a one); ##] #H1;
-ncut (a ◃ ∅); ##[ napply (transitivity … H1); nauto; ##] #H2;
+ncut (a ◃ ∅); ##[ napply (transitivity … H1); //; ##] #H2;
 nlapply (col2_4 …H2); #H3;
 ncut (a ∈ 𝐂 a one); ##[
-  nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4;
-nauto;
+  nnormalize; ncases (Ph a); nrewrite > (H a); //; ##] #H4;
+//;
 nqed.
 
 
diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4ca6460d2..dc78b7680 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -23,7 +23,7 @@ ndefinition natS ≝ S.
 include "topology/igft.ma".
 
 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
-nnormalize; nauto;
+nnormalize; /2/;
 nqed.
 
 alias symbol "covers" = "covers set".
@@ -33,9 +33,7 @@ nlemma cover_ind':
  ∀A:Ax.∀U,P:Ω^A.
    (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
     ◃ U ⊆ P.
- #A; #U; #P; #refl; #infty; #a; #H; nelim H
-  [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2; 
-            napply infty; nauto; ##] 
+ #A; #U; #P; #refl; #infty; #a; #H; nelim H; /3/. 
 nqed.
 
 alias symbol "covers" (instance 1) = "covers".
@@ -78,7 +76,7 @@ ncoercion uuax : ∀u:uuAx. Ax ≝ uuax on _u : uuAx to Ax.
 
 nlemma eq_rect_Type0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; nauto;
+ #A; #a; #x; #p; ncases p; //;
 nqed.
 
 nlemma eq_rect_Type0_r:
@@ -108,24 +106,24 @@ nlet rec cover_rect
 ≝ ?.
  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
  ncases (decide_mem … memdec b)
-  [ #_; #H; napply refl; nauto
-  | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
-    [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
-      [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
+  [ #_; #H; napply refl; /2/
+  | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
+    [ #E; napply False_rect_Type0; ncut (b=b) [//] ncases p in ⊢ (???% → ?)
+      [ #a; #K; #E2; napply H [ // | nrewrite > E2; // ]
     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
-        nauto]
+        //]
   ##| #a; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
-            nrewrite > E2; nnormalize; #_; nauto]##]
+            nrewrite > E2; nnormalize; #_; //]##]
       #Hcut; 
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y; #E2; nrewrite > E2 
-      (* [##2: napply cover_rect] nauto depth=1; *)
+      (* [##2: napply cover_rect] //; *)
        [ napply Hcut
-     ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
+     ##| napply (cover_rect A U memdec P refl infty a); // ]##]
 nqed.
 
 (********* Esempio:
@@ -171,6 +169,5 @@ ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=
       napply (S m * H (pred m) …); //]
 nqed.
 
-nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]
- nnormalize; //.
+nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)] //.
 nqed.
\ 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 e242cb882..6d84ba3d8 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -23,9 +23,7 @@ ndefinition natS ≝ S.
 
 include "topology/igft.ma".
 
-nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
-nnormalize; nauto;
-nqed.
+nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V./2/.nqed.
 
 ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
  mk_Sigma: ∀a:A. P a → Sigma A P.
@@ -65,8 +63,7 @@ nlemma ncover_ind':
    (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
     ◃ U ⊆ P.
  #A; #U; #P; #refl; #infty; #a; #H; nelim H
-  [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2; 
-            napply infty; nauto; ##] 
+  [ // | #b; #j; #K1; #K2; napply infty; //; ##] 
 nqed.
 
 alias symbol "covers" (instance 3) = "ncovers".
@@ -116,7 +113,7 @@ ncoercion uuax : ∀u:uuAx. nAx ≝ uuax on _u : uuAx to nAx.
 
 nlemma eq_rect_Type0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; nauto;
+ #A; #a; #x; #p; ncases p; //;
 nqed.
 
 nlemma eq_rect_Type0_r:
@@ -150,15 +147,15 @@ nlet rec cover_rect
 ≝ ?.
  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
  ncases (decide_mem … memdec b)
-  [ #_; #H; napply refl; nauto
-  | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
-    [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
-      [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
+  [ #_; #H; napply refl; /2/
+  | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
+    [ #E; napply False_rect_Type0; ncut (b=b) [//] ncases p in ⊢ (???% → ?)
+      [ #a; #K; #E2; napply H [ // | nrewrite > E2; // ]
     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
-        nauto]
+        //]
   ##| #a; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; /2/ ]##]
@@ -166,16 +163,16 @@ nlet rec cover_rect
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y
        [ napply Hcut
-     ##| napply (cover_rect A U memdec P refl infty a); nauto ]
+     ##| napply (cover_rect A U memdec P refl infty a); // ]
   ##| #a; #a1; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
       #Hcut;
       ncut (a1 ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
@@ -183,8 +180,8 @@ nlet rec cover_rect
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y; ncases y; nnormalize
        [##1,2: nassumption
-       | napply (cover_rect A U memdec P refl infty a); nauto
-       | napply (cover_rect A U memdec P refl infty a1); nauto]
+       | napply (cover_rect A U memdec P refl infty a); //
+       | napply (cover_rect A U memdec P refl infty a1); //]
 nqed.
 
 (********* Esempio:
@@ -239,6 +236,5 @@ ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=
          napply (S m * H true * H false) ]
 nqed.
 
-nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]
- nnormalize; //.
+nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]//.
 nqed.
\ No newline at end of file