(no commit message)

[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 c157bfa11a64af79534fe638c8dbeda604ebc8ed..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
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -100,19 +100,41 @@ nlemma eqoption_to_eq :
  ##]
 nqed.
 
+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; 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)
+          ##| ##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))
+                   ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                            nrewrite > H1; napply refl_eq
+                   ##]
+          ##]
+ ##]
+nqed.
+
 nlemma neq_to_neqoption :
 ∀T.∀op1,op2:option 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; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
- ##| ##2,3: #a; #H1; napply refl_eq
- ##| ##4: #a; #a0; #H1;
-          napply H;
-          napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
+ #T; #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
+          ##]
+ ##| ##2: #xx; #op2; ncases op2;
+          ##[ ##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 …))
+          ##]
  ##]
 nqed.
 
@@ -120,15 +142,15 @@ nlemma neqoption_to_neq :
 ∀T.∀op1,op2:option 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; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply (bool_destruct … H1)
- ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2)
- ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2)
- ##| ##4: #a; #a0; #H1; #H2;
-          napply (H a0 a H1);
-          napply (option_destruct_some_some ? a0 a H2)
+ #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)
+          ##]
+ ##| ##2: #xx; #op2; ncases op2;
+          ##[ ##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)
+          ##]
  ##]
 nqed.