1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / ast_type_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma
index b6042164cf354027cfb0f281b22b2877de6611dd..9e962a1c68f6b43de517e3c0c5d70d74bb32726d 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma
@@ -61,19 +61,19 @@ ndefinition astbasetype_destruct : astbasetype_destruct_aux.
 nqed.
 
 nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_ast_base_type.
- #b1; #b2; ncases b1; ncases b2; nnormalize; napply (refl_eq ??). nqed.
+ #b1; #b2; ncases b1; ncases b2; nnormalize; napply refl_eq. nqed.
 
 nlemma eqastbasetype_to_eq : ∀b1,b2.eq_ast_base_type b1 b2 = true → b1 = b2.
  #b1; #b2; ncases b1; ncases b2; nnormalize;
- ##[ ##1,5,9: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,5,9: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqastbasetype : ∀b1,b2.b1 = b2 → eq_ast_base_type b1 b2 = true.
  #b1; #b2; ncases b1; ncases b2; nnormalize;
- ##[ ##1,5,9: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (astbasetype_destruct ??? H)
+ ##[ ##1,5,9: #H; napply refl_eq
+ ##| ##*: #H; napply (astbasetype_destruct … H)
  ##]
 nqed.
 
@@ -82,7 +82,7 @@ nlemma asttype_destruct_base_base : ∀b1,b2.AST_TYPE_BASE b1 = AST_TYPE_BASE b2
  nchange with (match AST_TYPE_BASE b2 with [ AST_TYPE_BASE a ⇒ b1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma asttype_destruct_array_array_1 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → x1 = x2.
@@ -90,7 +90,7 @@ nlemma asttype_destruct_array_array_1 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AS
  nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY a _ ⇒ x1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → y1 = y2.
@@ -98,7 +98,7 @@ nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AS
  nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY _ b ⇒ y1 = b | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_STRUCT b2 → b1 = b2.
@@ -106,7 +106,7 @@ nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_S
  nchange with (match AST_TYPE_STRUCT b2 with [ AST_TYPE_STRUCT a ⇒ b1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition asttype_destruct_aux ≝
@@ -128,7 +128,7 @@ ndefinition asttype_destruct : asttype_destruct_aux.
  ##[ ##1: ncases b2;
           ##[ ##1: nnormalize; #s1; #s2; ncases s1; ncases s2; nnormalize;
                    ##[ ##1,5,9: #H; napply (λx:P.x)
-                   ##| ##*: #H; napply (astbasetype_destruct ??? (asttype_destruct_base_base ?? H))
+                   ##| ##*: #H; napply (astbasetype_destruct … (asttype_destruct_base_base … H))
                    ##]
           ##| ##2: #t; #n; #b; nnormalize; #H
           ##| ##3: #l; #b; nnormalize; #H
@@ -164,84 +164,84 @@ nlemma symmetric_eqasttype_aux1
 nqed.
 
 nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type.
- #t1; napply (ast_type_index ????? t1);
+ #t1; napply (ast_type_index … t1);
  ##[ ##1: #b1; #t2; ncases t2;
           ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1));
                    nrewrite > (symmetric_eqastbasetype b1 b2);
-                   napply (refl_eq ??)
-          ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
-          ##| ##3: #nl2; nnormalize; napply (refl_eq ??)
+                   napply refl_eq
+          ##| ##2: #st2; #n2; nnormalize; napply refl_eq
+          ##| ##3: #nl2; nnormalize; napply refl_eq
           ##]
  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
           ##[ ##2: #st2; #n2; nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = ((eq_ast_type st2 st1)⊗(eq_nat n2 n1)));
                    nrewrite > (symmetric_eqnat n1 n2);
                    nrewrite > (H st2);
-                   napply (refl_eq ??)
-          ##| ##1: #b2; nnormalize; napply (refl_eq ??)
-          ##| ##3: #nl2; nnormalize; napply (refl_eq ??)
+                   napply refl_eq
+          ##| ##1: #b2; nnormalize; napply refl_eq
+          ##| ##3: #nl2; nnormalize; napply refl_eq
           ##]
  ##| ##3: #hh1; #H; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
                    ##[ ##1: #hh2; nchange with ((eq_ast_type hh1 hh2) = (eq_ast_type hh2 hh1));
                             nrewrite > (H hh2);
-                            napply (refl_eq ??)
-                   ##| ##2: #hh2; #ll2; nnormalize; napply (refl_eq ??)
+                            napply refl_eq
+                   ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
                    ##]
-          ##| ##1: #b2; nnormalize; napply (refl_eq ??)
-          ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
+          ##| ##1: #b2; nnormalize; napply refl_eq
+          ##| ##2: #st2; #n2; nnormalize; napply refl_eq
           ##]
  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
-                   ##[ ##1: #hh2; nnormalize; napply (refl_eq ??)
+                   ##[ ##1: #hh2; nnormalize; napply refl_eq
                    ##| ##2: #hh2; #ll2; nnormalize;
                             nrewrite > (H hh2);
                             nrewrite > (symmetric_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2)));
-                            napply (refl_eq ??)
+                            napply refl_eq
                    ##]
-          ##| ##1: #b2; nnormalize; napply (refl_eq ??)
-          ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
+          ##| ##1: #b2; nnormalize; napply refl_eq
+          ##| ##2: #st2; #n2; nnormalize; napply refl_eq
           ##]
  ##]
 nqed.
 
 nlemma eqasttype_to_eq : ∀t1,t2.eq_ast_type t1 t2 = true → t1 = t2.
  #t1;
- napply (ast_type_index ????? t1);
+ napply (ast_type_index … t1);
  ##[ ##1: #b1; #t2; ncases t2;
           ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_ast_base_type b1 b2) = true);
                    nrewrite > (eqastbasetype_to_eq b1 b2 H);
-                   napply (refl_eq ??)
-          ##| ##2: #st2; #n2; nnormalize; #H; napply (bool_destruct ??? H)
-          ##| ##3: #nl2; nnormalize; #H; napply (bool_destruct ??? H)
+                   napply refl_eq
+          ##| ##2: #st2; #n2; nnormalize; #H; napply (bool_destruct … H)
+          ##| ##3: #nl2; nnormalize; #H; napply (bool_destruct … H)
           ##]
  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
           ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = true);
-                   nrewrite > (H st2 (andb_true_true_l ?? H1));
-                   nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r ?? H1));
-                   napply (refl_eq ??)
-          ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct ??? H1)
-          ##| ##3: #nl2; nnormalize; #H1; napply (bool_destruct ??? H1)
+                   nrewrite > (H st2 (andb_true_true_l … H1));
+                   nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H1));
+                   napply refl_eq
+          ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##3: #nl2; nnormalize; #H1; napply (bool_destruct … H1)
           ##]
  ##| ##3: #hh1; #H; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
                    ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_ast_type hh1 hh2) = true);
                             nrewrite > (H hh2 H1);
-                            napply (refl_eq ??)
-                   ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct ??? H1)
+                            napply refl_eq
+                   ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct … H1)
                    ##]
-          ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct ??? H1)
-          ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct ??? H1)
+          ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct … H1)
           ##]
  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
-                   ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct ??? H2)
+                   ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct … H2)
                    ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_ast_type hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_ast_type x y) ll1 ll2)) = true);
-                            nrewrite > (H hh2 (andb_true_true_l ?? H2));
-                            nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r ?? H2)));
-                            napply (refl_eq ??)
+                            nrewrite > (H hh2 (andb_true_true_l … H2));
+                            nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2)));
+                            napply refl_eq
                    ##]
-          ##| ##1: #b2; nnormalize; #H2; napply (bool_destruct ??? H2)
-          ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct ??? H2)
+          ##| ##1: #b2; nnormalize; #H2; napply (bool_destruct … H2)
+          ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct … H2)
           ##]
  ##]
 nqed.
@@ -256,47 +256,47 @@ nqed.
 
 nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
  #t1;
- napply (ast_type_index ????? t1);
+ napply (ast_type_index … t1);
  ##[ ##1: #b1; #t2; ncases t2;
-          ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base ?? H);
+          ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base … H);
                    nchange with ((eq_ast_base_type b2 b2) = true);
-                   nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq ??));
-                   napply (refl_eq ??)
-          ##| ##2: #st2; #n2; #H; napply (asttype_destruct ??? H)
-          ##| ##3: #nl2; #H; napply (asttype_destruct ??? H)
+                   nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …));
+                   napply refl_eq
+          ##| ##2: #st2; #n2; #H; napply (asttype_destruct … H)
+          ##| ##3: #nl2; #H; napply (asttype_destruct … H)
           ##]
  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
           ##[ ##2: #st2; #n2; #H1;  nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = true);
-                   nrewrite > (H st2 (asttype_destruct_array_array_1 ???? H1));
-                   nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 ???? H1));
+                   nrewrite > (H st2 (asttype_destruct_array_array_1 … H1));
+                   nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1));
                    nnormalize;
-                   napply (refl_eq ??)
-          ##| ##1: #b2; #H1; napply (asttype_destruct ??? H1)
-          ##| ##3: #nl2; #H1; napply (asttype_destruct ??? H1)
+                   napply refl_eq
+          ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
+          ##| ##3: #nl2; #H1; napply (asttype_destruct … H1)
           ##]
  ##| ##3: #hh1; #H; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
                    ##[ ##1: #hh2; #H1; nchange with ((eq_ast_type hh1 hh2) = true);
-                            nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct ?? H1)));
-                            napply (refl_eq ??)
-                   ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct ?? H1))
+                            nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
+                            napply refl_eq
+                   ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
                    ##]
-          ##| ##1: #b2; #H1; napply (asttype_destruct ??? H1)
-          ##| ##2: #st2; #n2; #H1; napply (asttype_destruct ??? H1)
+          ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
+          ##| ##2: #st2; #n2; #H1; napply (asttype_destruct … H1)
           ##]
  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
           ##[ ##3: #nl2; ncases nl2;
-                   ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct ?? H2))
+                   ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2))
                    ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_ast_type hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_ast_type x y) ll1 ll2)) = true);
-                            nrewrite > (H hh2 (nelist_destruct_cons_cons_1 ????? (asttype_destruct_struct_struct ?? H2)));
+                            nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2)));
                             nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?));
-                            ##[ ##1: nnormalize; napply (refl_eq ??)
-                            ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 ????? (asttype_destruct_struct_struct ?? H2));
-                                     napply (refl_eq ??)
+                            ##[ ##1: nnormalize; napply refl_eq
+                            ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 … (asttype_destruct_struct_struct … H2));
+                                     napply refl_eq
                             ##]
                    ##]
-          ##| ##1: #b2; #H2; napply (asttype_destruct ??? H2)
-          ##| ##2: #st2; #n2; #H2; napply (asttype_destruct ??? H2)
+          ##| ##1: #b2; #H2; napply (asttype_destruct … H2)
+          ##| ##2: #st2; #n2; #H2; napply (asttype_destruct … H2)
           ##]
  ##]
 nqed.
@@ -306,8 +306,8 @@ nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true →
  ncases ast;
  nnormalize;
  ##[ ##1: #t; #H; napply I
- ##| ##2: #t; #n; #H; napply (bool_destruct ??? H)
- ##| ##3: #t; #H; napply (bool_destruct ??? H)
+ ##| ##2: #t; #n; #H; napply (bool_destruct … H)
+ ##| ##3: #t; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -315,7 +315,7 @@ nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = tr
  #ast;
  ncases ast;
  nnormalize;
- ##[ ##1: #t; #H; napply (bool_destruct ??? H)
+ ##[ ##1: #t; #H; napply (bool_destruct … H)
  ##| ##2: #t; #n; #H; napply I
  ##| ##3: #l; #H; napply I
  ##]