1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / prod_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
index 02bd4e1384cafeec5c116a5301ef0c93b4e12886..7c9043921ba5c179f8cae8f23638b538e79df763 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
@@ -34,7 +34,7 @@ nlemma pair_destruct_1 :
  nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma pair_destruct_2 :
@@ -44,7 +44,7 @@ nlemma pair_destruct_2 :
  nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqpair :
@@ -54,16 +54,16 @@ nlemma symmetric_eqpair :
  (symmetricT T2 bool f2) →
  (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
  #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2;
  nnormalize;
  nrewrite > (H x1 x2);
  ncases (f1 x2 x1);
  nnormalize;
- ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
- ##| ##2: napply (refl_eq ??)
+ ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
+ ##| ##2: napply refl_eq
  ##]
 nqed.
 
@@ -74,15 +74,15 @@ nlemma eq_to_eqpair :
  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
  (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2; #H;
  nnormalize;
- nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
+ nrewrite > (H1 … (pair_destruct_1 … H));
  nnormalize;
- nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
- napply (refl_eq ??).
+ nrewrite > (H2 … (pair_destruct_2 … H));
+ napply refl_eq.
 nqed.
 
 nlemma eqpair_to_eq :
@@ -92,20 +92,20 @@ nlemma eqpair_to_eq :
  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
  (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
  #H3;
- ##[ ##2: napply (bool_destruct ??? H3) ##]
+ ##[ ##2: napply (bool_destruct … H3) ##]
  #H4;
- nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H4 (refl_eq …));
  nrewrite > (H2 y1 y2 H3);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma triple_destruct_1 :
@@ -115,7 +115,7 @@ nlemma triple_destruct_1 :
  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma triple_destruct_2 :
@@ -125,7 +125,7 @@ nlemma triple_destruct_2 :
  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma triple_destruct_3 :
@@ -135,7 +135,7 @@ nlemma triple_destruct_3 :
  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqtriple :
@@ -146,9 +146,9 @@ nlemma symmetric_eqtriple :
  (symmetricT T3 bool f3) →
  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -157,10 +157,10 @@ nlemma symmetric_eqtriple :
  ##[ ##1: nrewrite > (H1 y1 y2);
           ncases (f2 y2 y1);
           nnormalize;
-          ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
-          ##| ##2: napply (refl_eq ??)
+          ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
+          ##| ##2: napply refl_eq
           ##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
  ##]
 nqed.
 
@@ -172,17 +172,17 @@ nlemma eq_to_eqtriple :
  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
  (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #H;
  nnormalize;
- nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
+ nrewrite > (H1 … (triple_destruct_1 … H));
  nnormalize;
- nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
+ nrewrite > (H2 … (triple_destruct_2 … H));
  nnormalize;
- nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
- napply (refl_eq ??).
+ nrewrite > (H3 … (triple_destruct_3 … H));
+ napply refl_eq.
 nqed.
 
 nlemma eqtriple_to_eq :
@@ -193,24 +193,24 @@ nlemma eqtriple_to_eq :
  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H4; napply (bool_destruct ??? H4) ##]
+ ##[ ##2: #H4; napply (bool_destruct … H4) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H4; #H5; napply (bool_destruct ??? H5) ##]
+ ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
  #H4; #H5; #H6;
- nrewrite > (H4 (refl_eq ??));
- nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H4 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
  nrewrite > (H3 z1 z2 H5);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quadruple_destruct_1 :
@@ -220,7 +220,7 @@ nlemma quadruple_destruct_1 :
  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quadruple_destruct_2 :
@@ -230,7 +230,7 @@ nlemma quadruple_destruct_2 :
  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quadruple_destruct_3 :
@@ -240,7 +240,7 @@ nlemma quadruple_destruct_3 :
  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quadruple_destruct_4 :
@@ -250,7 +250,7 @@ nlemma quadruple_destruct_4 :
  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqquadruple :
@@ -262,9 +262,9 @@ nlemma symmetric_eqquadruple :
  (symmetricT T4 bool f4) →
  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -276,12 +276,12 @@ nlemma symmetric_eqquadruple :
           ##[ ##1: nrewrite > (H2 z1 z2);
                    ncases (f3 z2 z1);
                    nnormalize;
-                   ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
-                   ##| ##2: napply (refl_eq ??)
+                   ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
+                   ##| ##2: napply refl_eq
                    ##]
-          ##| ##2: napply (refl_eq ??)
+          ##| ##2: napply refl_eq
           ##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
  ##]
 nqed.
 
@@ -294,19 +294,19 @@ nlemma eq_to_eqquadruple :
  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
  (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #H;
  nnormalize;
- nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
+ nrewrite > (H1 … (quadruple_destruct_1 … H));
  nnormalize;
- nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
+ nrewrite > (H2 … (quadruple_destruct_2 … H));
  nnormalize;
- nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
+ nrewrite > (H3 … (quadruple_destruct_3 … H));
  nnormalize;
- nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
- napply (refl_eq ??).
+ nrewrite > (H4 … (quadruple_destruct_4 … H));
+ napply refl_eq.
 nqed.
 
 nlemma eqquadruple_to_eq :
@@ -318,29 +318,29 @@ nlemma eqquadruple_to_eq :
  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H5; napply (bool_destruct ??? H5) ##]
+ ##[ ##2: #H5; napply (bool_destruct … H5) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; napply (bool_destruct ??? H6) ##]
+ ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; #H7; napply (bool_destruct ??? H7) ##]
+ ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
  #H5; #H6; #H7; #H8;
- nrewrite > (H5 (refl_eq ??));
- nrewrite > (H6 (refl_eq ??));
- nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H5 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
  nrewrite > (H4 v1 v2 H7);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quintuple_destruct_1 :
@@ -350,7 +350,7 @@ nlemma quintuple_destruct_1 :
  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quintuple_destruct_2 :
@@ -360,7 +360,7 @@ nlemma quintuple_destruct_2 :
  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quintuple_destruct_3 :
@@ -370,7 +370,7 @@ nlemma quintuple_destruct_3 :
  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quintuple_destruct_4 :
@@ -380,7 +380,7 @@ nlemma quintuple_destruct_4 :
  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma quintuple_destruct_5 :
@@ -390,7 +390,7 @@ nlemma quintuple_destruct_5 :
  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqquintuple :
@@ -403,9 +403,9 @@ nlemma symmetric_eqquintuple :
  (symmetricT T5 bool f5) →
  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -420,14 +420,14 @@ nlemma symmetric_eqquintuple :
                    ##[ ##1: nrewrite > (H3 v1 v2);
                             ncases (f4 v2 v1);
                             nnormalize;
-                            ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
-                            ##| ##2: napply (refl_eq ??)
+                            ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
+                            ##| ##2: napply refl_eq
                             ##]
-                   ##| ##2: napply (refl_eq ??)
+                   ##| ##2: napply refl_eq
                    ##]
-          ##| ##2: napply (refl_eq ??)
+          ##| ##2: napply refl_eq
           ##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
  ##]
 nqed.
 
@@ -441,21 +441,21 @@ nlemma eq_to_eqquintuple :
  (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
  (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize;
- nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
+ nrewrite > (H1 … (quintuple_destruct_1 … H));
  nnormalize;
- nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
+ nrewrite > (H2 … (quintuple_destruct_2 … H));
  nnormalize;
- nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
+ nrewrite > (H3 … (quintuple_destruct_3 … H));
  nnormalize;
- nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
+ nrewrite > (H4 … (quintuple_destruct_4 … H));
  nnormalize;
- nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
- napply (refl_eq ??).
+ nrewrite > (H5 … (quintuple_destruct_5 … H));
+ napply refl_eq.
 nqed.
 
 nlemma eqquintuple_to_eq :
@@ -468,32 +468,32 @@ nlemma eqquintuple_to_eq :
  (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H6; napply (bool_destruct ??? H6) ##]
+ ##[ ##2: #H6; napply (bool_destruct … H6) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; napply (bool_destruct ??? H7) ##]
+ ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; napply (bool_destruct ??? H8) ##]
+ ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
  nletin K3 ≝ (H4 v1 v2);
  ncases (f4 v1 v2) in K3:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct ??? H9) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
  #H6; #H7; #H8; #H9; #H10;
- nrewrite > (H6 (refl_eq ??));
- nrewrite > (H7 (refl_eq ??));
- nrewrite > (H8 (refl_eq ??));
- nrewrite > (H10 (refl_eq ??));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H7 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
+ nrewrite > (H10 (refl_eq …));
  nrewrite > (H5 w1 w2 H9);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.