Release 0.5.9.

[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 4bc55e2d7434bdc45bd0892419bdec665d09b2c9..039e39b0fad9382eac9bb2ffd42c77affb41eb69 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
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,7 +27,6 @@ include "common/list_utility_lemmas.ma".
 (* dimensioni degli elementi *)
 (* ************************* *)
 
-(*
 ndefinition astbasetype_destruct_aux ≝
 Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 →
  match eq_astbasetype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
@@ -39,7 +38,6 @@ ndefinition astbasetype_destruct : astbasetype_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
-*)
 
 nlemma eq_to_eqastbasetype : ∀n1,n2.n1 = n2 → eq_astbasetype n1 n2 = true.
  #n1; #n2; #H;
@@ -60,7 +58,7 @@ nqed.
 nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
  #b1; #b2; ncases b1; ncases b2; nnormalize;
  ##[ ##1,5,9: #H; napply refl_eq
- ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -121,7 +119,6 @@ nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_S
  napply refl_eq.
 nqed.
 
-(*
 ndefinition asttype_destruct_aux ≝
 Πb1,b2:ast_type.ΠP:Prop.b1 = b2 →
  match eq_asttype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
@@ -152,7 +149,6 @@ ndefinition asttype_destruct : asttype_destruct_aux.
           ##]
  ##]
 nqed.
-*)
 
 nlemma eq_to_eqasttype_aux1
  : ∀nl1,nl2.
@@ -170,8 +166,8 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
                    nchange with ((eq_astbasetype b2 b2) = true);
                    nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …));
                    napply refl_eq
-          ##| ##2: #st2; #n2; #H; ndestruct (*napply (asttype_destruct … H)*)
-          ##| ##3: #nl2; #H; ndestruct (*napply (asttype_destruct … H)*)
+          ##| ##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_asttype st1 st2)⊗(eq_nat n1 n2)) = true);
@@ -179,26 +175,22 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
                    nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1));
                    nnormalize;
                    napply refl_eq
-          ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
-          ##| ##3: #nl2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
+          ##| ##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_asttype hh1 hh2) = true);
                             nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
                             napply refl_eq
-                   ##| ##2: #hh2; #ll2; #H1;
-                            (* !!! ndestruct non va *)
-                            nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
+                   ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
                    ##]
-          ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
-          ##| ##2: #st2; #n2; #H1; ndestruct (*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;
-                            (* !!! ndestruct non va *)
-                            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_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
                             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) ?));
@@ -207,8 +199,8 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
                                      napply refl_eq
                             ##]
                    ##]
-          ##| ##1: #b2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
-          ##| ##2: #st2; #n2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
+          ##| ##1: #b2; #H2; napply (asttype_destruct … H2)
+          ##| ##2: #st2; #n2; #H2; napply (asttype_destruct … H2)
           ##]
  ##]
 nqed.
@@ -228,37 +220,37 @@ nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2.
           ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_astbasetype b1 b2) = true);
                    nrewrite > (eqastbasetype_to_eq b1 b2 H);
                    napply refl_eq
-          ##| ##2: #st2; #n2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
-          ##| ##3: #nl2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
+          ##| ##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_asttype 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; ndestruct (*napply (bool_destruct … H1)*)
-          ##| ##3: #nl2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+          ##| ##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_asttype hh1 hh2) = true);
                             nrewrite > (H hh2 H1);
                             napply refl_eq
-                   ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+                   ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct … H1)
                    ##]
-          ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
-          ##| ##2: #st2; #n2; nnormalize; #H1; ndestruct (*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; ndestruct (*napply (bool_destruct … H2)*)
+                   ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct … H2)
                    ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype 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
                    ##]
-          ##| ##1: #b2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
-          ##| ##2: #st2; #n2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
+          ##| ##1: #b2; nnormalize; #H2; napply (bool_destruct … H2)
+          ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct … H2)
           ##]
  ##]
 nqed.
@@ -293,8 +285,8 @@ nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true →
  ncases ast;
  nnormalize;
  ##[ ##1: #t; #H; napply I
- ##| ##2: #t; #n; #H; ndestruct (*napply (bool_destruct … H)*)
- ##| ##3: #t; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##2: #t; #n; #H; napply (bool_destruct … H)
+ ##| ##3: #t; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -302,7 +294,7 @@ nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = tr
  #ast;
  ncases ast;
  nnormalize;
- ##[ ##1: #t; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##[ ##1: #t; #H; napply (bool_destruct … H)
  ##| ##2: #t; #n; #H; napply I
  ##| ##3: #l; #H; napply I
  ##]