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  (boolSymmetric T f) →
  61  (eq_option T o1 o2 f = eq_option T o2 o1 f).
  62  #T; #o1; #o2; #f; #H;
  63  ncases o1;
  64  ncases o2;
  65  nnormalize;
  66  ##[ ##1: napply (refl_eq ??)
  67  ##| ##2,3: #x; napply (refl_eq ??)
  68  ##| ##4: #x1; #x2; nrewrite > (H x1 x2); napply (refl_eq ??)
  69  ##]
  70 nqed.
  71
  72 nlemma eq_to_eqoption :
  73 ∀T.∀o1,o2:option T.∀f:T → T → bool.
  74  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  75  (o1 = o2 → eq_option T o1 o2 f = true).
  76  #T; #o1; #o2; #f; #H;
  77  ncases o1;
  78  ncases o2;
  79  ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
  80  ##| ##2: #H1; #H2; nelim (option_destruct_none_some ?? H2)
  81  ##| ##3: #H1; #H2; nelim (option_destruct_some_none ?? H2)
  82  ##| ##4: #x1; #x2; #H1;
  83           nrewrite > (option_destruct ??? H1);
  84           nnormalize;
  85           nrewrite > (H x1 x1 (refl_eq ??));
  86           napply (refl_eq ??)
  87  ##]
  88 nqed.
  89
  90 nlemma eqoption_to_eq :
  91 ∀T.∀o1,o2:option T.∀f:T → T → bool.
  92  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  93  (eq_option T o1 o2 f = true → o1 = o2).
  94  #T; #o1; #o2; #f; #H;
  95  ncases o1;
  96  ncases o2;
  97  ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
  98  ##| ##2,3: #H1; #H2; nnormalize in H2:(%); nelim (bool_destruct_false_true H2)
  99  ##| ##4: #x1; #x2; #H1;
 100           nnormalize in H1:(%);
 101           nrewrite > (H ?? H1);
 102           napply (refl_eq ??)
 103  ##]
 104 nqed.