helm/software/matita/contribs/ng_assembly2/common/option.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/comp.ma".
  24 include "common/option_base.ma".
  25 include "num/bool_lemmas.ma".
  26
  27 (* ****** *)
  28 (* OPTION *)
  29 (* ****** *)
  30
  31 nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
  32  #T; #x1; #x2; #H;
  33  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  34  nrewrite < H;
  35  nnormalize;
  36  napply refl_eq.
  37 nqed.
  38
  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 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  48  #T; #x; #H;
  49  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  50  nrewrite < H;
  51  nnormalize;
  52  napply I.
  53 nqed.
  54
  55 nlemma symmetric_eqoption :
  56 ∀T:Type.∀f:T → T → bool.
  57  (symmetricT T bool f) →
  58  (∀op1,op2:option T.
  59   (eq_option T f op1 op2 = eq_option T f op2 op1)).
  60  #T; #f; #H;
  61  #op1; #op2; nelim op1; nelim op2;
  62  nnormalize;
  63  ##[ ##1: napply refl_eq
  64  ##| ##2,3: #H; napply refl_eq
  65  ##| ##4: #a; #a0;
  66           nrewrite > (H a0 a);
  67           napply refl_eq
  68  ##]
  69 nqed.
  70
  71 nlemma eq_to_eqoption :
  72 ∀T.∀f:T → T → bool.
  73  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  74  (∀op1,op2:option T.
  75   (op1 = op2 → eq_option T f op1 op2 = true)).
  76  #T; #f; #H;
  77  #op1; #op2; nelim op1; nelim op2;
  78  nnormalize;
  79  ##[ ##1: #H1; napply refl_eq
  80  ##| ##2: #a; #H1;
  81          (* !!! ndestruct: assert false *)
  82          nelim (option_destruct_none_some ?? H1)
  83  ##| ##3: #a; #H1;
  84           (* !!! ndestruct: assert false *)
  85           nelim (option_destruct_some_none ?? H1)
  86  ##| ##4: #a; #a0; #H1;
  87           nrewrite > (H … (option_destruct_some_some … H1));
  88           napply refl_eq
  89  ##]
  90 nqed.
  91
  92 nlemma eqoption_to_eq :
  93 ∀T.∀f:T → T → bool.
  94  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  95  (∀op1,op2:option T.
  96   (eq_option T f op1 op2 = true → op1 = op2)).
  97  #T; #f; #H;
  98  #op1; #op2; nelim op1; nelim op2;
  99  nnormalize;
 100  ##[ ##1: #H1; napply refl_eq
 101  ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
 102  ##| ##4: #a; #a0; #H1;
 103           nrewrite > (H … H1);
 104           napply refl_eq
 105  ##]
 106 nqed.
 107
 108 nlemma decidable_option :
 109 ∀T.(Πx,y:T.decidable (x = y)) →
 110    (∀x,y:option T.decidable (x = y)).
 111  #T; #H; #x; nelim x;
 112  ##[ ##1: #y; ncases y;
 113           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 114           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 115                    nnormalize; #H1;
 116                    (* !!! ndestruct: assert false *)
 117                    napply (option_destruct_none_some T … H1)
 118           ##]
 119  ##| ##2: #xx; #y; ncases y;
 120           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 121                    nnormalize; #H2;
 122                    (* !!! ndestruct: assert false *)
 123                    napply (option_destruct_some_none T … H2)
 124           ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
 125                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 126                             nnormalize; #H2;
 127                             napply (H1 (option_destruct_some_some T … H2))
 128                    ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 129                             nrewrite > H1; napply refl_eq
 130                    ##]
 131           ##]
 132  ##]
 133 nqed.
 134
 135 nlemma neq_to_neqoption :
 136 ∀T.∀f:T → T → bool.
 137  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
 138  (∀op1,op2:option T.
 139   (op1 ≠ op2 → eq_option T f op1 op2 = false)).
 140  #T; #f; #H; #op1; nelim op1;
 141  ##[ ##1: #op2; ncases op2;
 142           ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
 143           ##| ##2: #yy; nnormalize; #H1; napply refl_eq
 144           ##]
 145  ##| ##2: #xx; #op2; ncases op2;
 146           ##[ ##1: nnormalize; #H1; napply refl_eq
 147           ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
 148                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
 149                    napply (H1 (refl_eq …))
 150           ##]
 151  ##]
 152 nqed.
 153
 154 nlemma neqoption_to_neq :
 155 ∀T.∀f:T → T → bool.
 156  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
 157  (∀op1,op2:option T.
 158   (eq_option T f op1 op2 = false → op1 ≠ op2)).
 159  #T; #f; #H; #op1; nelim op1;
 160  ##[ ##1: #op2; ncases op2;
 161           ##[ ##1: nnormalize; #H1;
 162                    ndestruct (*napply (bool_destruct … H1)*)
 163           ##| ##2: #yy; nnormalize; #H1; #H2;
 164                    (* !!! ndestruct: assert false *)
 165                    napply (option_destruct_none_some T … H2)
 166           ##]
 167  ##| ##2: #xx; #op2; ncases op2;
 168           ##[ ##1: nnormalize; #H1; #H2;
 169                    (* !!! ndestruct: assert false *)
 170                    napply (option_destruct_some_none T … H2)
 171           ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
 172                    napply (option_destruct_some_some T … H2)
 173           ##]
 174  ##]
 175 nqed.
 176
 177 nlemma option_is_comparable :
 178  comparable → comparable.
 179  #T; napply (mk_comparable (option T));
 180  ##[ napply (None ?)
 181  ##| napply (λx.false)
 182  ##| napply (eq_option … (eqc T))
 183  ##| napply (eqoption_to_eq … (eqc T));
 184      napply (eqc_to_eq T)
 185  ##| napply (eq_to_eqoption … (eqc T));
 186      napply (eq_to_eqc T)
 187  ##| napply (neqoption_to_neq … (eqc T));
 188      napply (neqc_to_neq T)
 189  ##| napply (neq_to_neqoption … (eqc T));
 190      napply (neq_to_neqc T)
 191  ##| napply decidable_option;
 192      napply (decidable_c T)
 193  ##| napply symmetric_eqoption;
 194      napply (symmetric_eqc T)
 195  ##]
 196 nqed.
 197
 198 unification hint 0 ≔ S: comparable;
 199          T ≟ (carr S),
 200          X ≟ (option_is_comparable S)
 201  (*********************************************) ⊢
 202          carr X ≡ option T.