]> matita.cs.unibo.it Git - helm.git/commitdiff
lambda_delta: partial commit ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Sep 2012 14:30:24 +0000 (14:30 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Sep 2012 14:30:24 +0000 (14:30 +0000)
14 files changed:
matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
matita/matita/contribs/lambda_delta/ground_2/arith.ma
matita/matita/lib/basics/relations.ma
matita/matita/predefined_virtuals.ml

diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma
new file mode 100644 (file)
index 0000000..ab90ceb
--- /dev/null
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( T1 πŸ™ break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'RTop $T1 $T2 }.
+
+include "basic_2/grammar/lenv_px.ma".
+
+(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
+
+definition ttop: relation term β‰ Ξ»T1,T2. True.
+
+definition ltop: relation lenv β‰ lpx ttop.
+
+interpretation
+  "top reduction (environment)"
+  'RTop L1 L2 = (ltop L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltop_refl: reflexive β€¦ ltop.
+/2 width=1/ qed.
+
+lemma ltop_sym: symmetric β€¦ ltop.
+/2 width=1/ qed.
+
+lemma ltop_trans: transitive β€¦ ltop.
+/2 width=3/ qed.
+
+lemma ltop_append: βˆ€K1,K2. K1 πŸ™ K2 β†’ βˆ€L1,L2. L1 πŸ™ L2 β†’ L1 @@ K1 πŸ™ L2 @@ K2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltop_inv_atom1: βˆ€L2. β‹† πŸ™ L2 β†’ L2 = β‹†.
+/2 width=2 by lpx_inv_atom1/ qed-.
+
+lemma ltop_inv_pair1: βˆ€K1,I,V1,L2. K1. β“‘{I} V1 πŸ™ L2 β†’
+                      βˆƒβˆƒK2,V2. K1 πŸ™ K2 & L2 = K2. β“‘{I} V2.
+#K1 #I #V1 #L2 #H
+elim (lpx_inv_pair1 β€¦ H) -H /2 width=4/
+qed-.
+
+lemma ltop_inv_atom2: βˆ€L1. L1 πŸ™ β‹† β†’ L1 = β‹†.
+/2 width=2 by lpx_inv_atom2/ qed-.
+
+lemma ltop_inv_pair2: βˆ€L1,K2,I,V2. L1 πŸ™ K2. β“‘{I} V2 β†’
+                      βˆƒβˆƒK1,V1. K1 πŸ™ K2 & L1 = K1. β“‘{I} V1.
+#L1 #K2 #I #V2 #H
+elim (lpx_inv_pair2 β€¦ H) -H /2 width=4/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltop_fwd_length: βˆ€L1,L2. L1 πŸ™ L2 β†’ |L1| = |L2|.
+/2 width=2 by lpx_fwd_length/ qed-.
index 319569fe5cdd434a4428297c6606e4ec8c534eaf..837b1c670c65cc6726e129056cbccc0e87d51925 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv.ma".
+include "basic_2/grammar/lenv_append.ma".
 
 (* SHIFT OF A CLOSURE *******************************************************)
 
@@ -22,3 +22,25 @@ let rec shift L T on L β‰ match L with
 ].
 
 interpretation "shift (closure)" 'Append L T = (shift L T).
+
+(* Basic properties *********************************************************)
+
+lemma shift_append_assoc: βˆ€L,K. βˆ€T:term. (L @@ K) @@ T = L @@ K @@ T.
+#L #K elim K -K normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma shift_inj: βˆ€L1,L2. βˆ€T1,T2:term. L1 @@ T1 = L2 @@ T2 β†’ |L1| = |L2| β†’
+                 L1 = L2 βˆ§ T1 = T2.
+#L1 elim L1 -L1
+[ * normalize /2 width=1/
+  #L2 #I2 #V2 #T1 #T2 #_ <plus_n_Sm #H destruct
+| #L1 #H1 #V1 #IH * normalize
+  [ #T1 #T2 #_ <plus_n_Sm #H destruct
+  | #L2 #I2 #V2 #T1 #T2 #H1 #H2
+    elim (IH β€¦ H1 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+  ]
+]
+qed-.
+  
\ No newline at end of file
index a9790823379a393b1a682edcc8eae677a90211e6..83b65a3353d47ac1f57f3d656cdd0d5338b00f55 100644 (file)
@@ -35,27 +35,64 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-axiom discr_lpair_append_xy_x: βˆ€I,L,K,V. (L @@ K).β“‘{I}V = L β†’ βŠ₯.
-(*
-#I #L #K #V #H
-lapply (refl β€¦ (|L|)) <H in βŠ’ (? ? % ? β†’ ?); -H
-normalize >append_length -I -V #H
-*)
-lemma append_inv_sn: βˆ€L1,L2,L. L1 @@ L = L2 @@ L β†’ L1 = L2.
-#L1 #L2 #L elim L -L normalize //
-#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
-qed.
+lemma append_inj_sn: βˆ€K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 β†’ |K1| = |K2| β†’
+                     L1 = L2 βˆ§ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+  #K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
+| #K1 #I1 #V1 #IH * normalize
+  [ #L1 #L2 #_ <plus_n_Sm #H destruct
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+    elim (IH β€¦ e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+  ]
+]
+qed-.
 
 (* Note: lemma 750 *)
-lemma append_inv_dx: βˆ€L1,L2,L. L @@ L1 = L @@ L2 β†’ L1 = L2.
-#L1 elim L1 -L1
-[ * normalize //
-  #L2 #I2 #V2 #L #H
-  elim (discr_lpair_append_xy_x I2 L L2 V2 ?) //
-| #L1 #I1 #V1 #IHL1 * normalize
-  [ #L #H -IHL1 elim (discr_lpair_append_xy_x β€¦ H)
-  | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *)
-    -H >e0 /3 width=2/
+lemma append_inj_dx: βˆ€K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 β†’ |L1| = |L2| β†’
+                     L1 = L2 βˆ§ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+  #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
+  normalize in H2; >append_length in H2; #H
+  elim (plus_xySz_x_false β€¦ H)
+| #K1 #I1 #V1 #IH * normalize
+  [ #L1 #L2 #H1 #H2 destruct
+    normalize in H2; >append_length in H2; #H
+    elim (plus_xySz_x_false β€¦ (sym_eq β€¦ H))
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+    elim (IH β€¦ e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
   ]
 ]
-qed.
+qed-.
+
+lemma length_inv_pos_dx_append: βˆ€d,L. |L| = d + 1 β†’
+                                βˆƒβˆƒI,K,V. |K| = d & L = β‹†.β“‘{I}V @@ K.
+#d @(nat_ind_plus β€¦ d) -d
+[ #L #H 
+  elim (length_inv_pos_dx β€¦ H) -H #I #K #V #H
+  >(length_inv_zero_dx β€¦ H) -H #H destruct
+  @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (* /3/ does not work *)
+| #d #IHd #L #H
+  elim (length_inv_pos_dx β€¦ H) -H #I #K #V #H
+  elim (IHd β€¦ H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
+  @(ex2_3_intro β€¦ (K0.β“‘{I}V)) //
+]
+qed-.
+
+(* Basic_eliminators ********************************************************)
+
+fact lenv_ind_dx_aux: βˆ€R:predicate lenv. R β‹† β†’
+                      (βˆ€I,L,V. R L β†’ R (⋆.β“‘{I}V @@ L)) β†’
+                      βˆ€d,L. |L| = d β†’ R L.
+#R #Hatom #Hpair #d @(nat_ind_plus β€¦ d) -d
+[ #L #H >(length_inv_zero_dx β€¦ H) -H //
+| #d #IH #L #H
+  elim (length_inv_pos_dx_append β€¦ H) -H #I #K #V #H1 #H2 destruct /3 width=1/
+]
+qed-.
+
+lemma lenv_ind_dx: βˆ€R:predicate lenv. R β‹† β†’
+                   (βˆ€I,L,V. R L β†’ R (⋆.β“‘{I}V @@ L)) β†’
+                   βˆ€L. R L.
+/3 width=2 by lenv_ind_dx_aux/ qed-.
index 780edc161d69ca33af45095714622341b1eaf3cb..faf6de02d1dfe6e55d1253c97718637c0e1fdb4f 100644 (file)
@@ -22,3 +22,31 @@ let rec length L β‰ match L with
 ].
 
 interpretation "length (local environment)" 'card L = (length L).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma length_inv_zero_dx: βˆ€L. |L| = 0 β†’ L = β‹†.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_zero_sn: βˆ€L. 0 = |L| β†’ L = β‹†.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_pos_dx: βˆ€d,L. |L| = d + 1 β†’
+                         βˆƒβˆƒI,K,V. |K| = d & L = K. β“‘{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+  lapply (injective_plus_l β€¦ H) -H /2 width=5/
+]
+qed-.
+
+lemma length_inv_pos_sn: βˆ€d,L. d + 1 = |L| β†’
+                         βˆƒβˆƒI,K,V. d = |K| & L = K. β“‘{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+  lapply (injective_plus_l β€¦ H) -H /2 width=5/
+]
+qed-.
index 1b0c88e021c03d71a5c83bc0d0b321f44745d3e8..9de1599e4050336ef539a24b0febad10f7e49d4d 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_append.ma".
 
 (* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
 
@@ -80,6 +80,10 @@ lemma lpx_refl: βˆ€R. reflexive ? R β†’ reflexive β€¦ (lpx R).
 #R #HR #L elim L -L // /2 width=1/
 qed.
 
+lemma lpx_sym: βˆ€R. symmetric ? R β†’ symmetric β€¦ (lpx R).
+#R #HR #L1 #L2 #H elim H -H // /3 width=1/
+qed.
+
 lemma lpx_trans: βˆ€R. Transitive ? R β†’ Transitive β€¦ (lpx R).
 #R #HR #L1 #L #H elim H -L //
 #I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
@@ -129,3 +133,8 @@ lemma lpx_inv_TC: βˆ€R. reflexive ? R β†’
                   βˆ€L1,L2. lpx (TC β€¦ R) L1 L2 β†’ TC β€¦ (lpx R) L1 L2.
 #R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
 qed.
+
+lemma lpx_append: βˆ€R,K1,K2. lpx R K1 K2 β†’ βˆ€L1,L2. lpx R L1 L2 β†’
+                  lpx R (L1 @@ K1) (L2 @@ K2).
+#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma
new file mode 100644 (file)
index 0000000..931d075
--- /dev/null
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/lenv_length.ma".
+
+(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************)
+
+inductive lpx_bi (R:bi_relation lenv term): relation lenv β‰
+| lpx_bi_stom: lpx_bi R (⋆) (⋆)
+| lpx_bi_pair: βˆ€I,K1,K2,V1,V2.
+               lpx_bi R K1 K2 β†’ R K1 V1 K2 V2 β†’
+               lpx_bi R (K1. β“‘{I} V1) (K2. β“‘{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_bi_inv_atom1_aux: βˆ€R,L1,L2. lpx_bi R L1 L2 β†’ L1 = β‹† β†’ L2 = β‹†.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom1: βˆ€R,L2. lpx_bi R (⋆) L2 β†’ L2 = β‹†.
+/2 width=4 by lpx_bi_inv_atom1_aux/ qed-.
+
+fact lpx_bi_inv_pair1_aux: βˆ€R,L1,L2. lpx_bi R L1 L2 β†’
+                           βˆ€I,K1,V1. L1 = K1. β“‘{I} V1 β†’
+                           βˆƒβˆƒK2,V2. lpx_bi R K1 K2 &
+                                    R K1 V1 K2 V2 & L2 = K2. β“‘{I} V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair1: βˆ€R,I,K1,V1,L2. lpx_bi R (K1. β“‘{I} V1) L2 β†’
+                        βˆƒβˆƒK2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                 L2 = K2. β“‘{I} V2.
+/2 width=3 by lpx_bi_inv_pair1_aux/ qed-.
+
+fact lpx_bi_inv_atom2_aux: βˆ€R,L1,L2. lpx_bi R L1 L2 β†’ L2 = β‹† β†’ L1 = β‹†.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom2: βˆ€R,L1. lpx_bi R L1 (⋆) β†’ L1 = β‹†.
+/2 width=4 by lpx_bi_inv_atom2_aux/ qed-.
+
+fact lpx_bi_inv_pair2_aux: βˆ€R,L1,L2. lpx_bi R L1 L2 β†’
+                           βˆ€I,K2,V2. L2 = K2. β“‘{I} V2 β†’
+                           βˆƒβˆƒK1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                    L1 = K1. β“‘{I} V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair2: βˆ€R,I,L1,K2,V2. lpx_bi R L1 (K2. β“‘{I} V2) β†’
+                        βˆƒβˆƒK1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                 L1 = K1. β“‘{I} V1.
+/2 width=3 by lpx_bi_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_bi_fwd_length: βˆ€R,L1,L2. lpx_bi R L1 L2 β†’ |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_bi_refl: βˆ€R. bi_reflexive ? ? R β†’ reflexive β€¦ (lpx_bi R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
index a115260b9a57a4751a7751f047150fda769ad143..1b64f3c9082acbeec314fb418e1b582c2198bbea 100644 (file)
@@ -312,6 +312,10 @@ notation "hvbox( β¦ƒ L1, break T1 β¦„ βž‘ break β¦ƒ L2 , break T2 β¦„ )"
    non associative with precedence 45
    for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
 
+notation "hvbox( β¦ƒ L1 β¦„ βž‘ βž‘ break β¦ƒ L2 β¦„ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedAlt $L1 $L2 }.
+
 notation "hvbox( β¦ƒ h , break L β¦„ βŠ’ break term 46 T1 βžΈ break [ g ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'XPRed $h $g $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma
new file mode 100644 (file)
index 0000000..46c2011
--- /dev/null
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+
+definition fpr: bi_relation lenv term β‰
+                Ξ»L1,T1,L2,T2. |L1| = |L2| βˆ§ L1 @@ T1 βž‘ L2 @@ T2.
+
+interpretation
+   "focalized parallel reduction (closure)"
+   'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fpr_refl: bi_reflexive β€¦ fpr.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpr_inv_atom1: βˆ€L2,T1,T2. β¦ƒβ‹†, T1⦄ βž‘ β¦ƒL2, T2⦄ β†’ T1 βž‘ T2 βˆ§ L2 = β‹†.
+#L2 #T1 #T2 * #H
+lapply (length_inv_zero_sn β€¦ H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair1: βˆ€I,K1,L2,V1,T1,T2. β¦ƒK1.β“‘{I}V1, T1⦄ βž‘ β¦ƒL2, T2⦄ β†’
+                     βˆƒβˆƒK2,V2. β¦ƒK1, -β“‘{I}V1.T1⦄ βž‘ β¦ƒK2, -β“‘{I}V2.T2⦄  &
+                              L2 = K2.β“‘{I}V2.
+#I1 #K1 #L2 #V1 #T1 #T2 * #H
+elim (length_inv_pos_sn β€¦ H) -H #I2 #K2 #V2 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus β€¦ H) // #_ #H0 destruct /3 width=4/
+qed-.
+
+lemma fpr_inv_atom3: βˆ€L1,T1,T2. β¦ƒL1,T1⦄ βž‘ β¦ƒβ‹†,T2⦄ β†’ T1 βž‘ T2 βˆ§ L1 = β‹†.
+#L1 #T1 #T2 * #H
+lapply (length_inv_zero_dx β€¦ H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair3: βˆ€I,L1,K2,V2,T1,T2. β¦ƒL1, T1⦄ βž‘ β¦ƒK2.β“‘{I}V2, T2⦄ β†’
+                     βˆƒβˆƒK1,V1. β¦ƒK1, -β“‘{I}V1.T1⦄ βž‘ β¦ƒK2, -β“‘{I}V2.T2⦄  &
+                              L1 = K1.β“‘{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 * #H
+elim (length_inv_pos_dx β€¦ H) -H #I1 #K1 #V1 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus β€¦ H) // #_ #H0 destruct /3 width=4/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma
new file mode 100644 (file)
index 0000000..46f9845
--- /dev/null
@@ -0,0 +1,93 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/lenv_px_bi.ma".
+include "basic_2/reducibility/fpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
+
+(* alternative definition *)
+definition lfpra: relation lenv β‰ lpx_bi fpr.
+
+interpretation
+  "focalized parallel reduction (environment) alternative"
+  'FocalizedPRedAlt L1 L2 = (lfpra L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lfpra_refl: reflexive β€¦ lfpra.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfpra_inv_atom1: βˆ€L2. β¦ƒβ‹†β¦„ βž‘➑ β¦ƒL2⦄ β†’ L2 = β‹†.
+/2 width=2 by lpx_bi_inv_atom1/ qed-.
+
+lemma lfpra_inv_pair1: βˆ€K1,I,V1,L2. β¦ƒK1. β“‘{I} V1⦄ βž‘➑ β¦ƒL2⦄ β†’
+                       βˆƒβˆƒK2,V2. β¦ƒK1⦄ βž‘➑ β¦ƒK2⦄ & β¦ƒK1, V1⦄ βž‘ β¦ƒK2, V2⦄ &
+                                L2 = K2. β“‘{I} V2.
+/2 width=1 by lpx_bi_inv_pair1/ qed-.
+
+lemma lfpra_inv_atom2: βˆ€L1. β¦ƒL1⦄ βž‘➑ β¦ƒβ‹†β¦„ β†’ L1 = β‹†.
+/2 width=2 by lpx_bi_inv_atom2/ qed-.
+
+lemma lfpra_inv_pair2: βˆ€L1,K2,I,V2. β¦ƒL1⦄ βž‘➑ β¦ƒK2. β“‘{I} V2⦄ β†’
+                       βˆƒβˆƒK1,V1. β¦ƒK1⦄ βž‘➑ β¦ƒK2⦄ & β¦ƒK1, V1⦄ βž‘ β¦ƒK2, V2⦄ &
+                                L1 = K1. β“‘{I} V1.
+/2 width=1 by lpx_bi_inv_pair2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfpra_fwd_length: βˆ€L1,L2. β¦ƒL1⦄ βž‘➑ β¦ƒL2⦄ β†’ |L1| = |L2|.
+/2 width=2 by lpx_bi_fwd_length/ qed-.
+
+(****************************************************************************)
+
+lemma fpr_lfpra: βˆ€L1,T1,L2,T2. β¦ƒL1, T1⦄ βž‘ β¦ƒL2, T2⦄ β†’ β¦ƒL1⦄ βž‘➑ β¦ƒL2⦄.
+#L1 #T1 @(cw_wf_ind β€¦ L1 T1) -L1 -T1 *
+[ #T1 #_ #L2 #T2 #H
+  elim (fpr_inv_atom1 β€¦ H) -H #_ #H destruct //
+| #L1 #I #V1 #T1 #IH #Y #X #H
+  elim (fpr_inv_pair1 β€¦ H) -H #L2 #V2 #HL12 #H destruct
+  @lpx_bi_pair 
+  [ @(IH β€¦ HL12) 
+  | @IH 
+  
+  /3 width=4/
+
+lemma fpr_lfpra: βˆ€L1,L2,T1,T2. β¦ƒL1, T1⦄ βž‘ β¦ƒL2, T2⦄ β†’ β¦ƒL1⦄ βž‘➑ β¦ƒL2⦄.
+#L1 elim L1 -L1
+[ #L2 #T1 #T2 #H
+  elim (fpr_inv_atom1 β€¦ H) -H #_ #H destruct //
+| #L1 #I #V1 #IH #L2 #T1 #T2 #H
+  elim (fpr_inv_pair1 β€¦ H) -H #L #V #HL1 #H destruct
+  @lpx_bi_pair /2 width=3/ 
+  
+  /4 width=3/
+
+(*
+include "basic_2/reducibility/lcpr.ma".
+
+lemma lcpr_pair2: βˆ€L1,L2. L1 βŠ’ βž‘ L2 β†’ βˆ€V1,V2. β¦ƒL1, V1⦄ βž‘ β¦ƒL2, V2⦄ β†’
+                  βˆ€I. L1. β“‘{I} V1 βŠ’ βž‘ L2. β“‘{I} V2.
+#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
+#H1 #H2 #I
+@(ex2_1_intro β€¦ (L.β“‘{I}V1)) /2 width=1/
+@tpss_
+
+(*
+<(ltpss_fwd_length β€¦ HL2) /4 width=5/
+qed.
+*)
+*)
\ No newline at end of file
index d204eba79add94bd571ffb62aa04a91a47941205..a74757b2a17c7b36ea4f6b65d61681e13be89f32 100644 (file)
@@ -203,6 +203,36 @@ lemma tpr_inv_lref2: βˆ€T1,i. T1 βž‘ #i β†’
                       | βˆƒβˆƒV,T. T βž‘ #i & T1 = β“V. T.
 /2 width=3/ qed-.
 
+(* Basic forward lemmas *****************************************************)
+
+lemma tpr_fwd_shift1: βˆ€L1,T1,T. L1 @@ T1 βž‘ T β†’
+                      βˆƒβˆƒL2,T2. L1 πŸ™ L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx β€¦ L1) -L1
+[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H
+  elim (tpr_inv_bind1 β€¦ H) -H *
+  [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct
+    elim (IH β€¦ HT10) -IH -T1 #L2 #V2 #HL12 #H destruct
+    elim (tps_fwd_shift1 β€¦ HTX0) -V2 #L3 #X3 #HL23 #H destruct
+    lapply (ltop_trans β€¦ HL12 HL23) -L2 #HL13
+    @(ex2_2_intro β€¦ (⋆.β“‘{I}V0@@L3)) /2 width=4/ /3 width=1/
+  | #T0 #_ #_ #H destruct
+  ]
+]
+qed-.
+
+lemma tpr_fwd_shift_bind_minus: βˆ€L1,L2. |L1| = |L2| β†’ βˆ€I1,I2,V1,V2,T1,T2.
+                                L1 @@ -β“‘{I1}V1.T1 βž‘ L2 @@ -β“‘{I2}V2.T2 β†’
+                                L1 πŸ™ L2 βˆ§ I1 = I2.
+#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
+elim (tpr_fwd_shift1 (L1.β“‘{I1}V1) β€¦ H) -H #Y #X #HY #HX
+elim (ltop_inv_pair1 β€¦ HY) -HY #L #V #HL1 #H destruct
+elim (shift_inj (L2.β“‘{I2}V2) β€¦ HX ?) -HX
+[ #H1 #_ destruct /2 width=1/
+| lapply (ltop_fwd_length β€¦ HL1) -HL1 normalize // 
+]
+qed-.
+
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
    Basic_1: removed local theorems: 1: pr0_delta_tau
index db116f77e63b526eb2dc408ec50dfb645a0b9327..7e35dca7ca5e31ae427ae32bbe2ab50c19fcec83 100644 (file)
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lenv_top.ma".
 include "basic_2/substitution/ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
@@ -250,6 +251,17 @@ lemma tps_fwd_tw: βˆ€L,T1,T2,d,e. L βŠ’ T1 β–Ά [d, e] T2 β†’ #{T1} β‰€ #{T2}.
 /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
 qed-.
 
+lemma tps_fwd_shift1: βˆ€L1,L,T1,T,d,e. L βŠ’ L1 @@ T1 β–Ά [d, e] T β†’
+                      βˆƒβˆƒL2,T2. L1 πŸ™ L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx β€¦ L1) -L1
+[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
+  elim (tps_inv_bind1 β€¦ H) -H #V2 #T2 #_ #HT12 #H destruct
+  elim (IH β€¦ HT12) -IH -L -T1 -d -e #L2 #T #HL12 #H destruct
+  @(ex2_2_intro β€¦ (⋆.β“‘{I}V2@@L2)) /2 width=4/ /3 width=2/
+]
+qed-.
+
 (* Basic_1: removed theorems 25:
             subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
             subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
index c51873baa09bb9d8f0c46e2f502e378cb05af921..f7f5e35c4ce10e08a684f7c6f8955530c9899f73 100644 (file)
@@ -69,6 +69,13 @@ lemma false_lt_to_le: βˆ€x,y. (x < y β†’ βŠ₯) β†’ y β‰€ x.
 #Hxy elim (H Hxy)
 qed-.
 
+lemma plus_xySz_x_false: βˆ€z,x,y. x + y + S z = x β†’ βŠ₯.
+#z #x elim x -x normalize
+[ #y <plus_n_Sm #H destruct
+| /3 width=2/
+]
+qed-.
+
 (* iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)
index 36b5fc2a35339c14a222eb19fad339b0a6bf26a1..afb5d5aae05515a1c9801c45abb9064f2a55a91f 100644 (file)
@@ -156,3 +156,10 @@ for @{'eqF ? ? f g}.
 interpretation "functional extentional equality" 
 'eqF A B f g = (exteqF A B f g).
 
+(********** relations on unboxed pairs **********)
+
+definition bi_relation: Type[0] β†’ Type[0] β†’ Type[0]
+≝ Ξ»A,B.Aβ†’Bβ†’Aβ†’Bβ†’Prop.
+
+definition bi_reflexive: βˆ€A,B. βˆ€R :bi_relation A B. Prop
+≝ Ξ»A,B,R. βˆ€x,y. R x y x y.
index 9e4efa32aadf4a7a26dcb21bd63168c830938192..b51681d92d162db45eab6f31ac8d71934bac582f 100644 (file)
@@ -1579,15 +1579,15 @@ let predefined_classes = [
  ["z"; "ΞΆ"; "𝕫"; "𝐳"; "𝛇"; "β“©"; ] ;
  ["Z"; "ℨ"; "β„€"; "𝐙"; "Ⓩ"; ] ;
  ["0"; "𝟘"; "β“ͺ"; ] ;
- ["1"; "πŸ™"; "β‘ "; ] ;
- ["2"; "𝟚"; "β‘‘"; ] ;
- ["3"; "πŸ›"; "β‘’"; ] ;
- ["4"; "𝟜"; "β‘£"; ] ;
- ["5"; "𝟝"; "β‘€"; ] ;
- ["6"; "𝟞"; "β‘₯"; ] ;
- ["7"; "𝟟"; "⑦"; ] ;
- ["8"; "𝟠"; "⑧"; ] ;
- ["9"; "𝟑"; "⑨"; ] ;
+ ["1"; "πŸ™"; "β‘ "; "β“΅"; ] ;
+ ["2"; "𝟚"; "β‘‘"; "β“Ά"; ] ;
+ ["3"; "πŸ›"; "β‘’"; "β“·"; ] ;
+ ["4"; "𝟜"; "β‘£"; "β“Έ"; ] ;
+ ["5"; "𝟝"; "β‘€"; "β“Ή"; ] ;
+ ["6"; "𝟞"; "β‘₯"; "β“Ί"; ] ;
+ ["7"; "𝟟"; "⑦"; "β“»"; ] ;
+ ["8"; "𝟠"; "⑧"; "β“Ό"; ] ;
+ ["9"; "𝟑"; "⑨"; "β“½"; ] ;
  ]
 ;;