X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ftest_errori.ma;h=4236c5c6341f7c0b93e878951e88b04880244284;hb=d97886196d2c730f72312b226bebc388be08f39e;hp=430df6e17f8b9d6cbd94239a272c0458ab57096c;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 430df6e17..4236c5c63 100644
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,7 +1,6 @@
 
-include "utility/utility.ma".
+(*include "utility/utility.ma".
 
-(*
 nlemma fold_right_neList2_aux3 :
 \forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
  #T; #h; #h'; #t; #t';
@@ -22,9 +21,8 @@ nlemma fold_right_neList2_aux3 :
           nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
 *)
 
-include "freescale/byte8_lemmas.ma".
+(*include "freescale/byte8_lemmas.ma".
 
-(*
 nlemma associative_plusb8_aux
  : \forall e1,e2,e3,e4.
   match plus_ex_d_dc e2 e4 with
@@ -69,3 +67,97 @@ nlemma associative_plusb8
  
  (*...*)
 *)
+
+(*include "compiler/ast_type_lemmas.ma".
+
+nlemma symmetric_eqasttype_aux1
+ : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
+ #x1; #x2; #y2; ncases y2; nnormalize;
+ ##[ ##1: #t; napply (refl_eq ??)
+ ##| ##2: #t; #l; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma symmetric_eqasttype_aux2
+ : ∀x1,y1,x2.eq_nat (len_neList ast_type (x1§§y1)) (len_neList ast_type («£x2»)) = false.
+ #x1; #y1; #x2; ncases y1; nnormalize;
+ ##[ ##1: #t; napply (refl_eq ??)
+ ##| ##2: #t; #l; napply (refl_eq ??)
+ ##]
+nqed.
+
+ndefinition symmetric_eqasttype_aux3 ≝
+λnelSubType1,nelSubType2:ne_list ast_type.
+ match eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2)
+  return λx.eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = x → bool
+ with
+  [ true ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = true).
+   fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
+                      true nelSubType1 nelSubType2
+                      (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
+  | false ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = false).false
+  ] (refl_eq ? (eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2))).
+
+nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type.
+ #t1;
+ napply (ast_type_ind ????? 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: #tt; #n; nnormalize; napply (refl_eq ??)
+          ##| ##3: #l; nnormalize; napply (refl_eq ??)
+          ##]
+ ##| ##2: #tt1; #n1; #H; #t2; ncases t2;
+          ##[ ##2: #tt2; #n2; nchange with (((eq_ast_type tt1 tt2)⊗(eq_nat n1 n2)) = ((eq_ast_type tt2 tt1)⊗(eq_nat n2 n1)));
+                   nrewrite > (H tt2);
+                   nrewrite > (symmetric_eqnat n1 n2);
+                   napply (refl_eq ??)
+          ##| ##1: #b2; nnormalize; napply (refl_eq ??)
+          ##| ##3: #l; nnormalize; napply (refl_eq ??)
+          ##]
+ ##| ##3: #tt1; #H; #t2; ncases t2;
+          ##[ ##3: #l; ncases l;
+                   ##[ ##1: #tt2; nnormalize; nrewrite > (H tt2); napply (refl_eq ??)
+                   ##| ##2: #tt2; #l1;
+                            nchange with (
+                             (match eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))
+                               return λx.eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = x → bool
+                              with
+                               [ true ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = true).
+                                fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
+                                                   true «£tt1» (tt2§§l1)
+                                                   (eqnat_to_eq (len_neList ? «£tt1») (len_neList ? (tt2§§l1)) p)
+                               | false ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = false).false
+                               ] (refl_eq ? (eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))))) = ?);
+
+                            (* eseguendo questa sequenza e' ok *)
+                            nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);
+                            nchange with (
+                             false = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
+                               return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
+                              with
+                               [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
+                                fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
+                                                   true (tt2§§l1) «£tt1»
+                                                   (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
+                               | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
+                               ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
+                            nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);
+                            nnormalize;
+
+                            (* se commentiamo invece la prima sequenza ed eseguiamo questa *)
+                            (* come e' possibile che rigetti la seconda rewrite? *)
+                            nchange with (
+                             ? = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
+                               return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
+                              with
+                               [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
+                                fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
+                                                   true (tt2§§l1) «£tt1»
+                                                   (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
+                               | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
+                               ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
+                            nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);                            
+                            nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);
+*)