1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool_lemmas.ma".
28 include "freescale/option.ma".
34 nlemma option_destruct : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
36 nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
42 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
44 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
50 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
52 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
58 nlemma bsymmetric_eqoption :
59 ∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
61 (eq_option T o1 o2 f = eq_option T o2 o1 f).
66 ##[ ##1: napply (refl_eq ??)
67 ##| ##2,3: #x; napply (refl_eq ??)
68 ##| ##4: #x1; #x2; nrewrite > (H x1 x2); napply (refl_eq ??)
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).
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);
85 nrewrite > (H x1 x1 (refl_eq ??));
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).
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);