(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
napply refl_eq.
nqed.
+(* !!! da togliere *)
nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
#T; #x; #H;
nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
napply I.
nqed.
+(* !!! da togliere *)
nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
#T; #x; #H;
nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
nelim 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)
+ ##| ##2: #a; #H1;
+ (* !!! ndestruct: assert false *)
+ nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1;
+ (* !!! ndestruct: assert false *)
+ nelim (option_destruct_some_none ?? H1)
##| ##4: #a; #a0; #H1;
nrewrite > (H … (option_destruct_some_some … H1));
napply refl_eq
nelim op2;
nnormalize;
##[ ##1: #H1; napply refl_eq
- ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
+ ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
##| ##4: #a; #a0; #H1;
nrewrite > (H … H1);
napply refl_eq
##[ ##1: #y; ncases y;
##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
- nnormalize; #H1; napply (option_destruct_none_some T … H1)
+ nnormalize; #H1;
+ (* !!! ndestruct: assert false *)
+ napply (option_destruct_none_some T … H1)
##]
##| ##2: #xx; #y; ncases y;
##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
- nnormalize; #H2; napply (option_destruct_some_none T … H2)
+ nnormalize; #H2;
+ (* !!! ndestruct: assert false *)
+ napply (option_destruct_some_none T … H2)
##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
- nnormalize; #H2; napply (H1 (option_destruct_some_some T … H2))
+ nnormalize; #H2;
+ napply (H1 (option_destruct_some_some T … H2))
##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
nrewrite > H1; napply refl_eq
##]
(eq_option T op1 op2 f = false → op1 ≠ op2).
#T; #op1; nelim op1;
##[ ##1: #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
- ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)
+ ##[ ##1: nnormalize; #f; #H; #H1;
+ ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2;
+ (* !!! ndestruct: assert false *)
+ napply (option_destruct_none_some T … H2)
##]
##| ##2: #xx; #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; #H2; napply (option_destruct_some_none T … H2)
+ ##[ ##1: nnormalize; #f; #H; #H1; #H2;
+ (* !!! ndestruct: assert false *)
+ napply (option_destruct_some_none T … H2)
##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
napply (option_destruct_some_some T … H2)
##]