helm/software/matita/contribs/ng_assembly/test_errori.ma

   1
   2 (*include "utility/utility.ma".
   3
   4 nlemma fold_right_neList2_aux3 :
   5 \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'.
   6  #T; #h; #h'; #t; #t';
   7  napply (ne_list_ind T ??? t);
   8  napply (ne_list_ind T ??? t');
   9  ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
  10  ##| ##2: #a; #l'; #H; #x; #H1;
  11           nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
  12           nrewrite > (nat_destruct_S_S ?? H1);
  13           napply (refl_eq ??)
  14  ##| ##3: #x; #a; #l'; #H; #H1;
  15           nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
  16           nrewrite > (nat_destruct_S_S ?? H1);
  17           napply (refl_eq ??)
  18  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
  19           (* sarebbe nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l)))); *)
  20           (* ma fa passare il seguente errato ... *)
  21           nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
  22 *)
  23
  24 (*include "freescale/byte8_lemmas.ma".
  25
  26 nlemma associative_plusb8_aux
  27  : \forall e1,e2,e3,e4.
  28   match plus_ex_d_dc e2 e4 with
  29    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
  30   〈plus_ex_dc_d e1 e3 (snd ?? (plus_ex_d_dc e2 e4)),(fst ?? (plus_ex_d_dc e2 e4))〉.
  31  #e1; #e2; #e3; #e4;
  32  (* anche qui appare un T1 *)
  33  ncases (plus_ex_d_dc e2 e4);
  34  #e5; #c;
  35  napply (refl_eq ??).
  36 nqed.
  37
  38 nlemma associative_plusb8
  39  : \forall b1,b2,b3.(plus_b8_d_d (plus_b8_d_d b1 b2) b3) = (plus_b8_d_d b1 (plus_b8_d_d b2 b3)).
  40  #b1; ncases b1; #e1; #e2;
  41  #b2; ncases b2; #e3; #e4;
  42  #b3; ncases b3; #e5; #e6;
  43
  44 (* perche' volendo posso introdurre anche 2 premesse diverse con lo stesso nome? tipo #e2; #e2 *)
  45
  46  nchange with (
  47  match plus_ex_d_dc (b8l (match plus_ex_d_dc e2 e4 with
  48                            [ pair l1 c1 ⇒ 〈plus_ex_dc_d e1 e3 c1,l1〉 ])) e6 with
  49   [ pair l2 c2 ⇒ 〈plus_ex_dc_d (b8h (match plus_ex_d_dc e2 e4 with
  50                                     [ pair l3 c3 ⇒ 〈plus_ex_dc_d e1 e3 c3,l3〉 ])) e5 c2,l2〉 ] =
  51  match plus_ex_d_dc e2 (b8l (match plus_ex_d_dc e4 e6 with
  52                                     [ pair l4 c4 ⇒ 〈plus_ex_dc_d e3 e5 c4,l4〉 ])) with
  53   [ pair l5 c5 ⇒ 〈plus_ex_dc_d e1 (b8h (match plus_ex_d_dc e4 e6 with
  54                                              [ pair l6 c6 ⇒ 〈plus_ex_dc_d e3 e5 c6,l6〉 ])) c5,l5〉 ]);
  55
  56 (* gia' qua ci sono T1, T2 che appaiono dal nulla al posto delle variabili *)
  57
  58  nrewrite > (associative_plusb8_aux e1 e2 e3 e4);
  59  nrewrite > (associative_plusb8_aux e3 e4 e5 e6);
  60  nrewrite > (plusex_d_dc_to_d_c e2 e4);
  61  nrewrite > (plusex_d_dc_to_d_d e2 e4);
  62  nrewrite > (plusex_d_dc_to_d_c e4 e6);
  63
  64  (* nel visualizzatore era (snd ?? (plus_ex_d_dc e5 T2)) ma ha accettato la versione corretta *)
  65
  66  nrewrite > (plusex_d_dc_to_d_d e4 e6);
  67
  68  (*...*)
  69 *)
  70
  71 (*include "compiler/ast_type_lemmas.ma".
  72
  73 nlemma symmetric_eqasttype_aux1
  74  : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
  75  #x1; #x2; #y2; ncases y2; nnormalize;
  76  ##[ ##1: #t; napply (refl_eq ??)
  77  ##| ##2: #t; #l; napply (refl_eq ??)
  78  ##]
  79 nqed.
  80
  81 nlemma symmetric_eqasttype_aux2
  82  : ∀x1,y1,x2.eq_nat (len_neList ast_type (x1§§y1)) (len_neList ast_type («£x2»)) = false.
  83  #x1; #y1; #x2; ncases y1; nnormalize;
  84  ##[ ##1: #t; napply (refl_eq ??)
  85  ##| ##2: #t; #l; napply (refl_eq ??)
  86  ##]
  87 nqed.
  88
  89 ndefinition symmetric_eqasttype_aux3 ≝
  90 λnelSubType1,nelSubType2:ne_list ast_type.
  91  match eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2)
  92   return λx.eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = x → bool
  93  with
  94   [ true ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = true).
  95    fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
  96                       true nelSubType1 nelSubType2
  97                       (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
  98   | false ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = false).false
  99   ] (refl_eq ? (eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2))).
 100
 101 nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type.
 102  #t1;
 103  napply (ast_type_ind ????? t1);
 104  ##[ ##1: #b1; #t2; ncases t2;
 105           ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1));
 106                    nrewrite > (symmetric_eqastbasetype b1 b2);
 107                    napply (refl_eq ??)
 108           ##| ##2: #tt; #n; nnormalize; napply (refl_eq ??)
 109           ##| ##3: #l; nnormalize; napply (refl_eq ??)
 110           ##]
 111  ##| ##2: #tt1; #n1; #H; #t2; ncases t2;
 112           ##[ ##2: #tt2; #n2; nchange with (((eq_ast_type tt1 tt2)⊗(eq_nat n1 n2)) = ((eq_ast_type tt2 tt1)⊗(eq_nat n2 n1)));
 113                    nrewrite > (H tt2);
 114                    nrewrite > (symmetric_eqnat n1 n2);
 115                    napply (refl_eq ??)
 116           ##| ##1: #b2; nnormalize; napply (refl_eq ??)
 117           ##| ##3: #l; nnormalize; napply (refl_eq ??)
 118           ##]
 119  ##| ##3: #tt1; #H; #t2; ncases t2;
 120           ##[ ##3: #l; ncases l;
 121                    ##[ ##1: #tt2; nnormalize; nrewrite > (H tt2); napply (refl_eq ??)
 122                    ##| ##2: #tt2; #l1;
 123                             nchange with (
 124                              (match eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))
 125                                return λx.eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = x → bool
 126                               with
 127                                [ true ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = true).
 128                                 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
 129                                                    true «£tt1» (tt2§§l1)
 130                                                    (eqnat_to_eq (len_neList ? «£tt1») (len_neList ? (tt2§§l1)) p)
 131                                | false ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = false).false
 132                                ] (refl_eq ? (eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))))) = ?);
 133
 134                             (* eseguendo questa sequenza e' ok *)
 135                             nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);
 136                             nchange with (
 137                              false = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
 138                                return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
 139                               with
 140                                [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
 141                                 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
 142                                                    true (tt2§§l1) «£tt1»
 143                                                    (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
 144                                | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
 145                                ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
 146                             nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);
 147                             nnormalize;
 148
 149                             (* se commentiamo invece la prima sequenza ed eseguiamo questa *)
 150                             (* come e' possibile che rigetti la seconda rewrite? *)
 151                             nchange with (
 152                              ? = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
 153                                return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
 154                               with
 155                                [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
 156                                 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
 157                                                    true (tt2§§l1) «£tt1»
 158                                                    (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
 159                                | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
 160                                ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
 161                             nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);
 162                             nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);
 163 *)