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 (*   Ultima modifica: 05/08/2009                                          *)
  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 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
  46  #T; #x; #y; #H;
  47  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
  48  nrewrite > H;
  49  nnormalize;
  50  napply I.
  51 nqed.
  52
  53 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
  54  #T; #x; #y; #H;
  55  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
  56  nrewrite < H;
  57  nnormalize;
  58  napply I.
  59 nqed.
  60
  61 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
  62  #T; #l;
  63  nelim l;
  64  nnormalize;
  65  ##[ ##1: napply refl_eq
  66  ##| ##2: #x; #y; #H;
  67           nrewrite > H;
  68           napply refl_eq
  69  ##]
  70 nqed.
  71
  72 nlemma associative_list : ∀T.associative (list T) (append T).
  73  #T; #x; #y; #z;
  74  nelim x;
  75  nnormalize;
  76  ##[ ##1: napply refl_eq
  77  ##| ##2: #a; #b; #H;
  78           nrewrite > H;
  79           napply refl_eq
  80  ##]
  81 nqed.
  82
  83 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
  84  #T; #l1; #l2; #a;
  85  nnormalize;
  86  napply refl_eq.
  87 nqed.
  88
  89 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
  90  #T; #a; #l; #l1;
  91  nrewrite > (associative_list T l [a] l1);
  92  nnormalize;
  93  napply refl_eq.
  94 nqed.
  95
  96 (* ************** *)
  97 (* NON-EMPTY LIST *)
  98 (* ************** *)
  99
 100 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
 101  #T; #x1; #x2; #H;
 102  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
 103  nrewrite < H;
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 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.
 109  #T; #x1; #x2; #y1; #y2; #H;
 110  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
 111  nrewrite < H;
 112  nnormalize;
 113  napply refl_eq.
 114 nqed.
 115
 116 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.
 117  #T; #x1; #x2; #y1; #y2; #H;
 118  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
 119  nrewrite < H;
 120  nnormalize;
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
 125  #T; #x1; #x2; #y1; #H;
 126  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
 127  nrewrite > H;
 128  nnormalize;
 129  napply I.
 130 nqed.
 131
 132 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
 133  #T; #x1; #x2; #y2; #H;
 134  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
 135  nrewrite < H;
 136  nnormalize;
 137  napply I.
 138 nqed.
 139
 140 nlemma associative_nelist : ∀T.associative (ne_list T) (ne_append T).
 141  #T; #x; #y; #z;
 142  nelim x;
 143  nnormalize;
 144  ##[ ##1: #hh; napply refl_eq
 145  ##| ##2: #hh; #tt; #H;
 146           nrewrite > H;
 147           napply refl_eq
 148  ##]
 149 nqed.
 150
 151 nlemma necons_append_commute : ∀T:Type.∀l1,l2:ne_list T.∀a:T.(a §§ (l1 & l2)) = ((a §§ l1) & l2).
 152  #T; #l1; #l2; #a;
 153  nnormalize;
 154  napply refl_eq.
 155 nqed.
 156
 157 nlemma append_necons_commute : ∀T:Type.∀a:T.∀l,l1:ne_list T.(l & (a §§ l1)) = (l & «£a») & l1.
 158  #T; #a; #l; #l1;
 159  nrewrite > (associative_nelist T l «£a» l1);
 160  nnormalize;
 161  napply refl_eq.
 162 nqed.