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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  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 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
  39  #T; #x; #H;
  40  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  41  nrewrite > H;
  42  nnormalize;
  43  napply I.
  44 nqed.
  45
  46 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  47  #T; #x; #H;
  48  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
  49  nrewrite < H;
  50  nnormalize;
  51  napply I.
  52 nqed.
  53
  54 nlemma symmetric_eqoption :
  55 ∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
  56  (symmetricT T bool f) →
  57  (eq_option T op1 op2 f = eq_option T op2 op1 f).
  58  #T; #op1; #op2; #f; #H;
  59  nelim op1;
  60  nelim op2;
  61  nnormalize;
  62  ##[ ##1: napply refl_eq
  63  ##| ##2,3: #H; napply refl_eq
  64  ##| ##4: #a; #a0;
  65           nrewrite > (H a0 a);
  66           napply refl_eq
  67  ##]
  68 nqed.
  69
  70 nlemma eq_to_eqoption :
  71 ∀T.∀op1,op2:option T.∀f:T → T → bool.
  72  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  73  (op1 = op2 → eq_option T op1 op2 f = true).
  74  #T; #op1; #op2; #f; #H;
  75  nelim op1;
  76  nelim op2;
  77  nnormalize;
  78  ##[ ##1: #H1; napply refl_eq
  79  ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
  80  ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
  81  ##| ##4: #a; #a0; #H1;
  82           nrewrite > (H … (option_destruct_some_some … H1));
  83           napply refl_eq
  84  ##]
  85 nqed.
  86
  87 nlemma eqoption_to_eq :
  88 ∀T.∀op1,op2:option T.∀f:T → T → bool.
  89  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  90  (eq_option T op1 op2 f = true → op1 = op2).
  91  #T; #op1; #op2; #f; #H;
  92  nelim op1;
  93  nelim op2;
  94  nnormalize;
  95  ##[ ##1: #H1; napply refl_eq
  96  ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
  97  ##| ##4: #a; #a0; #H1;
  98           nrewrite > (H … H1);
  99           napply refl_eq
 100  ##]
 101 nqed.
 102
 103 nlemma neq_to_neqoption :
 104 ∀T.∀op1,op2:option T.∀f:T → T → bool.
 105  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
 106  (op1 ≠ op2 → eq_option T op1 op2 f = false).
 107  #T; #op1; #op2; #f; #H;
 108  nelim op1;
 109  nelim op2;
 110  nnormalize;
 111  ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
 112  ##| ##2,3: #a; #H1; napply refl_eq
 113  ##| ##4: #a; #a0; #H1;
 114           napply H;
 115           napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
 116  ##]
 117 nqed.
 118
 119 nlemma neqoption_to_neq :
 120 ∀T.∀op1,op2:option T.∀f:T → T → bool.
 121  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
 122  (eq_option T op1 op2 f = false → op1 ≠ op2).
 123  #T; #op1; #op2; #f; #H;
 124  nelim op1;
 125  nelim op2;
 126  nnormalize;
 127  ##[ ##1: #H1; napply (bool_destruct … H1)
 128  ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2)
 129  ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2)
 130  ##| ##4: #a; #a0; #H1; #H2;
 131           napply (H a0 a H1);
 132           napply (option_destruct_some_some ? a0 a H2)
 133  ##]
 134 nqed.