helm/software/matita/contribs/ng_assembly/common/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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/option.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ****** *)
  27 (* OPTION *)
  28 (* ****** *)
  29
  30 nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
  31  #T; #x1; #x2; #H;
  32  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  33  nrewrite < H;
  34  nnormalize;
  35  napply refl_eq.
  36 nqed.
  37
  38 (* !!! da togliere *)
  39 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
  40  #T; #x; #H;
  41  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  42  nrewrite > H;
  43  nnormalize;
  44  napply I.
  45 nqed.
  46
  47 (* !!! da togliere *)
  48 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  49  #T; #x; #H;
  50  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply I.
  54 nqed.
  55
  56 nlemma symmetric_eqoption :
  57 ∀T:Type.∀f:T → T → bool.
  58  (symmetricT T bool f) →
  59  (∀op1,op2:option T.
  60   (eq_option T f op1 op2 = eq_option T f op2 op1)).
  61  #T; #f; #H;
  62  #op1; #op2; nelim op1; nelim op2;
  63  nnormalize;
  64  ##[ ##1: napply refl_eq
  65  ##| ##2,3: #H; napply refl_eq
  66  ##| ##4: #a; #a0;
  67           nrewrite > (H a0 a);
  68           napply refl_eq
  69  ##]
  70 nqed.
  71
  72 nlemma eq_to_eqoption :
  73 ∀T.∀f:T → T → bool.
  74  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  75  (∀op1,op2:option T.
  76   (op1 = op2 → eq_option T f op1 op2 = true)).
  77  #T; #f; #H;
  78  #op1; #op2; nelim op1; nelim op2;
  79  nnormalize;
  80  ##[ ##1: #H1; napply refl_eq
  81  ##| ##2: #a; #H1;
  82          (* !!! ndestruct: assert false *)
  83          nelim (option_destruct_none_some ?? H1)
  84  ##| ##3: #a; #H1;
  85           (* !!! ndestruct: assert false *)
  86           nelim (option_destruct_some_none ?? H1)
  87  ##| ##4: #a; #a0; #H1;
  88           nrewrite > (H … (option_destruct_some_some … H1));
  89           napply refl_eq
  90  ##]
  91 nqed.
  92
  93 nlemma eqoption_to_eq :
  94 ∀T.∀f:T → T → bool.
  95  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  96  (∀op1,op2:option T.
  97   (eq_option T f op1 op2 = true → op1 = op2)).
  98  #T; #f; #H;
  99  #op1; #op2; nelim op1; nelim op2;
 100  nnormalize;
 101  ##[ ##1: #H1; napply refl_eq
 102  ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
 103  ##| ##4: #a; #a0; #H1;
 104           nrewrite > (H … H1);
 105           napply refl_eq
 106  ##]
 107 nqed.
 108
 109 nlemma decidable_option :
 110 ∀T.(Πx,y:T.decidable (x = y)) →
 111    (∀x,y:option T.decidable (x = y)).
 112  #T; #H; #x; nelim x;
 113  ##[ ##1: #y; ncases y;
 114           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 115           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 116                    nnormalize; #H1;
 117                    (* !!! ndestruct: assert false *)
 118                    napply (option_destruct_none_some T … H1)
 119           ##]
 120  ##| ##2: #xx; #y; ncases y;
 121           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 122                    nnormalize; #H2;
 123                    (* !!! ndestruct: assert false *)
 124                    napply (option_destruct_some_none T … H2)
 125           ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
 126                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 127                             nnormalize; #H2;
 128                             napply (H1 (option_destruct_some_some T … H2))
 129                    ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 130                             nrewrite > H1; napply refl_eq
 131                    ##]
 132           ##]
 133  ##]
 134 nqed.
 135
 136 nlemma neq_to_neqoption :
 137 ∀T.∀f:T → T → bool.
 138  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
 139  (∀op1,op2:option T.
 140   (op1 ≠ op2 → eq_option T f op1 op2 = false)).
 141  #T; #f; #H; #op1; nelim op1;
 142  ##[ ##1: #op2; ncases op2;
 143           ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
 144           ##| ##2: #yy; nnormalize; #H1; napply refl_eq
 145           ##]
 146  ##| ##2: #xx; #op2; ncases op2;
 147           ##[ ##1: nnormalize; #H1; napply refl_eq
 148           ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
 149                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
 150                    napply (H1 (refl_eq …))
 151           ##]
 152  ##]
 153 nqed.
 154
 155 nlemma neqoption_to_neq :
 156 ∀T.∀f:T → T → bool.
 157  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
 158  (∀op1,op2:option T.
 159   (eq_option T f op1 op2 = false → op1 ≠ op2)).
 160  #T; #f; #H; #op1; nelim op1;
 161  ##[ ##1: #op2; ncases op2;
 162           ##[ ##1: nnormalize; #H1;
 163                    ndestruct (*napply (bool_destruct … H1)*)
 164           ##| ##2: #yy; nnormalize; #H1; #H2;
 165                    (* !!! ndestruct: assert false *)
 166                    napply (option_destruct_none_some T … H2)
 167           ##]
 168  ##| ##2: #xx; #op2; ncases op2;
 169           ##[ ##1: nnormalize; #H1; #H2;
 170                    (* !!! ndestruct: assert false *)
 171                    napply (option_destruct_some_none T … H2)
 172           ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
 173                    napply (option_destruct_some_some T … H2)
 174           ##]
 175  ##]
 176 nqed.