helm/software/matita/contribs/ng_assembly/freescale/option_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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/bool_lemmas.ma".
  28 include "freescale/option.ma".
  29
  30 (* ****** *)
  31 (* OPTION *)
  32 (* ****** *)
  33
  34 nlemma option_destruct : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
  35  #T; #x1; #x2; #H;
  36  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  37  nrewrite < H;
  38  nnormalize;
  39  napply (refl_eq ??).
  40 nqed.
  41
  42 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
  43  #T; #x; #H;
  44  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  45  nrewrite > H;
  46  nnormalize;
  47  napply I.
  48 nqed.
  49
  50 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  51  #T; #x; #H;
  52  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  53  nrewrite < H;
  54  nnormalize;
  55  napply I.
  56 nqed.
  57
  58 nlemma bsymmetric_eqoption :
  59 ∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
  60  (symmetricT T bool f) →
  61  (eq_option T o1 o2 f = eq_option T o2 o1 f).
  62  #T; #o1; #o2; #f; #H;
  63  napply (option_ind T ??? o1);
  64  napply (option_ind T ??? o2);
  65  nnormalize;
  66  ##[ ##1: napply (refl_eq ??)
  67  ##| ##2,3: #H; napply (refl_eq ??)
  68  ##| ##4: #a; #a0;
  69           nrewrite > (H a0 a);
  70           napply (refl_eq ??)
  71  ##]
  72 nqed.
  73
  74 nlemma eq_to_eqoption :
  75 ∀T.∀o1,o2:option T.∀f:T → T → bool.
  76  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  77  (o1 = o2 → eq_option T o1 o2 f = true).
  78  #T; #o1; #o2; #f; #H;
  79  napply (option_ind T ??? o1);
  80  napply (option_ind T ??? o2);
  81  nnormalize;
  82  ##[ ##1: #H1; napply (refl_eq ??)
  83  ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
  84  ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
  85  ##| ##4: #a; #a0; #H1;
  86           nrewrite > (option_destruct ??? H1);
  87           nrewrite > (H a a (refl_eq ??));
  88           napply (refl_eq ??)
  89  ##]
  90 nqed.
  91
  92 nlemma eqoption_to_eq :
  93 ∀T.∀o1,o2:option T.∀f:T → T → bool.
  94  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  95  (eq_option T o1 o2 f = true → o1 = o2).
  96  #T; #o1; #o2; #f; #H;
  97  napply (option_ind T ??? o1);
  98  napply (option_ind T ??? o2);
  99  nnormalize;
 100  ##[ ##1: #H1; napply (refl_eq ??)
 101  ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
 102  ##| ##4: #a; #a0; #H1;
 103           nrewrite > (H ?? H1);
 104           napply (refl_eq ??)
 105  ##]
 106 nqed.