(* OPTION *)
(* ****** *)
-nlemma option_destruct : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
+nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
#T; #x1; #x2; #H;
nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
nrewrite < H;
napply I.
nqed.
-nlemma bsymmetric_eqoption :
-∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
+nlemma symmetric_eqoption :
+∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
(symmetricT T bool f) →
- (eq_option T o1 o2 f = eq_option T o2 o1 f).
- #T; #o1; #o2; #f; #H;
- napply (option_ind T ??? o1);
- napply (option_ind T ??? o2);
+ (eq_option T op1 op2 f = eq_option T op2 op1 f).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
nnormalize;
##[ ##1: napply (refl_eq ??)
##| ##2,3: #H; napply (refl_eq ??)
nqed.
nlemma eq_to_eqoption :
-∀T.∀o1,o2:option T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
(∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (o1 = o2 → eq_option T o1 o2 f = true).
- #T; #o1; #o2; #f; #H;
- napply (option_ind T ??? o1);
- napply (option_ind T ??? o2);
+ (op1 = op2 → eq_option T op1 op2 f = true).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
nnormalize;
##[ ##1: #H1; napply (refl_eq ??)
##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
##| ##4: #a; #a0; #H1;
- nrewrite > (option_destruct ??? H1);
+ nrewrite > (option_destruct_some_some ??? H1);
nrewrite > (H a a (refl_eq ??));
napply (refl_eq ??)
##]
nqed.
nlemma eqoption_to_eq :
-∀T.∀o1,o2:option T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
(∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (eq_option T o1 o2 f = true → o1 = o2).
- #T; #o1; #o2; #f; #H;
- napply (option_ind T ??? o1);
- napply (option_ind T ??? o2);
+ (eq_option T op1 op2 f = true → op1 = op2).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
nnormalize;
##[ ##1: #H1; napply (refl_eq ??)
##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)