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 *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "common/option.ma".
24 include "num/bool_lemmas.ma".
30 nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
32 nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
38 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
40 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
46 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
48 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
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;
62 ##[ ##1: napply refl_eq
63 ##| ##2,3: #H; napply refl_eq
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;
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));
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;
95 ##[ ##1: #H1; napply refl_eq
96 ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
97 ##| ##4: #a; #a0; #H1;
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;
111 ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
112 ##| ##2,3: #a; #H1; napply refl_eq
113 ##| ##4: #a; #a0; #H1;
115 napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
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;
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;
132 napply (option_destruct_some_some ? a0 a H2)