helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/list.ma".
  24
  25 (* *************** *)
  26 (* LISTE GENERICHE *)
  27 (* *************** *)
  28
  29 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
  30  #T; #x1; #x2; #y1; #y2; #H;
  31  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
  32  nrewrite < H;
  33  nnormalize;
  34  napply refl_eq.
  35 nqed.
  36
  37 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
  38  #T; #x1; #x2; #y1; #y2; #H;
  39  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
  40  nrewrite < H;
  41  nnormalize;
  42  napply refl_eq.
  43 nqed.
  44
  45 (* !!! da togliere *)
  46 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
  47  #T; #x; #y; #H;
  48  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
  49  nrewrite > H;
  50  nnormalize;
  51  napply I.
  52 nqed.
  53
  54 (* !!! da togliere *)
  55 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
  56  #T; #x; #y; #H;
  57  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
  58  nrewrite < H;
  59  nnormalize;
  60  napply I.
  61 nqed.
  62
  63 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
  64  #T; #l;
  65  nelim l;
  66  nnormalize;
  67  ##[ ##1: napply refl_eq
  68  ##| ##2: #x; #y; #H;
  69           nrewrite > H;
  70           napply refl_eq
  71  ##]
  72 nqed.
  73
  74 nlemma associative_list : ∀T.associative (list T) (append T).
  75  #T; #x; #y; #z;
  76  nelim x;
  77  nnormalize;
  78  ##[ ##1: napply refl_eq
  79  ##| ##2: #a; #b; #H;
  80           nrewrite > H;
  81           napply refl_eq
  82  ##]
  83 nqed.
  84
  85 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
  86  #T; #l1; #l2; #a;
  87  nnormalize;
  88  napply refl_eq.
  89 nqed.
  90
  91 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
  92  #T; #a; #l; #l1;
  93  nrewrite > (associative_list T l [a] l1);
  94  nnormalize;
  95  napply refl_eq.
  96 nqed.
  97
  98 (* ************** *)
  99 (* NON-EMPTY LIST *)
 100 (* ************** *)
 101
 102 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
 103  #T; #x1; #x2; #H;
 104  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
 105  nrewrite < H;
 106  nnormalize;
 107  napply refl_eq.
 108 nqed.
 109
 110 nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
 111  #T; #x1; #x2; #y1; #y2; #H;
 112  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
 113  nrewrite < H;
 114  nnormalize;
 115  napply refl_eq.
 116 nqed.
 117
 118 nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
 119  #T; #x1; #x2; #y1; #y2; #H;
 120  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
 121  nrewrite < H;
 122  nnormalize;
 123  napply refl_eq.
 124 nqed.
 125
 126 (* !!! da togliere *)
 127 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
 128  #T; #x1; #x2; #y1; #H;
 129  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
 130  nrewrite > H;
 131  nnormalize;
 132  napply I.
 133 nqed.
 134
 135 (* !!! da togliere *)
 136 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
 137  #T; #x1; #x2; #y2; #H;
 138  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
 139  nrewrite < H;
 140  nnormalize;
 141  napply I.
 142 nqed.
 143
 144 nlemma associative_nelist : ∀T.associative (ne_list T) (ne_append T).
 145  #T; #x; #y; #z;
 146  nelim x;
 147  nnormalize;
 148  ##[ ##1: #hh; napply refl_eq
 149  ##| ##2: #hh; #tt; #H;
 150           nrewrite > H;
 151           napply refl_eq
 152  ##]
 153 nqed.
 154
 155 nlemma necons_append_commute : ∀T:Type.∀l1,l2:ne_list T.∀a:T.(a §§ (l1 & l2)) = ((a §§ l1) & l2).
 156  #T; #l1; #l2; #a;
 157  nnormalize;
 158  napply refl_eq.
 159 nqed.
 160
 161 nlemma append_necons_commute : ∀T:Type.∀a:T.∀l,l1:ne_list T.(l & (a §§ l1)) = (l & «£a») & l1.
 162  #T; #a; #l; #l1;
 163  nrewrite > (associative_nelist T l «£a» l1);
 164  nnormalize;
 165  napply refl_eq.
 166 nqed.