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

   1
   2 include "utility/utility.ma".
   3
   4 (*
   5 nlemma fold_right_neList2_aux3 :
   6 \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'.
   7  #T; #h; #h'; #t; #t';
   8  napply (ne_list_ind T ??? t);
   9  napply (ne_list_ind T ??? t');
  10  ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
  11  ##| ##2: #a; #l'; #H; #x; #H1;
  12           nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
  13           nrewrite > (nat_destruct_S_S ?? H1);
  14           napply (refl_eq ??)
  15  ##| ##3: #x; #a; #l'; #H; #H1;
  16           nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
  17           nrewrite > (nat_destruct_S_S ?? H1);
  18           napply (refl_eq ??)
  19  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
  20           (* sarebbe nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l)))); *)
  21           (* ma fa passare il seguente errato ... *)
  22           nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
  23 *)
  24
  25 include "freescale/byte8_lemmas.ma".
  26
  27 (*
  28 nlemma associative_plusb8_aux
  29  : \forall e1,e2,e3,e4.
  30   match plus_ex_d_dc e2 e4 with
  31    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
  32   〈plus_ex_dc_d e1 e3 (snd ?? (plus_ex_d_dc e2 e4)),(fst ?? (plus_ex_d_dc e2 e4))〉.
  33  #e1; #e2; #e3; #e4;
  34  (* anche qui appare un T1 *)
  35  ncases (plus_ex_d_dc e2 e4);
  36  #e5; #c;
  37  napply (refl_eq ??).
  38 nqed.
  39
  40 nlemma associative_plusb8
  41  : \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)).
  42  #b1; ncases b1; #e1; #e2;
  43  #b2; ncases b2; #e3; #e4;
  44  #b3; ncases b3; #e5; #e6;
  45
  46 (* perche' volendo posso introdurre anche 2 premesse diverse con lo stesso nome? tipo #e2; #e2 *)
  47
  48  nchange with (
  49  match plus_ex_d_dc (b8l (match plus_ex_d_dc e2 e4 with
  50                            [ pair l1 c1 ⇒ 〈plus_ex_dc_d e1 e3 c1,l1〉 ])) e6 with
  51   [ pair l2 c2 ⇒ 〈plus_ex_dc_d (b8h (match plus_ex_d_dc e2 e4 with
  52                                     [ pair l3 c3 ⇒ 〈plus_ex_dc_d e1 e3 c3,l3〉 ])) e5 c2,l2〉 ] =
  53  match plus_ex_d_dc e2 (b8l (match plus_ex_d_dc e4 e6 with
  54                                     [ pair l4 c4 ⇒ 〈plus_ex_dc_d e3 e5 c4,l4〉 ])) with
  55   [ pair l5 c5 ⇒ 〈plus_ex_dc_d e1 (b8h (match plus_ex_d_dc e4 e6 with
  56                                              [ pair l6 c6 ⇒ 〈plus_ex_dc_d e3 e5 c6,l6〉 ])) c5,l5〉 ]);
  57
  58 (* gia' qua ci sono T1, T2 che appaiono dal nulla al posto delle variabili *)
  59
  60  nrewrite > (associative_plusb8_aux e1 e2 e3 e4);
  61  nrewrite > (associative_plusb8_aux e3 e4 e5 e6);
  62  nrewrite > (plusex_d_dc_to_d_c e2 e4);
  63  nrewrite > (plusex_d_dc_to_d_d e2 e4);
  64  nrewrite > (plusex_d_dc_to_d_c e4 e6);
  65
  66  (* nel visualizzatore era (snd ?? (plus_ex_d_dc e5 T2)) ma ha accettato la versione corretta *)
  67
  68  nrewrite > (plusex_d_dc_to_d_d e4 e6);
  69
  70  (*...*)
  71 *)