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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
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 ]);
39 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
41 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
48 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
50 nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
56 nlemma symmetric_eqoption :
57 ∀T:Type.∀f:T → T → bool.∀op1,op2:option T.
58 (symmetricT T bool f) →
59 (eq_option T f op1 op2 = eq_option T f op2 op1).
60 #T; #f; #op1; #op2; #H;
64 ##[ ##1: napply refl_eq
65 ##| ##2,3: #H; napply refl_eq
72 nlemma eq_to_eqoption :
73 ∀T.∀f:T → T → bool.∀op1,op2:option T.
74 (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
75 (op1 = op2 → eq_option T f op1 op2 = true).
76 #T; #f; #op1; #op2; #H;
80 ##[ ##1: #H1; napply refl_eq
82 (* !!! ndestruct: assert false *)
83 nelim (option_destruct_none_some ?? 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));
93 nlemma eqoption_to_eq :
94 ∀T.∀f:T → T → bool.∀op1,op2:option T.
95 (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
96 (eq_option T f op1 op2 = true → op1 = op2).
97 #T; #f; #op1; #op2; #H;
101 ##[ ##1: #H1; napply refl_eq
102 ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
103 ##| ##4: #a; #a0; #H1;
109 nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y).
111 ##[ ##1: #y; ncases y;
112 ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
113 ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
115 (* !!! ndestruct: assert false *)
116 napply (option_destruct_none_some T … H1)
118 ##| ##2: #xx; #y; ncases y;
119 ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
121 (* !!! ndestruct: assert false *)
122 napply (option_destruct_some_none T … H2)
123 ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
124 ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
126 napply (H1 (option_destruct_some_some T … H2))
127 ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
128 nrewrite > H1; napply refl_eq
134 nlemma neq_to_neqoption :
135 ∀T.∀f:T → T → bool.∀op1,op2:option T.
136 (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
137 (op1 ≠ op2 → eq_option T f op1 op2 = false).
138 #T; #f; #op1; nelim op1;
139 ##[ ##1: #op2; ncases op2;
140 ##[ ##1: nnormalize; #H; #H1; nelim (H1 (refl_eq …))
141 ##| ##2: #yy; #H; nnormalize; #H1; napply refl_eq
143 ##| ##2: #xx; #op2; ncases op2;
144 ##[ ##1: #H; nnormalize; #H1; napply refl_eq
145 ##| ##2: #yy; #H; nnormalize; #H1; napply (H xx yy …);
146 nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
147 napply (H1 (refl_eq …))
152 nlemma neqoption_to_neq :
153 ∀T.∀f:T → T → bool.∀op1,op2:option T.
154 (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
155 (eq_option T f op1 op2 = false → op1 ≠ op2).
156 #T; #f; #op1; nelim op1;
157 ##[ ##1: #op2; ncases op2;
158 ##[ ##1: nnormalize; #H; #H1;
159 ndestruct (*napply (bool_destruct … H1)*)
160 ##| ##2: #yy; #H; nnormalize; #H1; #H2;
161 (* !!! ndestruct: assert false *)
162 napply (option_destruct_none_some T … H2)
164 ##| ##2: #xx; #op2; ncases op2;
165 ##[ ##1: nnormalize; #H; #H1; #H2;
166 (* !!! ndestruct: assert false *)
167 napply (option_destruct_some_none T … H2)
168 ##| ##2: #yy; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
169 napply (option_destruct_some_some T … H2)