Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / option_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
index 1d25b4bd95bfed16bf577492e00721d60aab517f..c8942ae6c277cc5c628fab86cac4902daf072c3b 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -35,7 +35,6 @@ nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1
  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 ]);
@@ -44,7 +43,6 @@ nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → 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 ]);
@@ -54,12 +52,12 @@ nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
 nqed.
 
 nlemma symmetric_eqoption :
-∀T:Type.∀f:T → T → bool.
+∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
  (symmetricT T bool f) →
- (∀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;
+ (eq_option T op1 op2 f = eq_option T op2 op1 f).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: napply refl_eq
  ##| ##2,3: #H; napply refl_eq
@@ -70,20 +68,16 @@ nlemma symmetric_eqoption :
 nqed.
 
 nlemma eq_to_eqoption :
-∀T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (∀op1,op2:option T.
-  (op1 = op2 → eq_option T f op1 op2 = true)).
- #T; #f; #H;
- #op1; #op2; nelim op1; nelim op2;
+ (op1 = op2 → eq_option T op1 op2 f = true).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
- ##| ##2: #a; #H1;
-         (* !!! ndestruct: assert false *)
-         nelim (option_destruct_none_some ?? H1)
- ##| ##3: #a; #H1;
-          (* !!! ndestruct: assert false *)
-          nelim (option_destruct_some_none ?? H1)
+ ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
  ##| ##4: #a; #a0; #H1;
           nrewrite > (H … (option_destruct_some_some … H1));
           napply refl_eq
@@ -91,41 +85,34 @@ nlemma eq_to_eqoption :
 nqed.
 
 nlemma eqoption_to_eq :
-∀T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (∀op1,op2:option T.
-  (eq_option T f op1 op2 = true → op1 = op2)).
- #T; #f; #H;
- #op1; #op2; nelim op1; nelim op2;
+ (eq_option T op1 op2 f = true → op1 = op2).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
- ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
  ##| ##4: #a; #a0; #H1;
           nrewrite > (H … H1);
           napply refl_eq
  ##]
 nqed.
 
-nlemma decidable_option :
-∀T.(Πx,y:T.decidable (x = y)) →
-   (∀x,y:option T.decidable (x = y)).
+nlemma decidable_option : ∀T.∀H:(Π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 …))
           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1;
-                   (* !!! ndestruct: assert false *)
-                   napply (option_destruct_none_some T … H1)
+                   nnormalize; #H1; napply (option_destruct_none_some T … H1)
           ##]
  ##| ##2: #xx; #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2;
-                   (* !!! ndestruct: assert false *)
-                   napply (option_destruct_some_none T … H2)
+                   nnormalize; #H2; 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
                    ##]
@@ -134,18 +121,17 @@ nlemma decidable_option :
 nqed.
 
 nlemma neq_to_neqoption :
-∀T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (∀op1,op2:option T.
-  (op1 ≠ op2 → eq_option T f op1 op2 = false)).
- #T; #f; #H; #op1; nelim op1;
+ (op1 ≠ op2 → eq_option T op1 op2 f = false).
+ #T; #op1; nelim op1;
  ##[ ##1: #op2; ncases op2;
-          ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
-          ##| ##2: #yy; nnormalize; #H1; napply refl_eq
+          ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …))
+          ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq
           ##]
  ##| ##2: #xx; #op2; ncases op2;
-          ##[ ##1: nnormalize; #H1; napply refl_eq
-          ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
+          ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq
+          ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …);
                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
                    napply (H1 (refl_eq …))
           ##]
@@ -153,23 +139,17 @@ nlemma neq_to_neqoption :
 nqed.
 
 nlemma neqoption_to_neq :
-∀T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (∀op1,op2:option T.
-  (eq_option T f op1 op2 = false → op1 ≠ op2)).
- #T; #f; #H; #op1; nelim op1;
+ (eq_option T op1 op2 f = false → op1 ≠ op2).
+ #T; #op1; nelim op1;
  ##[ ##1: #op2; ncases op2;
-          ##[ ##1: nnormalize; #H1;
-                   ndestruct (*napply (bool_destruct … H1)*)
-          ##| ##2: #yy; nnormalize; #H1; #H2;
-                   (* !!! ndestruct: assert false *)
-                   napply (option_destruct_none_some T … H2)
+          ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
+          ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)
           ##]
  ##| ##2: #xx; #op2; ncases op2;
-          ##[ ##1: nnormalize; #H1; #H2;
-                   (* !!! ndestruct: assert false *)
-                   napply (option_destruct_some_none T … H2)
-          ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+          ##[ ##1: nnormalize; #f; #H; #H1; #H2; 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)
           ##]
  ##]