nqed.
nlemma symmetric_eqoption :
-∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
+∀T:Type.∀f:T → T → bool.
(symmetricT T bool f) →
- (eq_option T op1 op2 f = eq_option T op2 op1 f).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+ (eq_option T f op1 op2 = eq_option T f op2 op1)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
nnormalize;
##[ ##1: napply refl_eq
##| ##2,3: #H; napply refl_eq
nqed.
nlemma eq_to_eqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.
(∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (op1 = op2 → eq_option T op1 op2 f = true).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+ (op1 = op2 → eq_option T f op1 op2 = true)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
nnormalize;
##[ ##1: #H1; napply refl_eq
##| ##2: #a; #H1;
nqed.
nlemma eqoption_to_eq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.
(∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (eq_option T op1 op2 f = true → op1 = op2).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+ (eq_option T f op1 op2 = true → op1 = op2)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
nnormalize;
##[ ##1: #H1; napply refl_eq
##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
##]
nqed.
-nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y).
+nlemma decidable_option :
+∀T.(Πx,y:T.decidable (x = y)) →
+ (∀x,y:option T.decidable (x = y)).
#T; #H; #x; nelim x;
##[ ##1: #y; ncases y;
##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
nqed.
nlemma neq_to_neqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.
(∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (op1 ≠ op2 → eq_option T op1 op2 f = false).
- #T; #op1; nelim op1;
+ (∀op1,op2:option T.
+ (op1 ≠ op2 → eq_option T f op1 op2 = false)).
+ #T; #f; #H; #op1; nelim op1;
##[ ##1: #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …))
- ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq
+ ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
+ ##| ##2: #yy; nnormalize; #H1; napply refl_eq
##]
##| ##2: #xx; #op2; ncases op2;
- ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq
- ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …);
+ ##[ ##1: nnormalize; #H1; napply refl_eq
+ ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
napply (H1 (refl_eq …))
##]
nqed.
nlemma neqoption_to_neq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.
(∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (eq_option T op1 op2 f = false → op1 ≠ op2).
- #T; #op1; nelim op1;
+ (∀op1,op2:option T.
+ (eq_option T f op1 op2 = false → op1 ≠ op2)).
+ #T; #f; #H; #op1; nelim op1;
##[ ##1: #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1;
+ ##[ ##1: nnormalize; #H1;
ndestruct (*napply (bool_destruct … H1)*)
- ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2;
+ ##| ##2: #yy; nnormalize; #H1; #H2;
(* !!! ndestruct: assert false *)
napply (option_destruct_none_some T … H2)
##]
##| ##2: #xx; #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; #H2;
+ ##[ ##1: nnormalize; #H1; #H2;
(* !!! ndestruct: assert false *)
napply (option_destruct_some_none T … H2)
- ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+ ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
napply (option_destruct_some_some T … H2)
##]
##]