helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "utility/utility.ma".
  24
  25 (* ************ *)
  26 (* List Utility *)
  27 (* ************ *)
  28
  29 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
  30  #T; #x1; #x2; #H;
  31  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
  32  nrewrite < H;
  33  nnormalize;
  34  napply (refl_eq ??).
  35 nqed.
  36
  37 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.
  38  #T; #x1; #x2; #y1; #y2; #H;
  39  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
  40  nrewrite < H;
  41  nnormalize;
  42  napply (refl_eq ??).
  43 nqed.
  44
  45 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.
  46  #T; #x1; #x2; #y1; #y2; #H;
  47  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
  48  nrewrite < H;
  49  nnormalize;
  50  napply (refl_eq ??).
  51 nqed.
  52
  53 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
  54  #T; #x1; #x2; #y1; #H;
  55  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  56  nrewrite > H;
  57  nnormalize;
  58  napply I.
  59 nqed.
  60
  61 nlemma list_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  62  #T; #x1; #x2; #y2; #H;
  63  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply I.
  67 nqed.
  68
  69 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
  70  #T; #l;
  71  ncases l;
  72  nnormalize;
  73  ##[ ##1: #H; napply I
  74  ##| ##2: #x; #l; #H; napply (bool_destruct ??? H)
  75  ##]
  76 nqed.
  77
  78 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
  79  #T; #l;
  80  ncases l;
  81  nnormalize;
  82  ##[ ##1: #H; napply (bool_destruct ??? H)
  83  ##| ##2: #x; #l; #H; napply I
  84  ##]
  85 nqed.
  86
  87 (* ******** *)
  88 (* naturali *)
  89 (* ******** *)
  90
  91 nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
  92  #n;
  93  ncases n;
  94  ##[ ##1: nnormalize; #H; napply I
  95  ##| ##2: #n1; nnormalize; #H; napply (bool_destruct ??? H)
  96  ##]
  97 nqed.