1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / utility_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
index 40aaf0b4e839de31e1872e318f71f8a012ac6012..a71b75fdc9150d0ef656b7edbd9cc6b374b5ef7c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
@@ -31,7 +31,7 @@ nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x
  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
@@ -39,7 +39,7 @@ nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons
  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
@@ -47,7 +47,7 @@ nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons
  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
@@ -70,12 +70,12 @@ nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2
  #T; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2; nnormalize;
-          ##[ ##1: #H; napply (refl_eq ??)
+          ##[ ##1: #H; napply refl_eq
           ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
           ##]
  ##| ##2: #h; #l2; ncases l2; nnormalize;
-          ##[ ##1: #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
-          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
           ##]
  ##]
 nqed.
@@ -88,7 +88,7 @@ nlemma symmetric_foldrightlist2_aux
  #T1; #T2; #f; #acc; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??)
+          ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
           ##| ##2: #h; #l; #H1; #H2; #H3;
                    nchange in H1:(%) with (O = (S (len_list ? l)));
                    nelim (nat_destruct_0_S ? H1)
@@ -103,7 +103,7 @@ nlemma symmetric_foldrightlist2_aux
                                  (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
                    nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
                    nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
-                   napply (refl_eq ??)
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -114,7 +114,7 @@ nlemma symmetric_foldrightlist2
   fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_eqlenlist T1 l1 l2 H).
  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
  nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlenlist T1 l1 l2 H) H1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_bfoldrightlist2
@@ -124,15 +124,15 @@ nlemma symmetric_bfoldrightlist2
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: #H; nnormalize; napply (refl_eq ??)
-          ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+          ##[ ##1: #H; nnormalize; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; nnormalize; napply (refl_eq ??)
+          ##[ ##1: #H1; nnormalize; napply refl_eq
           ##| ##2: #hh2; #ll2; #H1; nnormalize;
                    nrewrite > (H ll2 H1);
                    nrewrite > (H1 hh1 hh2);
-                   napply (refl_eq ??)
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -144,16 +144,16 @@ nlemma bfoldrightlist2_to_eq
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: #H; #H1; napply (refl_eq ??)
-          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+          ##[ ##1: #H; #H1; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
           ##| ##2: #hh2; #ll2; #H1; #H2;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
-                   nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
-                   nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
-                   napply (refl_eq ??)
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r … H2));
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -165,17 +165,17 @@ nlemma eq_to_bfoldrightlist2
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: #H; #H1; nnormalize; napply (refl_eq ??)
+          ##[ ##1: #H; #H1; nnormalize; napply refl_eq
           ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
           ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
-                   nrewrite > (list_destruct_1 ????? H2);
-                   nrewrite > (H1 hh2 hh2 (refl_eq ??));
+                   nrewrite > (list_destruct_1 … H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq …));
                    nnormalize;
-                   nrewrite > (H ll2 H1 (list_destruct_2 ????? H2));
-                   napply (refl_eq ??)
+                   nrewrite > (H ll2 H1 (list_destruct_2 … H2));
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -184,12 +184,12 @@ nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neL
  #T; #l1;
  nelim l1;
  ##[ ##1: #h; #l2; ncases l2; nnormalize;
-          ##[ ##1: #H; #H1; napply (refl_eq ??)
-          ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
+          ##[ ##1: #H; #H1; napply refl_eq
+          ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
           ##]
  ##| ##2: #h; #l2; ncases l2; nnormalize;
-          ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
-          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
           ##]
  ##]
 nqed.
@@ -202,24 +202,24 @@ nlemma symmetric_foldrightnelist2_aux
  #T1; #T2; #f; #acc; #l1;
  nelim l1;
  ##[ ##1: #h; #l2; ncases l2;
-          ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
+          ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
           ##| ##2: #h1; #l; ncases l;
                    ##[ ##1: #h3; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S O) = (S (S O)));
-                            nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
-                            nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
                    ##]                   
           ##]
  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
           ##[ ##1: #h4; ncases l3;
                    ##[ ##1: #h5; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S (S O)) = (S O));
-                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
-                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
                    ##]
           ##| ##2: #h4; #l4; #H1; #H2; #H3;
                    nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
@@ -228,7 +228,7 @@ nlemma symmetric_foldrightnelist2_aux
                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
                    nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
                    nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
-                   napply (refl_eq ??)
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -239,7 +239,7 @@ nlemma symmetric_foldrightnelist2
   fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_eqlennelist T1 l1 l2 H).
  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_bfoldrightnelist2
@@ -249,15 +249,15 @@ nlemma symmetric_bfoldrightnelist2
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
-          ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply (refl_eq ??)
-          ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+          ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; nnormalize; napply (refl_eq ??)
+          ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
           ##| ##2: #hh2; #ll2; #H1; nnormalize;
                    nrewrite > (H ll2 H1);
                    nrewrite > (H1 hh1 hh2);
-                   napply (refl_eq ??)
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -269,16 +269,16 @@ nlemma bfoldrightnelist2_to_eq
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
-          ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply (refl_eq ??)
-          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+          ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
           ##| ##2: #hh2; #ll2; #H1; #H2;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
-                   nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
-                   nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
-                   napply (refl_eq ??)
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r … H2));
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -291,18 +291,18 @@ nlemma eq_to_bfoldrightnelist2
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: #hh2; #H; #H1; nnormalize;
-                   nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil ??? H1));
-                   napply (refl_eq ??)
+                   nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
+                   napply refl_eq
           ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
           ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
-                   nrewrite > (nelist_destruct_cons_cons_1 ????? H2);
-                   nrewrite > (H1 hh2 hh2 (refl_eq ??));
+                   nrewrite > (nelist_destruct_cons_cons_1 … H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq …));
                    nnormalize;
-                   nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 ????? H2));
-                   napply (refl_eq ??)
+                   nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
+                   napply refl_eq
           ##]
  ##]
 nqed.
@@ -312,7 +312,7 @@ nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_emp
  ncases l;
  nnormalize;
  ##[ ##1: #H; napply I
- ##| ##2: #x; #l; #H; napply (bool_destruct ??? H)
+ ##| ##2: #x; #l; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -320,7 +320,7 @@ nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true 
  #T; #l;
  ncases l;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct ??? H)
+ ##[ ##1: #H; napply (bool_destruct … H)
  ##| ##2: #x; #l; #H; napply I
  ##]
 nqed.
@@ -333,6 +333,6 @@ nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
  #n;
  ncases n;
  ##[ ##1: nnormalize; #H; napply I
- ##| ##2: #n1; nnormalize; #H; napply (bool_destruct ??? H)
+ ##| ##2: #n1; nnormalize; #H; napply (bool_destruct … H)
  ##]
 nqed.