]> matita.cs.unibo.it Git - helm.git/commitdiff
- cpr is now defined and the cpr_flat propery is proved! (it did not
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 7 Aug 2011 20:44:42 +0000 (20:44 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 7 Aug 2011 20:44:42 +0000 (20:44 +0000)
hold in the first version of the calculus because cpr (aka pr2) was
badly designed).
- relocation properties of tpr closed!
- fixed bug in drop (base case was too restrictive)
- some refactoring

29 files changed:
matita/matita/lib/lambda-delta/notation.ma
matita/matita/lib/lambda-delta/reduction/cpr.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/reduction/lpr.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/reduction/lpr_defs.ma [deleted file]
matita/matita/lib/lambda-delta/reduction/tpr.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/reduction/tpr_defs.ma [deleted file]
matita/matita/lib/lambda-delta/reduction/tpr_lift.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/reduction/tpr_main.ma [deleted file]
matita/matita/lib/lambda-delta/reduction/tpr_pts.ma
matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
matita/matita/lib/lambda-delta/substitution/drop.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/drop_defs.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/drop_drop.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/drop_main.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/leq.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/leq_defs.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/lift.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/lift_defs.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/lift_lift.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/lift_main.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/lift_weight.ma
matita/matita/lib/lambda-delta/substitution/pts.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/substitution/pts_defs.ma [deleted file]
matita/matita/lib/lambda-delta/substitution/pts_lift.ma
matita/matita/lib/lambda-delta/syntax/length.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/xoa.conf.xml
matita/matita/lib/lambda-delta/xoa.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/xoa_defs.ma [deleted file]
matita/matita/lib/lambda-delta/xoa_props.ma

index 86e31894c92c58d15cfab77a6b35f624c69ff558..375d06abc776e6af2eb9c444c7619bbd50053caf 100644 (file)
@@ -11,7 +11,7 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM Ξ»Ξ΄ ****************************************)
 
-(*  *****************************************************************)
+(* Syntax *******************************************************************)
 
 notation "hvbox( β‹† )"
  non associative with precedence 90
@@ -36,7 +36,11 @@ notation "hvbox( π•— { I } break (term 90 T1) . break (term 90 T) )"
 notation "hvbox( T . break π•“ { I } break (term 90 T1) )"
  non associative with precedence 89
  for @{ 'DBind $T $I $T1 }.
-
+(*
+notation "hvbox( |  L  | )"
+ non associative with precedence 70
+ for @{ 'Length $L }.
+*)
 notation "hvbox( # term 90 x )"
  non associative with precedence 90
  for @{ 'Weight $x }.
@@ -45,7 +49,7 @@ notation "hvbox( # [ x , break y ] )"
  non associative with precedence 90
  for @{ 'Weight $x $y }.
 
-(* substitution *************************************************************)
+(* Substitution *************************************************************)
 
 notation "hvbox( T1 break [ d , break e ] β‰ˆ break T2 )"
    non associative with precedence 45
@@ -63,7 +67,7 @@ notation "hvbox( L βŠ’ break term 90 T1 break [ d , break e ] β‰« break T2 )"
    non associative with precedence 45
    for @{ 'PSubst $L $T1 $d $e $T2 }.
 
-(* reduction ****************************************************************)
+(* Reduction ****************************************************************)
 
 notation "hvbox( T1 β‡’ break T2 )"
    non associative with precedence 45
diff --git a/matita/matita/lib/lambda-delta/reduction/cpr.ma b/matita/matita/lib/lambda-delta/reduction/cpr.ma
new file mode 100644 (file)
index 0000000..80ccfd9
--- /dev/null
@@ -0,0 +1,53 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/length.ma".
+include "lambda-delta/reduction/tpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+definition cpr: lenv β†’ term β†’ term β†’ Prop β‰
+   Ξ»L,T1,T2. βˆƒβˆƒT. T1 β‡’ T & L βŠ’ T [0, |L|] β‰« T2.
+
+interpretation
+   "context-sensitive parallel reduction (term)"
+   'PRed L T1 T2 = (cpr L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpr_pr: βˆ€T1,T2. T1 β‡’ T2 β†’ βˆ€L. L βŠ’ T1 β‡’ T2.
+/2/ qed.
+
+axiom cpr_pts: βˆ€L,T1,T2,d,e. L βŠ’ T1 [d, e] β‰« T2 β†’ L βŠ’ T1 β‡’ T2.
+
+lemma cpr_refl: βˆ€L,T. L βŠ’ T β‡’ T.
+/2/ qed.
+
+(* NOTE: new property *)
+lemma cpr_flat: βˆ€I,L,V1,V2,T1,T2.
+                L βŠ’ V1 β‡’ V2 β†’ L βŠ’ T1 β‡’ T2 β†’ L βŠ’ π•—{I} V1. T1 β‡’ π•—{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
+qed.
+
+axiom cpr_delta: βˆ€L,K,V0,V,i.
+                 β†“[0, i] L β‰‘ K. π•“{Abbr} V0 β†’ β†‘[0, i + 1] V0 β‰‘ V β†’ L βŠ’ #i β‡’ V.
+(*
+#L #K #V0 #V #i #HLK #HV0
+@ex2_1_intro [2: // |1: skip ]
+@pts_subst [4,6,7,8: // |1,2,3: skip |5: 
+*)
+
+lemma cpr_cast: βˆ€L,V,T1,T2.
+                L βŠ’ T1 β‡’ T2 β†’ L βŠ’ π•—{Cast} V. T1 β‡’ T2.
+#L #V #T1 #T2 * /3/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
diff --git a/matita/matita/lib/lambda-delta/reduction/lpr.ma b/matita/matita/lib/lambda-delta/reduction/lpr.ma
new file mode 100644 (file)
index 0000000..92f7721
--- /dev/null
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "lambda-delta/reduction/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+inductive lpr: lenv β†’ lenv β†’ Prop β‰
+| lpr_sort: lpr (⋆) (⋆)
+| lpr_item: βˆ€K1,K2,I,V1,V2.
+            lpr K1 K2 β†’ V1 β‡’ V2 β†’ lpr (K1. π•“{I} V1) (K2. π•“{I} V2) (*𝕓*)
+.
+
+interpretation
+  "context-free parallel reduction (environment)"
+  'PRed L1 L2 = (lpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpr_inv_item1_aux: βˆ€L1,L2. L1 β‡’ L2 β†’ βˆ€K1,I,V1. L1 = K1. π•“{I} V1 β†’
+                         βˆƒβˆƒK2,V2. K1 β‡’ K2 & V1 β‡’ V2 & L2 = K2. π•“{I} V2.
+#L1 #L2 * -L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+lemma lpr_inv_item1: βˆ€K1,I,V1,L2. K1. π•“{I} V1 β‡’ L2 β†’
+                     βˆƒβˆƒK2,V2. K1 β‡’ K2 & V1 β‡’ V2 & L2 = K2. π•“{I} V2.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
deleted file mode 100644 (file)
index 8adec5c..0000000
+++ /dev/null
@@ -1,41 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "lambda-delta/reduction/tpr_defs.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-inductive lpr: lenv β†’ lenv β†’ Prop β‰
-| lpr_sort: lpr (⋆) (⋆)
-| lpr_item: βˆ€K1,K2,I,V1,V2.
-            lpr K1 K2 β†’ V1 β‡’ V2 β†’ lpr (K1. π•“{I} V1) (K2. π•“{I} V2) (*𝕓*)
-.
-
-interpretation
-  "context-free parallel reduction (environment)"
-  'PRed L1 L2 = (lpr L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpr_inv_item1_aux: βˆ€L1,L2. L1 β‡’ L2 β†’ βˆ€K1,I,V1. L1 = K1. π•“{I} V1 β†’
-                         βˆƒβˆƒK2,V2. K1 β‡’ K2 & V1 β‡’ V2 & L2 = K2. π•“{I} V2.
-#L1 #L2 * -L1 L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
-]
-qed.
-
-lemma lpr_inv_item1: βˆ€K1,I,V1,L2. K1. π•“{I} V1 β‡’ L2 β†’
-                     βˆƒβˆƒK2,V2. K1 β‡’ K2 & V1 β‡’ V2 & L2 = K2. π•“{I} V2.
-/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr.ma
new file mode 100644 (file)
index 0000000..3145cca
--- /dev/null
@@ -0,0 +1,240 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/pts.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+inductive tpr: term β†’ term β†’ Prop β‰
+| tpr_sort : βˆ€k. tpr (⋆k) (⋆k)
+| tpr_lref : βˆ€i. tpr (#i) (#i)
+| tpr_bind : βˆ€I,V1,V2,T1,T2. tpr V1 V2 β†’ tpr T1 T2 β†’
+             tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+| tpr_flat : βˆ€I,V1,V2,T1,T2. tpr V1 V2 β†’ tpr T1 T2 β†’
+             tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+| tpr_beta : βˆ€V1,V2,W,T1,T2.
+             tpr V1 V2 β†’ tpr T1 T2 β†’
+             tpr (π•š{Appl} V1. π•š{Abst} W. T1) (π•š{Abbr} V2. T2)
+| tpr_delta: βˆ€V1,V2,T1,T2,T.
+             tpr V1 V2 β†’ tpr T1 T2 β†’ β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T β†’
+             tpr (π•š{Abbr} V1. T1) (π•š{Abbr} V2. T)
+| tpr_theta: βˆ€V,V1,V2,W1,W2,T1,T2.
+             tpr V1 V2 β†’ β†‘[0,1] V2 β‰‘ V β†’ tpr W1 W2 β†’ tpr T1 T2 β†’
+             tpr (π•š{Appl} V1. π•š{Abbr} W1. T1) (π•š{Abbr} W2. π•š{Appl} V. T2)
+| tpr_zeta : βˆ€V,T,T1,T2. β†‘[0,1] T1 β‰‘ T β†’ tpr T1 T2 β†’
+             tpr (π•š{Abbr} V. T) T2
+| tpr_tau  : βˆ€V,T1,T2. tpr T1 T2 β†’ tpr (π•š{Cast} V. T1) T2
+.
+
+interpretation
+   "context-free parallel reduction (term)"
+   'PRed T1 T2 = (tpr T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tpr_refl: βˆ€T. T β‡’ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tpr_inv_sort1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€k. U1 = β‹†k β†’ U2 = β‹†k.
+#U1 #U2 * -U1 U2
+[ #k0 #k #H destruct -k0 //
+| #i #k #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
+| #V #T #T1 #T2 #_ #_ #k #H destruct
+| #V #T1 #T2 #_ #k #H destruct
+]
+qed.
+
+lemma tpr_inv_sort1: βˆ€k,U2. β‹†k β‡’ U2 β†’ U2 = β‹†k.
+/2/ qed.
+
+lemma tpr_inv_lref1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€i. U1 = #i β†’ U2 = #i.
+#U1 #U2 * -U1 U2
+[ #k #i #H destruct
+| #j #i #H destruct -j //
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #_ #_ #i #H destruct
+| #V #T1 #T2 #_ #i #H destruct
+]
+qed.
+
+lemma tpr_inv_lref1: βˆ€i,U2. #i β‡’ U2 β†’ U2 = #i.
+/2/ qed.
+
+lemma tpr_inv_abbr1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Abbr} V1. T1 β†’
+                         βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abbr} V2. T2
+                          | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
+                                       β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
+                                       U2 = π•š{Abbr} V2. T
+                          | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & T β‡’ U2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_abbr1: βˆ€V1,T1,U2. π•š{Abbr} V1. T1 β‡’ U2 β†’
+                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abbr} V2. T2
+                      | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
+                                   β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
+                                   U2 = π•š{Abbr} V2. T
+                      | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & tpr T U2.
+/2/ qed.
+
+lemma tpr_inv_abst1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Abst} V1. T1 β†’
+                         βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abst} V2. T2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_abst1: βˆ€V1,T1,U2. π•š{Abst} V1. T1 β‡’ U2 β†’
+                     βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abst} V2. T2.
+/2/ qed.
+
+lemma tpr_inv_bind1: βˆ€V1,T1,U2,I. π•“{I} V1. T1 β‡’ U2 β†’
+                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•“{I} V2. T2
+                      | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
+                                   β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
+                                   U2 = π•š{Abbr} V2. T & I = Abbr
+                      | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & tpr T U2 & I = Abbr.
+#V1 #T1 #U2 * #H
+[ elim (tpr_inv_abbr1 β€¦ H) -H * /3 width=7/
+| /3/
+]
+qed.
+
+lemma tpr_inv_appl1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,U0. U1 = π•š{Appl} V1. U0 β†’
+                         βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
+                                                U2 = π•š{Appl} V2. T2
+                          | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
+                                                U0 = π•š{Abst} W. T1 &
+                                                U2 = π•“{Abbr} V2. T2
+                          | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
+                                                β†‘[0,1] V2 β‰‘ V &
+                                                U0 = π•š{Abbr} W1. T1 &
+                                                U2 = π•š{Abbr} W2. π•š{Appl} V. T2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
+  destruct -V1 T0 /3 width=12/
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_appl1: βˆ€V1,U0,U2. π•š{Appl} V1. U0 β‡’ U2 β†’
+                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
+                                            U2 = π•š{Appl} V2. T2
+                      | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
+                                            U0 = π•š{Abst} W. T1 &
+                                            U2 = π•“{Abbr} V2. T2
+                      | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
+                                            β†‘[0,1] V2 β‰‘ V &
+                                            U0 = π•š{Abbr} W1. T1 &
+                                            U2 = π•š{Abbr} W2. π•š{Appl} V. T2.
+/2/ qed.
+
+lemma tpr_inv_cast1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Cast} V1. T1 β†’
+                           (βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Cast} V2. T2)
+                         βˆ¨ T1 β‡’ U2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
+]
+qed.
+
+lemma tpr_inv_cast1: βˆ€V1,T1,U2. π•š{Cast} V1. T1 β‡’ U2 β†’
+                       (βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Cast} V2. T2)
+                     βˆ¨ T1 β‡’ U2.
+/2/ qed.
+
+lemma tpr_inv_flat1: βˆ€V1,U0,U2,I. π•—{I} V1. U0 β‡’ U2 β†’
+                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
+                                            U2 = π•—{I} V2. T2
+                      | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
+                                            U0 = π•š{Abst} W. T1 &
+                                            U2 = π•“{Abbr} V2. T2 & I = Appl
+                      | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
+                                            β†‘[0,1] V2 β‰‘ V &
+                                            U0 = π•š{Abbr} W1. T1 &
+                                            U2 = π•š{Abbr} W2. π•š{Appl} V. T2 &
+                                            I = Appl
+                      |                     (U0 β‡’ U2 βˆ§ I = Cast).
+#V1 #U0 #U2 * #H
+[ elim (tpr_inv_appl1 β€¦ H) -H * /3 width=12/
+| elim (tpr_inv_cast1 β€¦ H) -H [1: *] /3 width=5/
+]
+qed.
+
+lemma tpr_inv_lref2_aux: βˆ€T1,T2. T1 β‡’ T2 β†’ βˆ€i. T2 = #i β†’
+                         βˆ¨βˆ¨           T1 = #i
+                          | βˆƒβˆƒV,T,T0. β†‘[O,1] T0 β‰‘ T & T0 β‡’ #i &
+                                      T1 = π•š{Abbr} V. T
+                          | βˆƒβˆƒV,T.    T β‡’ #i & T1 = π•š{Cast} V. T.
+#T1 #T2 * -T1 T2
+[ #k #i #H destruct
+| #j #i /2/
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
+| #V #T1 #T2 #HT12 #i #H destruct /3/
+]
+qed.
+
+lemma tpr_inv_lref2: βˆ€T1,i. T1 β‡’ #i β†’
+                     βˆ¨βˆ¨           T1 = #i
+                      | βˆƒβˆƒV,T,T0. β†‘[O,1] T0 β‰‘ T & T0 β‡’ #i &
+                                  T1 = π•“{Abbr} V. T
+                      | βˆƒβˆƒV,T.    T β‡’ #i & T1 = π•—{Cast} V. T.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
deleted file mode 100644 (file)
index cb96099..0000000
+++ /dev/null
@@ -1,240 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/pts_defs.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-inductive tpr: term β†’ term β†’ Prop β‰
-| tpr_sort : βˆ€k. tpr (⋆k) (⋆k)
-| tpr_lref : βˆ€i. tpr (#i) (#i)
-| tpr_bind : βˆ€I,V1,V2,T1,T2. tpr V1 V2 β†’ tpr T1 T2 β†’
-             tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
-| tpr_flat : βˆ€I,V1,V2,T1,T2. tpr V1 V2 β†’ tpr T1 T2 β†’
-             tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
-| tpr_beta : βˆ€V1,V2,W,T1,T2.
-             tpr V1 V2 β†’ tpr T1 T2 β†’
-             tpr (π•š{Appl} V1. π•š{Abst} W. T1) (π•š{Abbr} V2. T2)
-| tpr_delta: βˆ€V1,V2,T1,T2,T.
-             tpr V1 V2 β†’ tpr T1 T2 β†’ β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T β†’
-             tpr (π•š{Abbr} V1. T1) (π•š{Abbr} V2. T)
-| tpr_theta: βˆ€V,V1,V2,W1,W2,T1,T2.
-             tpr V1 V2 β†’ β†‘[0,1] V2 β‰‘ V β†’ tpr W1 W2 β†’ tpr T1 T2 β†’
-             tpr (π•š{Appl} V1. π•š{Abbr} W1. T1) (π•š{Abbr} W2. π•š{Appl} V. T2)
-| tpr_zeta : βˆ€V,T,T1,T2. β†‘[0,1] T1 β‰‘ T β†’ tpr T1 T2 β†’
-             tpr (π•š{Abbr} V. T) T2
-| tpr_tau  : βˆ€V,T1,T2. tpr T1 T2 β†’ tpr (π•š{Cast} V. T1) T2
-.
-
-interpretation
-   "context-free parallel reduction (term)"
-   'PRed T1 T2 = (tpr T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma tpr_refl: βˆ€T. T β‡’ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tpr_inv_sort1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€k. U1 = β‹†k β†’ U2 = β‹†k.
-#U1 #U2 * -U1 U2
-[ #k0 #k #H destruct -k0 //
-| #i #k #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
-| #V #T #T1 #T2 #_ #_ #k #H destruct
-| #V #T1 #T2 #_ #k #H destruct
-]
-qed.
-
-lemma tpr_inv_sort1: βˆ€k,U2. β‹†k β‡’ U2 β†’ U2 = β‹†k.
-/2/ qed.
-
-lemma tpr_inv_lref1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€i. U1 = #i β†’ U2 = #i.
-#U1 #U2 * -U1 U2
-[ #k #i #H destruct
-| #j #i #H destruct -j //
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #_ #_ #i #H destruct
-| #V #T1 #T2 #_ #i #H destruct
-]
-qed.
-
-lemma tpr_inv_lref1: βˆ€i,U2. #i β‡’ U2 β†’ U2 = #i.
-/2/ qed.
-
-lemma tpr_inv_abbr1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Abbr} V1. T1 β†’
-                         βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abbr} V2. T2
-                          | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
-                                       β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
-                                       U2 = π•š{Abbr} V2. T
-                          | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & T β‡’ U2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_abbr1: βˆ€V1,T1,U2. π•š{Abbr} V1. T1 β‡’ U2 β†’
-                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abbr} V2. T2
-                      | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
-                                   β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
-                                   U2 = π•š{Abbr} V2. T
-                      | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & tpr T U2.
-/2/ qed.
-
-lemma tpr_inv_abst1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Abst} V1. T1 β†’
-                         βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abst} V2. T2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_abst1: βˆ€V1,T1,U2. π•š{Abst} V1. T1 β‡’ U2 β†’
-                     βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Abst} V2. T2.
-/2/ qed.
-
-lemma tpr_inv_bind1: βˆ€V1,T1,U2,I. π•“{I} V1. T1 β‡’ U2 β†’
-                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•“{I} V2. T2
-                      | βˆƒβˆƒV2,T2,T. V1 β‡’ V2 & T1 β‡’ T2 &
-                                   β‹†.  π•“{Abbr} V2 βŠ’ T2 [0, 1] β‰« T &
-                                   U2 = π•š{Abbr} V2. T & I = Abbr
-                      | βˆƒβˆƒT. β†‘[0,1] T β‰‘ T1 & tpr T U2 & I = Abbr.
-#V1 #T1 #U2 * #H
-[ elim (tpr_inv_abbr1 β€¦ H) -H * /3 width=7/
-| /3/
-]
-qed.
-
-lemma tpr_inv_appl1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,U0. U1 = π•š{Appl} V1. U0 β†’
-                         βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
-                                                U2 = π•š{Appl} V2. T2
-                          | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
-                                                U0 = π•š{Abst} W. T1 &
-                                                U2 = π•“{Abbr} V2. T2
-                          | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
-                                                β†‘[0,1] V2 β‰‘ V &
-                                                U0 = π•š{Abbr} W1. T1 &
-                                                U2 = π•š{Abbr} W2. π•š{Appl} V. T2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
-  destruct -V1 T0 /3 width=12/
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_appl1: βˆ€V1,U0,U2. π•š{Appl} V1. U0 β‡’ U2 β†’
-                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
-                                            U2 = π•š{Appl} V2. T2
-                      | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
-                                            U0 = π•š{Abst} W. T1 &
-                                            U2 = π•“{Abbr} V2. T2
-                      | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
-                                            β†‘[0,1] V2 β‰‘ V &
-                                            U0 = π•š{Abbr} W1. T1 &
-                                            U2 = π•š{Abbr} W2. π•š{Appl} V. T2.
-/2/ qed.
-
-lemma tpr_inv_cast1_aux: βˆ€U1,U2. U1 β‡’ U2 β†’ βˆ€V1,T1. U1 = π•š{Cast} V1. T1 β†’
-                           (βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Cast} V2. T2)
-                         βˆ¨ T1 β‡’ U2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
-]
-qed.
-
-lemma tpr_inv_cast1: βˆ€V1,T1,U2. π•š{Cast} V1. T1 β‡’ U2 β†’
-                       (βˆƒβˆƒV2,T2. V1 β‡’ V2 & T1 β‡’ T2 & U2 = π•š{Cast} V2. T2)
-                     βˆ¨ T1 β‡’ U2.
-/2/ qed.
-
-lemma tpr_inv_flat1: βˆ€V1,U0,U2,I. π•—{I} V1. U0 β‡’ U2 β†’
-                     βˆ¨βˆ¨ βˆƒβˆƒV2,T2.            V1 β‡’ V2 & U0 β‡’ T2 &
-                                            U2 = π•—{I} V2. T2
-                      | βˆƒβˆƒV2,W,T1,T2.       V1 β‡’ V2 & T1 β‡’ T2 &
-                                            U0 = π•š{Abst} W. T1 &
-                                            U2 = π•“{Abbr} V2. T2 & I = Appl
-                      | βˆƒβˆƒV2,V,W1,W2,T1,T2. V1 β‡’ V2 & W1 β‡’ W2 & T1 β‡’ T2 &
-                                            β†‘[0,1] V2 β‰‘ V &
-                                            U0 = π•š{Abbr} W1. T1 &
-                                            U2 = π•š{Abbr} W2. π•š{Appl} V. T2 &
-                                            I = Appl
-                      |                     (U0 β‡’ U2 βˆ§ I = Cast).
-#V1 #U0 #U2 * #H
-[ elim (tpr_inv_appl1 β€¦ H) -H * /3 width=12/
-| elim (tpr_inv_cast1 β€¦ H) -H [1: *] /3 width=5/
-]
-qed.
-
-lemma tpr_inv_lref2_aux: βˆ€T1,T2. T1 β‡’ T2 β†’ βˆ€i. T2 = #i β†’
-                         βˆ¨βˆ¨           T1 = #i
-                          | βˆƒβˆƒV,T,T0. β†‘[O,1] T0 β‰‘ T & T0 β‡’ #i &
-                                      T1 = π•š{Abbr} V. T
-                          | βˆƒβˆƒV,T.    T β‡’ #i & T1 = π•š{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #k #i #H destruct
-| #j #i /2/
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
-]
-qed.
-
-lemma tpr_inv_lref2: βˆ€T1,i. T1 β‡’ #i β†’
-                     βˆ¨βˆ¨           T1 = #i
-                      | βˆƒβˆƒV,T,T0. β†‘[O,1] T0 β‰‘ T & T0 β‡’ #i &
-                                  T1 = π•“{Abbr} V. T
-                      | βˆƒβˆƒV,T.    T β‡’ #i & T1 = π•—{Cast} V. T.
-/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_lift.ma b/matita/matita/lib/lambda-delta/reduction/tpr_lift.ma
new file mode 100644 (file)
index 0000000..d639f71
--- /dev/null
@@ -0,0 +1,102 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "lambda-delta/substitution/pts_lift.ma".
+include "lambda-delta/reduction/tpr.ma".
+
+(* Relocation properties ****************************************************)
+
+lemma tpr_lift: βˆ€T1,T2. T1 β‡’ T2 β†’
+                βˆ€d,e,U1. β†‘[d, e] T1 β‰‘ U1 β†’ βˆ€U2. β†‘[d, e] T2 β‰‘ U2 β†’ U1 β‡’ U2.
+#T1 #T2 #H elim H -H T1 T2
+[ #k #d #e #U1 #HU1 #U2 #HU2
+  lapply (lift_mono β€¦ HU1 β€¦ HU2) -HU1 #H destruct -U1; 
+  lapply (lift_inv_sort1 β€¦ HU2) -HU2 #H destruct -U2 //
+| #i #d #e #U1 #HU1 #U2 #HU2
+  lapply (lift_mono β€¦ HU1 β€¦ HU2) -HU1 #H destruct -U1;
+  lapply (lift_inv_lref1 β€¦ HU2) * * #Hid #H destruct -U2 //
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+  elim (lift_inv_bind1 β€¦ HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+  elim (lift_inv_bind1 β€¦ HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 β€¦ HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+  elim (lift_inv_flat1 β€¦ HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 β€¦ HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+  elim (lift_inv_bind1 β€¦ HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+  elim (lift_inv_bind1 β€¦ HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
+| #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+  elim (lift_inv_bind1 β€¦ HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+  elim (lift_inv_bind1 β€¦ HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
+  elim (lift_total T2 (d + 1) e) #U2 #HTU2
+  @tpr_delta
+  [4: @(pts_lift_le β€¦ HT2 β€¦ HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *)
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 β€¦ HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+  elim (lift_inv_bind1 β€¦ HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+  elim (lift_inv_bind1 β€¦ HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
+  elim (lift_inv_flat1 β€¦ HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
+  elim (lift_trans_ge β€¦ HV2 β€¦ HV3 ?) -HV2 HV3 V // /3/
+| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
+  elim (lift_inv_bind1 β€¦ HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
+  elim (lift_trans_ge β€¦ HT1 β€¦ HT3 ?) -HT1 HT3 T // /3 width=6/
+| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
+  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/
+]
+qed.
+
+lemma tpr_inv_lift: βˆ€T1,T2. T1 β‡’ T2 β†’
+                    βˆ€d,e,U1. β†‘[d, e] U1 β‰‘ T1 β†’
+                    βˆƒβˆƒU2. β†‘[d, e] U2 β‰‘ T2 & U1 β‡’ U2.
+#T1 #T2 #H elim H -H T1 T2
+[ #k #d #e #U1 #HU1
+  lapply (lift_inv_sort2 β€¦ HU1) -HU1 #H destruct -U1 /2/
+| #i #d #e #U1 #HU1
+  lapply (lift_inv_lref2 β€¦ HU1) -HU1 * * #Hid #H destruct -U1 /3/
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
+  elim (lift_inv_bind2 β€¦ HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
+  elim (IHV12 β€¦ HV01) -IHV12 HV01;
+  elim (IHT12 β€¦ HT01) -IHT12 HT01 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
+  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
+  elim (IHV12 β€¦ HV01) -IHV12 HV01;
+  elim (IHT12 β€¦ HT01) -IHT12 HT01 /3 width=5/
+| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
+  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
+  elim (lift_inv_bind2 β€¦ HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
+  elim (IHV12 β€¦ HV01) -IHV12 HV01;
+  elim (IHT12 β€¦ HT01) -IHT12 HT01 /3 width=5/
+| #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
+  elim (lift_inv_bind2 β€¦ HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
+  elim (IHV12 β€¦ HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
+  elim (IHT12 β€¦ HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
+  elim (pts_inv_lift1_le β€¦ HT20 β€¦ HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+  @ex2_1_intro  [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *)
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
+  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
+  elim (lift_inv_bind2 β€¦ HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
+  elim (IHV12 β€¦ HV01) -IHV12 HV01 #V3 #HV32 #HV03
+  elim (IHW12 β€¦ HW01) -IHW12 HW01 #W3 #HW32 #HW03
+  elim (IHT12 β€¦ HT01) -IHT12 HT01 #T3 #HT32 #HT03
+  elim (lift_trans_le β€¦ HV32 β€¦ HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
+  @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *)
+| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
+  elim (lift_inv_bind2 β€¦ HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
+  elim (lift_div_le β€¦ HT1 β€¦ HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
+  elim (IHT12 β€¦ HT1) -IHT12 HT1 /3 width=5/
+| #V #T1 #T2 #_ #IHT12 #d #e #X #HX
+  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
+  elim (IHT12 β€¦ HT01) -IHT12 HT01 /3/
+]
+qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_main.ma b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma
deleted file mode 100644 (file)
index 1d5d7d7..0000000
+++ /dev/null
@@ -1,130 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "lambda-delta/substitution/lift_main.ma".
-include "lambda-delta/substitution/drop_main.ma".
-*)
-include "lambda-delta/reduction/tpr_defs.ma".
-
-axiom tpr_lift: βˆ€T1,T2. T1 β‡’ T2 β†’
-                βˆ€d,e,U1. β†‘[d, e] T1 β‰‘ U1 β†’ βˆ€U2. β†‘[d, e] T2 β‰‘ U2 β†’ U1 β‡’ U2.
-(*
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2
-  lapply (lift_mono β€¦ HU1 β€¦ HU2) -HU1 #H destruct -U1; 
-  lapply (lift_inv_sort1 β€¦ HU2) -HU2 #H destruct -U2 //
-| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2
-  lapply (lift_mono β€¦ HU1 β€¦ HU2) -HU1 #H destruct -U1;
-  lapply (lift_inv_lref1 β€¦ HU2) * * #Hid #H destruct -U2 //
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
-  elim (lift_inv_bind1 β€¦ HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
-  elim (lift_inv_bind1 β€¦ HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
-  /5 width=5/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 β€¦ HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
-  elim (lift_inv_flat1 β€¦ HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
-  /3 width=5/
-| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 β€¦ HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
-  elim (lift_inv_bind1 β€¦ HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
-  elim (lift_inv_bind1 β€¦ HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2
-  /5 width=5/
-| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03
-  lapply (lift_inv_lref1 β€¦ HX) -HX * * #Hid #H destruct -X;
-  [ -HV12;
-    elim (lift_trans_ge β€¦ HV20 β€¦ HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03
-    elim (drop_trans_le β€¦ HKL β€¦ HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0
-    elim (drop_inv_skip2 β€¦ HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L;
-    @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *)
-  | -IHV12;
-    lapply (lift_trans_be β€¦ HV20 β€¦ HV03 ? ?) -HV20 HV03 V0 /2/ #HV23
-    lapply (drop_trans_ge β€¦ HKL β€¦ HLK0 ?) -HKL HLK0 L // -Hid #HKK0
-    @pr_delta /width=6/
-  ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 β€¦ HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
-  elim (lift_inv_bind1 β€¦ HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
-  elim (lift_inv_bind1 β€¦ HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
-  elim (lift_inv_flat1 β€¦ HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
-  lapply (lift_trans_ge β€¦ HV2 β€¦ HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3
-  @pr_theta /3 width=5/
-| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20
-  elim (lift_inv_bind1 β€¦ HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
-  lapply (lift_trans_ge β€¦ HT1 β€¦ HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3
-  @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *)
-| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2
-  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X;
-  @pr_tau /2 width=5/
-]
-qed.
-*)
-axiom tpr_inv_lift: βˆ€T1,T2. T1 β‡’ T2 β†’
-                    βˆ€d,e,U1. β†‘[d, e] U1 β‰‘ T1 β†’
-                    βˆƒβˆƒU2. β†‘[d, e] U2 β‰‘ T2 & U1 β‡’ U2.
-(*
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #d #e #K #_ #U1 #HU1
-  lapply (lift_inv_sort2 β€¦ HU1) -HU1 #H destruct -U1 /2/
-| #L #i #d #e #K #_ #U1 #HU1
-  lapply (lift_inv_lref2 β€¦ HU1) -HU1 * * #Hid #H destruct -U1 /3/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_bind2 β€¦ HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
-  elim (IHV12 β€¦ HLK β€¦ HV01) -IHV12 #V3 #HV32 #HV03
-  elim (IHT12 β€¦ HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
-  elim (IHV12 β€¦ HLK β€¦ HV01) -IHV12 HV01 #V3 #HV32 #HV03
-  elim (IHT12 β€¦ HLK β€¦ HT01) -IHT12 HT01 HLK /3 width=5/
-| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
-  elim (lift_inv_bind2 β€¦ HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
-  elim (IHV12 β€¦ HLK β€¦ HV01) -IHV12 HV01 #V3 #HV32 #HV03
-  elim (IHT12 β€¦ HT01) -IHT12 HT01
-    [3: -HV32 HV03 @(drop_skip β€¦ HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *)
-    -HLK HW01
-  /3 width=5/
-| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX
-  lapply (lift_inv_lref2 β€¦ HX) -HX * * #Hid #HX destruct -X;
-  [ -HV12;
-    elim (drop_conf_lt β€¦ HLK β€¦ HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31
-    elim (IHV12 β€¦ HK0L β€¦ HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34
-    elim (lift_trans_le β€¦ HV42 β€¦ HV20 ?) -HV42 HV20 V2 // #V2 #HV42
-    >arith5 // -Hid #HV20  
-    @(ex2_1_intro β€¦ V2) /2 width=6/ (**) (* /3 width=8/ is slow *)
-  | -IHV12;
-    lapply (drop_conf_ge β€¦ HLK β€¦ HLK0 Hid) -HLK HLK0 L #HK
-    elim (lift_free β€¦ HV20 d (i - e + 1) ? ? ?) -HV20 /2/
-    >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *)
-  ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
-  elim (lift_inv_bind2 β€¦ HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
-  elim (IHV12 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03
-  elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03
-  elim (IHT12 β€¦ HT01) -IHT12 HT01
-    [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip β€¦ HLK) /2/ |2: skip ] (**) (* /3/ is too slow *)
-    -HLK HW01 #T3 #HT32 #HT03
-  elim (lift_trans_le β€¦ HV32 β€¦ HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
-  @(ex2_1_intro β€¦ (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *)
-| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_bind2 β€¦ HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
-  elim (lift_div_le β€¦ HT1 β€¦ HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
-  elim (IHT12 β€¦ HLK β€¦ HT1) -IHT12 HLK HT1 /3 width=5/
-| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX
-  elim (lift_inv_flat2 β€¦ HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
-  elim (IHT12 β€¦ HLK β€¦ HT01) -IHT12 HLK HT01 /3/
-]
-qed.
-*)
\ No newline at end of file
index ea6b8027bbbbf299a835db37c3f86b333a25c3df..f8a41f0250b9a1c90c436ebf424f228830226868 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/reduction/lpr_defs.ma".
+include "lambda-delta/reduction/lpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
index 53ad09398e059ada66500d5c2eb4013b2ae99989..b5743ddd138d824ce76d35bd869a19425987529f 100644 (file)
@@ -11,7 +11,7 @@
 
 include "lambda-delta/substitution/lift_weight.ma".
 include "lambda-delta/substitution/pts_pts.ma".
-include "lambda-delta/reduction/tpr_main.ma".
+include "lambda-delta/reduction/tpr_lift.ma".
 include "lambda-delta/reduction/tpr_pts.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
diff --git a/matita/matita/lib/lambda-delta/substitution/drop.ma b/matita/matita/lib/lambda-delta/substitution/drop.ma
new file mode 100644 (file)
index 0000000..d192c84
--- /dev/null
@@ -0,0 +1,147 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/leq.ma".
+include "lambda-delta/substitution/lift.ma".
+
+(* DROPPING *****************************************************************)
+
+inductive drop: lenv β†’ nat β†’ nat β†’ lenv β†’ Prop β‰
+| drop_sort: βˆ€d,e. drop (⋆) d e (⋆)
+| drop_comp: βˆ€L1,L2,I,V. drop L1 0 0 L2 β†’ drop (L1. π•“{I} V) 0 0 (L2. π•“{I} V)
+| drop_drop: βˆ€L1,L2,I,V,e. drop L1 0 e L2 β†’ drop (L1. π•“{I} V) 0 (e + 1) L2
+| drop_skip: βˆ€L1,L2,I,V1,V2,d,e.
+             drop L1 d e L2 β†’ β†‘[d,e] V2 β‰‘ V1 β†’
+             drop (L1. π•“{I} V1) (d + 1) e (L2. π•“{I} V2)
+.
+
+interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma drop_inv_refl_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ d = 0 β†’ e = 0 β†’ L1 = L2.
+#d #e #L1 #L2 #H elim H -H d e L1 L2
+[ //
+| #L1 #L2 #I #V #_ #IHL12 #H1 #H2
+  >(IHL12 H1 H2) -IHL12 H1 H2 L1 //
+| #L1 #L2 #I #V #e #_ #_ #_ #H
+  elim (plus_S_eq_O_false β€¦ H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H
+  elim (plus_S_eq_O_false β€¦ H)
+]
+qed.
+
+lemma drop_inv_refl: βˆ€L1,L2. β†“[0, 0] L1 β‰‘ L2 β†’ L1 = L2.
+/2 width=5/ qed.
+
+lemma drop_inv_sort1_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ L1 = β‹† β†’
+                          L2 = β‹†.
+#d #e #L1 #L2 * -d e L1 L2
+[ //
+| #L1 #L2 #I #V #_ #H destruct
+| #L1 #L2 #I #V #e #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma drop_inv_sort1: βˆ€d,e,L2. β†“[d, e] β‹† β‰‘ L2 β†’ L2 = β‹†.
+/2 width=5/ qed.
+
+lemma drop_inv_O1_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ d = 0 β†’
+                       βˆ€K,I,V. L1 = K. π•“{I} V β†’ 
+                       (e = 0 βˆ§ L2 = K. π•“{I} V) βˆ¨
+                       (0 < e βˆ§ β†“[d, e - 1] K β‰‘ L2).
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #K #I #V #H destruct
+| #L1 #L2 #I #V #HL12 #H #K #J #W #HX destruct -L1 I V
+  >(drop_inv_refl β€¦ HL12) -HL12 K /3/
+| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false β€¦ H)
+]
+qed.
+
+lemma drop_inv_O1: βˆ€e,K,I,V,L2. β†“[0, e] K. π•“{I} V β‰‘ L2 β†’
+                   (e = 0 βˆ§ L2 = K. π•“{I} V) βˆ¨
+                   (0 < e βˆ§ β†“[0, e - 1] K β‰‘ L2).
+/2/ qed.
+
+lemma drop_inv_drop1: βˆ€e,K,I,V,L2.
+                      β†“[0, e] K. π•“{I} V β‰‘ L2 β†’ 0 < e β†’ β†“[0, e - 1] K β‰‘ L2.
+#e #K #I #V #L2 #H #He
+elim (drop_inv_O1 β€¦ H) -H * // #H destruct -e;
+elim (lt_refl_false β€¦ He)
+qed.
+
+lemma drop_inv_skip2_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ 0 < d β†’
+                          βˆ€I,K2,V2. L2 = K2. π•“{I} V2 β†’
+                          βˆƒβˆƒK1,V1. β†“[d - 1, e] K1 β‰‘ K2 &
+                                   β†‘[d - 1, e] V2 β‰‘ V1 & 
+                                   L1 = K1. π•“{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #I #K #V #H destruct
+| #L1 #L2 #I #V #_ #H elim (lt_refl_false β€¦ H)
+| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false β€¦ H)
+| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z;
+  /2 width=5/
+]
+qed.
+
+lemma drop_inv_skip2: βˆ€d,e,I,L1,K2,V2. β†“[d, e] L1 β‰‘ K2. π•“{I} V2 β†’ 0 < d β†’
+                      βˆƒβˆƒK1,V1. β†“[d - 1, e] K1 β‰‘ K2 & β†‘[d - 1, e] V2 β‰‘ V1 &
+                               L1 = K1. π•“{I} V1.
+/2/ qed.
+
+(* Basic properties *********************************************************)
+
+lemma drop_refl: βˆ€L. β†“[0, 0] L β‰‘ L.
+#L elim L -L /2/
+qed.
+
+lemma drop_drop_lt: βˆ€L1,L2,I,V,e.
+                    β†“[0, e - 1] L1 β‰‘ L2 β†’ 0 < e β†’ β†“[0, e] L1. π•“{I} V β‰‘ L2.
+#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
+qed.
+
+lemma drop_fwd_drop2: βˆ€L1,I2,K2,V2,e. β†“[O, e] L1 β‰‘ K2. π•“{I2} V2 β†’
+                      β†“[O, e + 1] L1 β‰‘ K2.
+#L1 elim L1 -L1
+[ #I2 #K2 #V2 #e #H lapply (drop_inv_sort1 β€¦ H) -H #H destruct
+| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
+  elim (drop_inv_O1 β€¦ H) -H * #He #H
+  [ -IHL1; destruct -e K2 I2 V2 /2/
+  | @drop_drop >(plus_minus_m_m e 1) /2/
+  ]
+]
+qed.
+
+lemma drop_leq_drop1: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’
+                      βˆ€I,K1,V,i. β†“[0, i] L1 β‰‘ K1. π•“{I} V β†’
+                      d β‰€ i β†’ i < d + e β†’
+                      βˆƒβˆƒK2. K1 [0, d + e - i - 1] β‰ˆ K2 &
+                            β†“[0, i] L2 β‰‘ K2. π•“{I} V.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e
+[ #d #e #I #K1 #V #i #H
+  lapply (drop_inv_sort1 β€¦ H) -H #H destruct
+| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #I #K1 #V #i #_ #_ #H
+  elim (lt_zero_false β€¦ H)
+| #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie
+  elim (drop_inv_O1 β€¦ H) -H * #Hi #HLK1
+  [ -IHL12 Hie; destruct -i K1 J W;
+    <minus_n_O <minus_plus_m_m /2/
+  | -HL12;
+    elim (IHL12 β€¦ HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+  ]
+| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #I #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
+  lapply (plus_S_le_to_pos β€¦ Hdi) #Hi
+  lapply (drop_inv_drop1 β€¦ H ?) -H // #HLK1
+  elim (IHL12 β€¦ HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/
+]
+qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
deleted file mode 100644 (file)
index 51c6576..0000000
+++ /dev/null
@@ -1,137 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/leq_defs.ma".
-include "lambda-delta/substitution/lift_defs.ma".
-
-(* DROPPING *****************************************************************)
-
-inductive drop: lenv β†’ nat β†’ nat β†’ lenv β†’ Prop β‰
-| drop_refl: βˆ€L. drop L 0 0 L
-| drop_drop: βˆ€L1,L2,I,V,e. drop L1 0 e L2 β†’ drop (L1. π•“{I} V) 0 (e + 1) L2
-| drop_skip: βˆ€L1,L2,I,V1,V2,d,e.
-             drop L1 d e L2 β†’ β†‘[d,e] V2 β‰‘ V1 β†’
-             drop (L1. π•“{I} V1) (d + 1) e (L2. π•“{I} V2)
-.
-
-interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma drop_inv_refl_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ d = 0 β†’ e = 0 β†’ L1 = L2.
-#d #e #L1 #L2 * -d e L1 L2
-[ //
-| #L1 #L2 #I #V #e #_ #_ #H
-  elim (plus_S_eq_O_false β€¦ H)
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H
-  elim (plus_S_eq_O_false β€¦ H)
-]
-qed.
-
-lemma drop_inv_refl: βˆ€L1,L2. β†“[0, 0] L1 β‰‘ L2 β†’ L1 = L2.
-/2 width=5/ qed.
-
-lemma drop_inv_sort1_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ L1 = β‹† β†’
-                          βˆ§βˆ§ L2 = β‹† & d = 0 & e = 0.
-#d #e #L1 #L2 * -d e L1 L2
-[ /2/
-| #L1 #L2 #I #V #e #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
-qed.
-
-lemma drop_inv_sort1: βˆ€d,e,L2. β†“[d, e] β‹† β‰‘ L2 β†’
-                      βˆ§βˆ§ L2 = β‹† & d = 0 & e = 0.
-/2/ qed.
-
-lemma drop_inv_O1_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ d = 0 β†’
-                       βˆ€K,I,V. L1 = K. π•“{I} V β†’ 
-                       (e = 0 βˆ§ L2 = K. π•“{I} V) βˆ¨
-                       (0 < e βˆ§ β†“[d, e - 1] K β‰‘ L2).
-#d #e #L1 #L2 * -d e L1 L2
-[ /3/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false β€¦ H)
-]
-qed.
-
-lemma drop_inv_O1: βˆ€e,K,I,V,L2. β†“[0, e] K. π•“{I} V β‰‘ L2 β†’
-                   (e = 0 βˆ§ L2 = K. π•“{I} V) βˆ¨
-                   (0 < e βˆ§ β†“[0, e - 1] K β‰‘ L2).
-/2/ qed.
-
-lemma drop_inv_drop1: βˆ€e,K,I,V,L2.
-                      β†“[0, e] K. π•“{I} V β‰‘ L2 β†’ 0 < e β†’ β†“[0, e - 1] K β‰‘ L2.
-#e #K #I #V #L2 #H #He
-elim (drop_inv_O1 β€¦ H) -H * // #H destruct -e;
-elim (lt_refl_false β€¦ He)
-qed.
-
-lemma drop_inv_skip2_aux: βˆ€d,e,L1,L2. β†“[d, e] L1 β‰‘ L2 β†’ 0 < d β†’
-                          βˆ€I,K2,V2. L2 = K2. π•“{I} V2 β†’
-                          βˆƒβˆƒK1,V1. β†“[d - 1, e] K1 β‰‘ K2 &
-                                   β†‘[d - 1, e] V2 β‰‘ V1 & 
-                                   L1 = K1. π•“{I} V1.
-#d #e #L1 #L2 * -d e L1 L2
-[ #L #H elim (lt_refl_false β€¦ H)
-| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false β€¦ H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z;
-  /2 width=5/
-]
-qed.
-
-lemma drop_inv_skip2: βˆ€d,e,I,L1,K2,V2. β†“[d, e] L1 β‰‘ K2. π•“{I} V2 β†’ 0 < d β†’
-                      βˆƒβˆƒK1,V1. β†“[d - 1, e] K1 β‰‘ K2 & β†‘[d - 1, e] V2 β‰‘ V1 &
-                               L1 = K1. π•“{I} V1.
-/2/ qed.
-
-(* Basic properties *********************************************************)
-
-lemma drop_drop_lt: βˆ€L1,L2,I,V,e.
-                    β†“[0, e - 1] L1 β‰‘ L2 β†’ 0 < e β†’ β†“[0, e] L1. π•“{I} V β‰‘ L2.
-#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
-qed.
-
-lemma drop_fwd_drop2: βˆ€L1,I2,K2,V2,e. β†“[O, e] L1 β‰‘ K2. π•“{I2} V2 β†’
-                      β†“[O, e + 1] L1 β‰‘ K2.
-#L1 elim L1 -L1
-[ #I2 #K2 #V2 #e #H elim (drop_inv_sort1 β€¦ H) -H #H destruct
-| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
-  elim (drop_inv_O1 β€¦ H) -H * #He #H
-  [ -IHL1; destruct -e K2 I2 V2 /2/
-  | @drop_drop >(plus_minus_m_m e 1) /2/
-  ]
-]
-qed.
-
-lemma drop_leq_drop1: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’
-                      βˆ€I,K1,V,i. β†“[0, i] L1 β‰‘ K1. π•“{I} V β†’
-                      d β‰€ i β†’ i < d + e β†’
-                      βˆƒβˆƒK2. K1 [0, d + e - i - 1] β‰ˆ K2 &
-                            β†“[0, i] L2 β‰‘ K2. π•“{I} V.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
-[ #d #e #I #K1 #V #i #H
-  elim (drop_inv_sort1 β€¦ H) -H #H destruct
-| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #I #K1 #V #i #_ #_ #H
-  elim (lt_zero_false β€¦ H)
-| #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie
-  elim (drop_inv_O1 β€¦ H) -H * #Hi #HLK1
-  [ -IHL12 Hie; destruct -i K1 J W;
-    <minus_n_O <minus_plus_m_m /2/
-  | -HL12;
-    elim (IHL12 β€¦ HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
-  ]
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #I #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
-  lapply (plus_S_le_to_pos β€¦ Hdi) #Hi
-  lapply (drop_inv_drop1 β€¦ H ?) -H // #HLK1
-  elim (IHL12 β€¦ HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/
-]
-qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_drop.ma b/matita/matita/lib/lambda-delta/substitution/drop_drop.ma
new file mode 100644 (file)
index 0000000..96fd0db
--- /dev/null
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "lambda-delta/substitution/drop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Main properties **********************************************************)
+
+lemma drop_conf_ge: βˆ€d1,e1,L,L1. β†“[d1, e1] L β‰‘ L1 β†’
+                    βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ d1 + e1 β‰€ e2 β†’
+                    β†“[0, e2 - e1] L1 β‰‘ L2.
+#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
+[ #d #e #e2 #L2 #H
+  >(drop_inv_sort1 β€¦ H) -H L2 //
+| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ <minus_n_O
+   <(drop_inv_refl β€¦ HK12) -HK12 K2 //
+| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
+  lapply (drop_inv_drop1 β€¦ H ?) -H /2/ #HL2
+  <minus_plus_comm /3/
+| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
+  lapply (transitive_le 1 β€¦ Hdee2) // #He2
+  lapply (drop_inv_drop1 β€¦ H ?) -H // -He2 #HL2
+  lapply (transitive_le (1+e) β€¦ Hdee2) // #Hee2
+  @drop_drop_lt >minus_minus_comm /3/ (**) (* explicit constructor *)
+]
+qed.
+
+lemma drop_conf_lt: βˆ€d1,e1,L,L1. β†“[d1, e1] L β‰‘ L1 β†’
+                    βˆ€e2,K2,I,V2. β†“[0, e2] L β‰‘ K2. π•“{I} V2 β†’
+                    e2 < d1 β†’ let d β‰ d1 - e2 - 1 in
+                    βˆƒβˆƒK1,V1. β†“[0, e2] L1 β‰‘ K1. π•“{I} V1 &
+                             β†“[d, e1] K2 β‰‘ K1 & β†‘[d, e1] V1 β‰‘ V2.
+#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
+[ #d #e #e2 #K2 #I #V2 #H
+  lapply (drop_inv_sort1 β€¦ H) -H #H destruct
+| #L1 #L2 #I #V #_ #_ #e2 #K2 #J #V2 #_ #H
+  elim (lt_zero_false β€¦ H)
+| #L1 #L2 #I #V #e #_ #_ #e2 #K2 #J #V2 #_ #H
+  elim (lt_zero_false β€¦ H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d
+  elim (drop_inv_O1 β€¦ H) -H *
+  [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/
+  | -HL12 -HV12 #He #HLK
+    elim (IHL12 β€¦ HLK ?) -IHL12 HLK [ <minus_minus /3 width=5/ | /2/ ] (**) (* a bit slow *)
+  ]
+]
+qed.
+
+lemma drop_trans_le: βˆ€d1,e1,L1,L. β†“[d1, e1] L1 β‰‘ L β†’
+                     βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ e2 β‰€ d1 β†’
+                     βˆƒβˆƒL0. β†“[0, e2] L1 β‰‘ L0 & β†“[d1 - e2, e1] L0 β‰‘ L2.
+#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
+[ #d #e #e2 #L2 #H
+  >(drop_inv_sort1 β€¦ H) -H L2 /2/
+| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #HL2 #H
+  >(drop_inv_refl β€¦ HK12) -HK12 K1;
+  lapply (le_O_to_eq_O β€¦ H) -H #H destruct -e2 /2/
+| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
+  lapply (le_O_to_eq_O β€¦ H) -H #H destruct -e2;
+  elim (IHL12 β€¦ HL2 ?) -IHL12 HL2 // #L0 #H #HL0
+  lapply (drop_inv_refl β€¦ H) -H #H destruct -L1 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+  elim (drop_inv_O1 β€¦ H) -H *
+  [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/
+  | -HL12 HV12 #He2 #HL2
+    elim (IHL12 β€¦ HL2 ?) -IHL12 HL2 L2
+    [ <minus_le_minus_minus_comm /3/ | /2/ ]
+  ]
+]
+qed.
+
+lemma drop_trans_ge: βˆ€d1,e1,L1,L. β†“[d1, e1] L1 β‰‘ L β†’
+                     βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ d1 β‰€ e2 β†’ β†“[0, e1 + e2] L1 β‰‘ L2.
+#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
+[ #d #e #e2 #L2 #H
+  >(drop_inv_sort1 β€¦ H) -H L2 //
+| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ normalize
+  >(drop_inv_refl β€¦ HK12) -HK12 K1 //
+| /3/
+| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
+  lapply (lt_to_le_to_lt 0 β€¦ Hde2) // #He2
+  lapply (lt_to_le_to_lt β€¦ (e + e2) He2 ?) // #Hee2
+  lapply (drop_inv_drop1 β€¦ H ?) -H // #HL2
+  @drop_drop_lt // >le_plus_minus // @IHL12 /2/ (**) (* explicit constructor *)
+]
+qed.
+
+lemma drop_trans_ge_comm: βˆ€d1,e1,e2,L1,L2,L.
+                          β†“[d1, e1] L1 β‰‘ L β†’ β†“[0, e2] L β‰‘ L2 β†’ d1 β‰€ e2 β†’
+                          β†“[0, e2 + e1] L1 β‰‘ L2.
+#e1 #e1 #e2 >commutative_plus /2 width=5/
+qed.
+
+axiom drop_div: βˆ€e1,L1,L. β†“[0, e1] L1 β‰‘ L β†’ βˆ€e2,L2. β†“[0, e2] L2 β‰‘ L β†’
+                βˆƒβˆƒL0. β†“[0, e1] L0 β‰‘ L2 & β†“[e1, e2] L0 β‰‘ L1.
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
deleted file mode 100644 (file)
index 575f254..0000000
+++ /dev/null
@@ -1,96 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "lambda-delta/substitution/drop_defs.ma".
-
-(* DROPPING *****************************************************************)
-
-(* Main properties **********************************************************)
-
-lemma drop_conf_ge: βˆ€d1,e1,L,L1. β†“[d1, e1] L β‰‘ L1 β†’
-                    βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ d1 + e1 β‰€ e2 β†’
-                    β†“[0, e2 - e1] L1 β‰‘ L2.
-#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
-[ //
-| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
-  lapply (drop_inv_drop1 β€¦ H ?) -H /2/ #HL2
-  <minus_plus_comm /3/
-| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
-  lapply (transitive_le 1 β€¦ Hdee2) // #He2
-  lapply (drop_inv_drop1 β€¦ H ?) -H // -He2 #HL2
-  lapply (transitive_le (1+e) β€¦ Hdee2) // #Hee2
-  @drop_drop_lt >minus_minus_comm /3/ (**) (* explicit constructor *)
-]
-qed.
-
-lemma drop_conf_lt: βˆ€d1,e1,L,L1. β†“[d1, e1] L β‰‘ L1 β†’
-                    βˆ€e2,K2,I,V2. β†“[0, e2] L β‰‘ K2. π•“{I} V2 β†’
-                    e2 < d1 β†’ let d β‰ d1 - e2 - 1 in
-                    βˆƒβˆƒK1,V1. β†“[0, e2] L1 β‰‘ K1. π•“{I} V1 &
-                             β†“[d, e1] K2 β‰‘ K1 & β†‘[d, e1] V1 β‰‘ V2.
-#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
-[ #L0 #e2 #K2 #I #V2 #_ #H
-  elim (lt_zero_false β€¦ H)
-| #L1 #L2 #I #V #e #_ #_ #e2 #K2 #J #V2 #_ #H
-  elim (lt_zero_false β€¦ H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d
-  elim (drop_inv_O1 β€¦ H) -H *
-  [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/
-  | -HL12 -HV12 #He #HLK
-    elim (IHL12 β€¦ HLK ?) -IHL12 HLK [ <minus_minus /3 width=5/ | /2/ ] (**) (* a bit slow *)
-  ]
-]
-qed.
-
-lemma drop_trans_le: βˆ€d1,e1,L1,L. β†“[d1, e1] L1 β‰‘ L β†’
-                     βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ e2 β‰€ d1 β†’
-                     βˆƒβˆƒL0. β†“[0, e2] L1 β‰‘ L0 & β†“[d1 - e2, e1] L0 β‰‘ L2.
-#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
-[ #L #e2 #L2 #HL2 #H
-  lapply (le_O_to_eq_O β€¦ H) -H #H destruct -e2 /2/
-| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
-  lapply (le_O_to_eq_O β€¦ H) -H #H destruct -e2;
-  elim (IHL12 β€¦ HL2 ?) -IHL12 HL2 // #L0 #H #HL0
-  lapply (drop_inv_refl β€¦ H) -H #H destruct -L1 /3 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
-  elim (drop_inv_O1 β€¦ H) -H *
-  [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/
-  | -HL12 HV12 #He2 #HL2
-    elim (IHL12 β€¦ HL2 ?) -IHL12 HL2 L2
-    [ <minus_le_minus_minus_comm /3/ | /2/ ]
-  ]
-]
-qed.
-
-lemma drop_trans_ge: βˆ€d1,e1,L1,L. β†“[d1, e1] L1 β‰‘ L β†’
-                     βˆ€e2,L2. β†“[0, e2] L β‰‘ L2 β†’ d1 β‰€ e2 β†’ β†“[0, e1 + e2] L1 β‰‘ L2.
-#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
-[ //
-| /3/
-| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
-  lapply (lt_to_le_to_lt 0 β€¦ Hde2) // #He2
-  lapply (lt_to_le_to_lt β€¦ (e + e2) He2 ?) // #Hee2
-  lapply (drop_inv_drop1 β€¦ H ?) -H // #HL2
-  @drop_drop_lt // >le_plus_minus // @IHL12 /2/ (**) (* explicit constructor *)
-]
-qed.
-
-lemma drop_trans_ge_comm: βˆ€d1,e1,e2,L1,L2,L.
-                          β†“[d1, e1] L1 β‰‘ L β†’ β†“[0, e2] L β‰‘ L2 β†’ d1 β‰€ e2 β†’
-                          β†“[0, e2 + e1] L1 β‰‘ L2.
-#e1 #e1 #e2 >commutative_plus /2 width=5/
-qed.
-
-axiom drop_div: βˆ€e1,L1,L. β†“[0, e1] L1 β‰‘ L β†’ βˆ€e2,L2. β†“[0, e2] L2 β‰‘ L β†’
-                βˆƒβˆƒL0. β†“[0, e1] L0 β‰‘ L2 & β†“[e1, e2] L0 β‰‘ L1.
diff --git a/matita/matita/lib/lambda-delta/substitution/leq.ma b/matita/matita/lib/lambda-delta/substitution/leq.ma
new file mode 100644 (file)
index 0000000..3c79815
--- /dev/null
@@ -0,0 +1,60 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/lenv.ma".
+
+(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+
+inductive leq: lenv β†’ nat β†’ nat β†’ lenv β†’ Prop β‰
+| leq_sort: βˆ€d,e. leq (⋆) d e (⋆)
+| leq_comp: βˆ€L1,L2,I1,I2,V1,V2.
+            leq L1 0 0 L2 β†’ leq (L1. π•“{I1} V1) 0 0 (L2. π•“{I2} V2)
+| leq_eq:   βˆ€L1,L2,I,V,e. leq L1 0 e L2 β†’ leq (L1. π•“{I} V) 0 (e + 1) (L2.𝕓{I} V)
+| leq_skip: βˆ€L1,L2,I1,I2,V1,V2,d,e.
+            leq L1 d e L2 β†’ leq (L1. π•“{I1} V1) (d + 1) e (L2. π•“{I2} V2)
+.
+
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
+
+(* Basic properties *********************************************************)
+
+lemma leq_refl: βˆ€d,e,L. L [d, e] β‰ˆ L.
+#d elim d -d
+[ #e elim e -e [ #L elim L -L /2/ | #e #IHe #L elim L -L /2/ ]
+| #d #IHd #e #L elim L -L /2/
+]
+qed.
+
+lemma leq_sym: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’ L2 [d, e] β‰ˆ L1.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
+qed.
+
+lemma leq_skip_lt: βˆ€L1,L2,d,e. leq L1 (d - 1) e L2 β†’ 0 < d β†’
+                   βˆ€I1,I2,V1,V2. L1. π•“{I1} V1 [d, e] β‰ˆ L2. π•“{I2} V2.
+
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ 
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma leq_inv_sort1_aux: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’ L1 = β‹† β†’ L2 = β‹†.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e
+[ //
+| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct
+| #L1 #L2 #I #V #e #_ #_ #H destruct
+| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct
+qed.
+
+lemma leq_inv_sort1: βˆ€L2,d,e. β‹† [d, e] β‰ˆ L2 β†’ L2 = β‹†.
+/2 width=5/ qed.
+
+lemma leq_inv_sort2: βˆ€L1,d,e. L1 [d, e] β‰ˆ β‹† β†’ L1 = β‹†.
+/3/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/leq_defs.ma b/matita/matita/lib/lambda-delta/substitution/leq_defs.ma
deleted file mode 100644 (file)
index 3c79815..0000000
+++ /dev/null
@@ -1,60 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/syntax/lenv.ma".
-
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-
-inductive leq: lenv β†’ nat β†’ nat β†’ lenv β†’ Prop β‰
-| leq_sort: βˆ€d,e. leq (⋆) d e (⋆)
-| leq_comp: βˆ€L1,L2,I1,I2,V1,V2.
-            leq L1 0 0 L2 β†’ leq (L1. π•“{I1} V1) 0 0 (L2. π•“{I2} V2)
-| leq_eq:   βˆ€L1,L2,I,V,e. leq L1 0 e L2 β†’ leq (L1. π•“{I} V) 0 (e + 1) (L2.𝕓{I} V)
-| leq_skip: βˆ€L1,L2,I1,I2,V1,V2,d,e.
-            leq L1 d e L2 β†’ leq (L1. π•“{I1} V1) (d + 1) e (L2. π•“{I2} V2)
-.
-
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
-
-(* Basic properties *********************************************************)
-
-lemma leq_refl: βˆ€d,e,L. L [d, e] β‰ˆ L.
-#d elim d -d
-[ #e elim e -e [ #L elim L -L /2/ | #e #IHe #L elim L -L /2/ ]
-| #d #IHd #e #L elim L -L /2/
-]
-qed.
-
-lemma leq_sym: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’ L2 [d, e] β‰ˆ L1.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
-qed.
-
-lemma leq_skip_lt: βˆ€L1,L2,d,e. leq L1 (d - 1) e L2 β†’ 0 < d β†’
-                   βˆ€I1,I2,V1,V2. L1. π•“{I1} V1 [d, e] β‰ˆ L2. π•“{I2} V2.
-
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ 
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma leq_inv_sort1_aux: βˆ€L1,L2,d,e. L1 [d, e] β‰ˆ L2 β†’ L1 = β‹† β†’ L2 = β‹†.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
-[ //
-| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct
-| #L1 #L2 #I #V #e #_ #_ #H destruct
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct
-qed.
-
-lemma leq_inv_sort1: βˆ€L2,d,e. β‹† [d, e] β‰ˆ L2 β†’ L2 = β‹†.
-/2 width=5/ qed.
-
-lemma leq_inv_sort2: βˆ€L1,d,e. L1 [d, e] β‰ˆ β‹† β†’ L1 = β‹†.
-/3/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma
new file mode 100644 (file)
index 0000000..a5b15e1
--- /dev/null
@@ -0,0 +1,230 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/term.ma".
+
+(* RELOCATION ***************************************************************)
+
+inductive lift: term β†’ nat β†’ nat β†’ term β†’ Prop β‰
+| lift_sort   : βˆ€k,d,e. lift (⋆k) d e (⋆k)
+| lift_lref_lt: βˆ€i,d,e. i < d β†’ lift (#i) d e (#i)
+| lift_lref_ge: βˆ€i,d,e. d β‰€ i β†’ lift (#i) d e (#(i + e))
+| lift_bind   : βˆ€I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 β†’ lift T1 (d + 1) e T2 β†’
+                lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| lift_flat   : βˆ€I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 β†’ lift T1 d e T2 β†’
+                lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
+
+(* Basic properties *********************************************************)
+
+lemma lift_lref_ge_minus: βˆ€d,e,i. d + e β‰€ i β†’ β†‘[d, e] #(i - e) β‰‘ #i.
+#d #e #i #H >(plus_minus_m_m i e) in βŠ’ (? ? ? ? %) /3/
+qed.
+
+lemma lift_refl: βˆ€T,d. β†‘[d, 0] T β‰‘ T.
+#T elim T -T
+[ //
+| #i #d elim (lt_or_ge i d) /2/
+| #I elim I -I /2/
+]
+qed.
+
+lemma lift_total: βˆ€T1,d,e. βˆƒT2. β†‘[d,e] T1 β‰‘ T2.
+#T1 elim T1 -T1
+[ /2/
+| #i #d #e elim (lt_or_ge i d) /3/
+| * #I #V1 #T1 #IHV1 #IHT1 #d #e
+  elim (IHV1 d e) -IHV1 #V2 #HV12
+  [ elim (IHT1 (d+1) e) -IHT1 /3/
+  | elim (IHT1 d e) -IHT1 /3/
+  ]
+]
+qed.
+
+lemma lift_split: βˆ€d1,e2,T1,T2. β†‘[d1, e2] T1 β‰‘ T2 β†’ βˆ€d2,e1.
+                                d1 β‰€ d2 β†’ d2 β‰€ d1 + e1 β†’ e1 β‰€ e2 β†’
+                                βˆƒβˆƒT. β†‘[d1, e1] T1 β‰‘ T & β†‘[d2, e2 - e1] T β‰‘ T2.
+#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
+[ /3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
+  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2 /4/
+| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
+  lapply (transitive_le β€¦(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
+  <(arith_d1 i e2 e1) // /3/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV β€¦ Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT (d2+1) β€¦ ? ? He12) /3 width = 5/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV β€¦ Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT d2 β€¦ ? ? He12) /3 width = 5/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lift_inv_refl_aux: βˆ€d,e,T1,T2. β†‘[d, e] T1 β‰‘ T2 β†’ e = 0 β†’ T1 = T2.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/
+qed.
+
+lemma lift_inv_refl: βˆ€d,T1,T2. β†‘[d, 0] T1 β‰‘ T2 β†’ T1 = T2.
+/2/ qed.
+
+lemma lift_inv_sort1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€k. T1 = β‹†k β†’ T2 = β‹†k.
+#d #e #T1 #T2 * -d e T1 T2 //
+[ #i #d #e #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+]
+qed.
+
+lemma lift_inv_sort1: βˆ€d,e,T2,k. β†‘[d,e] β‹†k β‰‘ T2 β†’ T2 = β‹†k.
+/2 width=5/ qed.
+
+lemma lift_inv_lref1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€i. T1 = #i β†’
+                          (i < d βˆ§ T2 = #i) βˆ¨ (d β‰€ i βˆ§ T2 = #(i + e)).
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #i #H destruct
+| #j #d #e #Hj #i #Hi destruct /3/
+| #j #d #e #Hj #i #Hi destruct /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+]
+qed.
+
+lemma lift_inv_lref1: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’
+                      (i < d βˆ§ T2 = #i) βˆ¨ (d β‰€ i βˆ§ T2 = #(i + e)).
+/2/ qed.
+
+lemma lift_inv_lref1_lt: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’ i < d β†’ T2 = #i.
+#d #e #T2 #i #H elim (lift_inv_lref1 β€¦ H) -H * //
+#Hdi #_ #Hid lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
+elim (lt_refl_false β€¦ Hdd)
+qed.
+
+lemma lift_inv_lref1_ge: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’ d β‰€ i β†’ T2 = #(i + e).
+#d #e #T2 #i #H elim (lift_inv_lref1 β€¦ H) -H * //
+#Hid #_ #Hdi lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
+elim (lt_refl_false β€¦ Hdd)
+qed.
+
+lemma lift_inv_bind1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
+                          βˆ€I,V1,U1. T1 = π•“{I} V1.U1 β†’
+                          βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
+                                   T2 = π•“{I} V2. U2.
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
+]
+qed.
+
+lemma lift_inv_bind1: βˆ€d,e,T2,I,V1,U1. β†‘[d,e] π•“{I} V1. U1 β‰‘ T2 β†’
+                      βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
+                               T2 = π•“{I} V2. U2.
+/2/ qed.
+
+lemma lift_inv_flat1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
+                          βˆ€I,V1,U1. T1 = π•—{I} V1.U1 β†’
+                          βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
+                                   T2 = π•—{I} V2. U2.
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
+]
+qed.
+
+lemma lift_inv_flat1: βˆ€d,e,T2,I,V1,U1. β†‘[d,e] π•—{I} V1. U1 β‰‘ T2 β†’
+                      βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
+                               T2 = π•—{I} V2. U2.
+/2/ qed.
+
+lemma lift_inv_sort2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€k. T2 = β‹†k β†’ T1 = β‹†k.
+#d #e #T1 #T2 * -d e T1 T2 //
+[ #i #d #e #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+]
+qed.
+
+lemma lift_inv_sort2: βˆ€d,e,T1,k. β†‘[d,e] T1 β‰‘ β‹†k β†’ T1 = β‹†k.
+/2 width=5/ qed.
+
+lemma lift_inv_lref2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€i. T2 = #i β†’
+                          (i < d βˆ§ T1 = #i) βˆ¨ (d + e β‰€ i βˆ§ T1 = #(i - e)).
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #i #H destruct
+| #j #d #e #Hj #i #Hi destruct /3/
+| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+]
+qed.
+
+lemma lift_inv_lref2: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’
+                      (i < d βˆ§ T1 = #i) βˆ¨ (d + e β‰€ i βˆ§ T1 = #(i - e)).
+/2/ qed.
+
+lemma lift_inv_lref2_lt: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’ i < d β†’ T1 = #i.
+#d #e #T1 #i #H elim (lift_inv_lref2 β€¦ H) -H * //
+#Hdi #_ #Hid lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
+elim (plus_lt_false β€¦ Hdd)
+qed.
+
+lemma lift_inv_lref2_ge: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’ d + e β‰€ i β†’ T1 = #(i - e).
+#d #e #T1 #i #H elim (lift_inv_lref2 β€¦ H) -H * //
+#Hid #_ #Hdi lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
+elim (plus_lt_false β€¦ Hdd)
+qed.
+
+lemma lift_inv_bind2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
+                          βˆ€I,V2,U2. T2 = π•“{I} V2.U2 β†’
+                          βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
+                                   T1 = π•“{I} V1. U1.
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
+]
+qed.
+
+lemma lift_inv_bind2: βˆ€d,e,T1,I,V2,U2. β†‘[d,e] T1 β‰‘  π•“{I} V2. U2 β†’
+                      βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
+                               T1 = π•“{I} V1. U1.
+/2/ qed.
+
+lemma lift_inv_flat2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
+                          βˆ€I,V2,U2. T2 = π•—{I} V2.U2 β†’
+                          βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
+                                   T1 = π•—{I} V1. U1.
+#d #e #T1 #T2 * -d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width = 5/
+]
+qed.
+
+lemma lift_inv_flat2: βˆ€d,e,T1,I,V2,U2. β†‘[d,e] T1 β‰‘  π•—{I} V2. U2 β†’
+                      βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
+                               T1 = π•—{I} V1. U1.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
deleted file mode 100644 (file)
index 71d438d..0000000
+++ /dev/null
@@ -1,211 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/syntax/term.ma".
-
-(* RELOCATION ***************************************************************)
-
-inductive lift: term β†’ nat β†’ nat β†’ term β†’ Prop β‰
-| lift_sort   : βˆ€k,d,e. lift (⋆k) d e (⋆k)
-| lift_lref_lt: βˆ€i,d,e. i < d β†’ lift (#i) d e (#i)
-| lift_lref_ge: βˆ€i,d,e. d β‰€ i β†’ lift (#i) d e (#(i + e))
-| lift_bind   : βˆ€I,V1,V2,T1,T2,d,e.
-                lift V1 d e V2 β†’ lift T1 (d + 1) e T2 β†’
-                lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| lift_flat   : βˆ€I,V1,V2,T1,T2,d,e.
-                lift V1 d e V2 β†’ lift T1 d e T2 β†’
-                lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
-
-(* Basic properties *********************************************************)
-
-lemma lift_lref_ge_minus: βˆ€d,e,i. d + e β‰€ i β†’ β†‘[d, e] #(i - e) β‰‘ #i.
-#d #e #i #H >(plus_minus_m_m i e) in βŠ’ (? ? ? ? %) /3/
-qed.
-
-lemma lift_refl: βˆ€T,d. β†‘[d, 0] T β‰‘ T.
-#T elim T -T
-[ //
-| #i #d elim (lt_or_ge i d) /2/
-| #I elim I -I /2/
-]
-qed.
-
-lemma lift_total: βˆ€T1,d,e. βˆƒT2. β†‘[d,e] T1 β‰‘ T2.
-#T1 elim T1 -T1
-[ /2/
-| #i #d #e elim (lt_or_ge i d) /3/
-| * #I #V1 #T1 #IHV1 #IHT1 #d #e
-  elim (IHV1 d e) -IHV1 #V2 #HV12
-  [ elim (IHT1 (d+1) e) -IHT1 /3/
-  | elim (IHT1 d e) -IHT1 /3/
-  ]
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lift_inv_refl_aux: βˆ€d,e,T1,T2. β†‘[d, e] T1 β‰‘ T2 β†’ e = 0 β†’ T1 = T2.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/
-qed.
-
-lemma lift_inv_refl: βˆ€d,T1,T2. β†‘[d, 0] T1 β‰‘ T2 β†’ T1 = T2.
-/2/ qed.
-
-lemma lift_inv_sort1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€k. T1 = β‹†k β†’ T2 = β‹†k.
-#d #e #T1 #T2 * -d e T1 T2 //
-[ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
-]
-qed.
-
-lemma lift_inv_sort1: βˆ€d,e,T2,k. β†‘[d,e] β‹†k β‰‘ T2 β†’ T2 = β‹†k.
-/2 width=5/ qed.
-
-lemma lift_inv_lref1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€i. T1 = #i β†’
-                          (i < d βˆ§ T2 = #i) βˆ¨ (d β‰€ i βˆ§ T2 = #(i + e)).
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3/
-| #j #d #e #Hj #i #Hi destruct /3/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
-]
-qed.
-
-lemma lift_inv_lref1: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’
-                      (i < d βˆ§ T2 = #i) βˆ¨ (d β‰€ i βˆ§ T2 = #(i + e)).
-/2/ qed.
-
-lemma lift_inv_lref1_lt: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’ i < d β†’ T2 = #i.
-#d #e #T2 #i #H elim (lift_inv_lref1 β€¦ H) -H * //
-#Hdi #_ #Hid lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
-elim (lt_refl_false β€¦ Hdd)
-qed.
-
-lemma lift_inv_lref1_ge: βˆ€d,e,T2,i. β†‘[d,e] #i β‰‘ T2 β†’ d β‰€ i β†’ T2 = #(i + e).
-#d #e #T2 #i #H elim (lift_inv_lref1 β€¦ H) -H * //
-#Hid #_ #Hdi lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
-elim (lt_refl_false β€¦ Hdd)
-qed.
-
-lemma lift_inv_bind1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
-                          βˆ€I,V1,U1. T1 = π•“{I} V1.U1 β†’
-                          βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
-                                   T2 = π•“{I} V2. U2.
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
-]
-qed.
-
-lemma lift_inv_bind1: βˆ€d,e,T2,I,V1,U1. β†‘[d,e] π•“{I} V1. U1 β‰‘ T2 β†’
-                      βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
-                               T2 = π•“{I} V2. U2.
-/2/ qed.
-
-lemma lift_inv_flat1_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
-                          βˆ€I,V1,U1. T1 = π•—{I} V1.U1 β†’
-                          βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
-                                   T2 = π•—{I} V2. U2.
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
-]
-qed.
-
-lemma lift_inv_flat1: βˆ€d,e,T2,I,V1,U1. β†‘[d,e] π•—{I} V1. U1 β‰‘ T2 β†’
-                      βˆƒβˆƒV2,U2. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
-                               T2 = π•—{I} V2. U2.
-/2/ qed.
-
-lemma lift_inv_sort2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€k. T2 = β‹†k β†’ T1 = β‹†k.
-#d #e #T1 #T2 * -d e T1 T2 //
-[ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
-]
-qed.
-
-lemma lift_inv_sort2: βˆ€d,e,T1,k. β†‘[d,e] T1 β‰‘ β‹†k β†’ T1 = β‹†k.
-/2 width=5/ qed.
-
-lemma lift_inv_lref2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’ βˆ€i. T2 = #i β†’
-                          (i < d βˆ§ T1 = #i) βˆ¨ (d + e β‰€ i βˆ§ T1 = #(i - e)).
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3/
-| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
-]
-qed.
-
-lemma lift_inv_lref2: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’
-                      (i < d βˆ§ T1 = #i) βˆ¨ (d + e β‰€ i βˆ§ T1 = #(i - e)).
-/2/ qed.
-
-lemma lift_inv_lref2_lt: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’ i < d β†’ T1 = #i.
-#d #e #T1 #i #H elim (lift_inv_lref2 β€¦ H) -H * //
-#Hdi #_ #Hid lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
-elim (plus_lt_false β€¦ Hdd)
-qed.
-
-lemma lift_inv_lref2_ge: βˆ€d,e,T1,i. β†‘[d,e] T1 β‰‘ #i β†’ d + e β‰€ i β†’ T1 = #(i - e).
-#d #e #T1 #i #H elim (lift_inv_lref2 β€¦ H) -H * //
-#Hid #_ #Hdi lapply (le_to_lt_to_lt β€¦ Hdi Hid) -Hdi Hid #Hdd
-elim (plus_lt_false β€¦ Hdd)
-qed.
-
-lemma lift_inv_bind2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
-                          βˆ€I,V2,U2. T2 = π•“{I} V2.U2 β†’
-                          βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
-                                   T1 = π•“{I} V1. U1.
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
-]
-qed.
-
-lemma lift_inv_bind2: βˆ€d,e,T1,I,V2,U2. β†‘[d,e] T1 β‰‘  π•“{I} V2. U2 β†’
-                      βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d+1,e] U1 β‰‘ U2 &
-                               T1 = π•“{I} V1. U1.
-/2/ qed.
-
-lemma lift_inv_flat2_aux: βˆ€d,e,T1,T2. β†‘[d,e] T1 β‰‘ T2 β†’
-                          βˆ€I,V2,U2. T2 = π•—{I} V2.U2 β†’
-                          βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
-                                   T1 = π•—{I} V1. U1.
-#d #e #T1 #T2 * -d e T1 T2
-[ #k #d #e #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width = 5/
-]
-qed.
-
-lemma lift_inv_flat2: βˆ€d,e,T1,I,V2,U2. β†‘[d,e] T1 β‰‘  π•—{I} V2. U2 β†’
-                      βˆƒβˆƒV1,U1. β†‘[d,e] V1 β‰‘ V2 & β†‘[d,e] U1 β‰‘ U2 &
-                               T1 = π•—{I} V1. U1.
-/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_lift.ma b/matita/matita/lib/lambda-delta/substitution/lift_lift.ma
new file mode 100644 (file)
index 0000000..4281046
--- /dev/null
@@ -0,0 +1,154 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "lambda-delta/substitution/lift.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* Main properies ***********************************************************)
+
+lemma lift_inj:  βˆ€d,e,T1,U. β†‘[d,e] T1 β‰‘ U β†’ βˆ€T2. β†‘[d,e] T2 β‰‘ U β†’ T1 = T2.
+#d #e #T1 #U #H elim H -H d e T1 U
+[ #k #d #e #X #HX
+  lapply (lift_inv_sort2 β€¦ HX) -HX //
+| #i #d #e #Hid #X #HX 
+  lapply (lift_inv_lref2_lt β€¦ HX ?) -HX //
+| #i #d #e #Hdi #X #HX 
+  lapply (lift_inv_lref2_ge β€¦ HX ?) -HX /2/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_bind2 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_flat2 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+]
+qed.
+
+lemma lift_div_le: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
+                   βˆ€d2,e2,T2. β†‘[d2 + e1, e2] T2 β‰‘ T β†’
+                   d1 β‰€ d2 β†’
+                   βˆƒβˆƒT0. β†‘[d1, e1] T0 β‰‘ T2 & β†‘[d2, e2] T0 β‰‘ T1.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
+  lapply (lift_inv_sort2 β€¦ Hk) -Hk #Hk destruct -T2 /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2
+  lapply (lift_inv_lref2_lt β€¦ Hi ?) -Hi /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  elim (lift_inv_lref2 β€¦ Hi) -Hi * #Hid2 #H destruct -T2
+  [ -Hd12; lapply (lt_plus_to_lt_l β€¦ Hid2) -Hid2 #Hid2 /3/
+  | -Hid1; lapply (arith1 β€¦ Hid2) -Hid2 #Hid2
+    @(ex2_1_intro β€¦ #(i - e2))
+    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le β€¦ Hd12) -Hd12 /2/ | -Hd12 /2/ ]
+    | -Hd12 >(plus_minus_m_m i e2) in βŠ’ (? ? ? ? %) /3/
+    ]
+  ]
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_bind2 β€¦ H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW β€¦ HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  >plus_plus_comm_23 in HU2 #HU2 elim (IHU β€¦ HU2 ?) /3 width = 5/
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_flat2 β€¦ H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW β€¦ HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  elim (IHU β€¦ HU2 ?) /3 width = 5/
+]
+qed.
+
+lemma lift_mono:  βˆ€d,e,T,U1. β†‘[d,e] T β‰‘ U1 β†’ βˆ€U2. β†‘[d,e] T β‰‘ U2 β†’ U1 = U2.
+#d #e #T #U1 #H elim H -H d e T U1
+[ #k #d #e #X #HX
+  lapply (lift_inv_sort1 β€¦ HX) -HX //
+| #i #d #e #Hid #X #HX 
+  lapply (lift_inv_lref1_lt β€¦ HX ?) -HX //
+| #i #d #e #Hdi #X #HX 
+  lapply (lift_inv_lref1_ge β€¦ HX ?) -HX //
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_bind1 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_flat1 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+]
+qed.
+
+lemma lift_trans_be: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
+                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’
+                     d1 β‰€ d2 β†’ d2 β‰€ d1 + e1 β†’ β†‘[d1, e1 + e2] T1 β‰‘ T2.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
+  >(lift_inv_sort1 β€¦ HT2) -HT2 //
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_
+  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2
+  lapply (lift_inv_lref1_lt β€¦ HT2 Hid2) /2/
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21
+  lapply (lift_inv_lref1_ge β€¦ HT2 ?) -HT2
+  [ @(transitive_le β€¦ Hd21 ?) -Hd21 /2/
+  | -Hd21 /2/
+  ]
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
+  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  lapply (IHV12 β€¦ HV20 ? ?) // -IHV12 HV20 #HV10
+  lapply (IHT12 β€¦ HT20 ? ?) /2/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
+  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  lapply (IHV12 β€¦ HV20 ? ?) // -IHV12 HV20 #HV10
+  lapply (IHT12 β€¦ HT20 ? ?) /2/
+]
+qed.
+
+lemma lift_trans_le: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
+                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’ d2 β‰€ d1 β†’
+                     βˆƒβˆƒT0. β†‘[d2, e2] T1 β‰‘ T0 & β†‘[d1 + e2, e1] T0 β‰‘ T2.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #X #HX #_
+  >(lift_inv_sort1 β€¦ HX) -HX /2/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
+  lapply (lt_to_le_to_lt β€¦ (d1+e2) Hid1 ?) // #Hie2
+  elim (lift_inv_lref1 β€¦ HX) -HX * #Hid2 #HX destruct -X /4/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
+  lapply (transitive_le β€¦ Hd21 Hid1) -Hd21 #Hid2
+  lapply (lift_inv_lref1_ge β€¦ HX ?) -HX /2/ #HX destruct -X;
+  >plus_plus_comm_23 /4/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21
+  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
+  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21
+  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
+  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
+]
+qed.
+
+lemma lift_trans_ge: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
+                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’ d1 + e1 β‰€ d2 β†’
+                     βˆƒβˆƒT0. β†‘[d2 - e1, e2] T1 β‰‘ T0 & β†‘[d1, e1] T0 β‰‘ T2.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #X #HX #_
+  >(lift_inv_sort1 β€¦ HX) -HX /2/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hded
+  lapply (lt_to_le_to_lt β€¦ (d1+e1) Hid1 ?) // #Hid1e
+  lapply (lt_to_le_to_lt β€¦ (d2-e1) Hid1 ?) /2/ #Hid2e
+  lapply (lt_to_le_to_lt β€¦ Hid1e Hded) -Hid1e Hded #Hid2
+  lapply (lift_inv_lref1_lt β€¦ HX ?) -HX // #HX destruct -X /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
+  elim (lift_inv_lref1 β€¦ HX) -HX * #Hied #HX destruct -X;
+  [2: >plus_plus_comm_23] /4/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
+  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
+  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /2/ #T
+  <plus_minus /3 width=5/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
+  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
+  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
+]
+qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
deleted file mode 100644 (file)
index 26680f3..0000000
+++ /dev/null
@@ -1,173 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "lambda-delta/substitution/lift_defs.ma".
-
-(* RELOCATION ***************************************************************)
-
-(* Main properies ***********************************************************)
-
-lemma lift_inj:  βˆ€d,e,T1,U. β†‘[d,e] T1 β‰‘ U β†’ βˆ€T2. β†‘[d,e] T2 β‰‘ U β†’ T1 = T2.
-#d #e #T1 #U #H elim H -H d e T1 U
-[ #k #d #e #X #HX
-  lapply (lift_inv_sort2 β€¦ HX) -HX //
-| #i #d #e #Hid #X #HX 
-  lapply (lift_inv_lref2_lt β€¦ HX ?) -HX //
-| #i #d #e #Hdi #X #HX 
-  lapply (lift_inv_lref2_ge β€¦ HX ?) -HX /2/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
-  elim (lift_inv_bind2 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
-  elim (lift_inv_flat2 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
-]
-qed.
-
-lemma lift_div_le: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
-                   βˆ€d2,e2,T2. β†‘[d2 + e1, e2] T2 β‰‘ T β†’
-                   d1 β‰€ d2 β†’
-                   βˆƒβˆƒT0. β†‘[d1, e1] T0 β‰‘ T2 & β†‘[d2, e2] T0 β‰‘ T1.
-#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
-  lapply (lift_inv_sort2 β€¦ Hk) -Hk #Hk destruct -T2 /3/
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2
-  lapply (lift_inv_lref2_lt β€¦ Hi ?) -Hi /3/
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  elim (lift_inv_lref2 β€¦ Hi) -Hi * #Hid2 #H destruct -T2
-  [ -Hd12; lapply (lt_plus_to_lt_l β€¦ Hid2) -Hid2 #Hid2 /3/
-  | -Hid1; lapply (arith1 β€¦ Hid2) -Hid2 #Hid2
-    @(ex2_1_intro β€¦ #(i - e2))
-    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le β€¦ Hd12) -Hd12 /2/ | -Hd12 /2/ ]
-    | -Hd12 >(plus_minus_m_m i e2) in βŠ’ (? ? ? ? %) /3/
-    ]
-  ]
-| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
-  lapply (lift_inv_bind2 β€¦ H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
-  elim (IHW β€¦ HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
-  >plus_plus_comm_23 in HU2 #HU2 elim (IHU β€¦ HU2 ?) /3 width = 5/
-| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
-  lapply (lift_inv_flat2 β€¦ H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
-  elim (IHW β€¦ HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
-  elim (IHU β€¦ HU2 ?) /3 width = 5/
-]
-qed.
-
-lemma lift_free: βˆ€d1,e2,T1,T2. β†‘[d1, e2] T1 β‰‘ T2 β†’ βˆ€d2,e1.
-                               d1 β‰€ d2 β†’ d2 β‰€ d1 + e1 β†’ e1 β‰€ e2 β†’
-                               βˆƒβˆƒT. β†‘[d1, e1] T1 β‰‘ T & β†‘[d2, e2 - e1] T β‰‘ T2.
-#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
-[ /3/
-| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
-  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2 /4/
-| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-  lapply (transitive_le β€¦(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
-  <(arith_d1 i e2 e1) // /3/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
-  elim (IHV β€¦ Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT (d2+1) β€¦ ? ? He12) /3 width = 5/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
-  elim (IHV β€¦ Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT d2 β€¦ ? ? He12) /3 width = 5/
-]
-qed.
-
-lemma lift_mono:  βˆ€d,e,T,U1. β†‘[d,e] T β‰‘ U1 β†’ βˆ€U2. β†‘[d,e] T β‰‘ U2 β†’ U1 = U2.
-#d #e #T #U1 #H elim H -H d e T U1
-[ #k #d #e #X #HX
-  lapply (lift_inv_sort1 β€¦ HX) -HX //
-| #i #d #e #Hid #X #HX 
-  lapply (lift_inv_lref1_lt β€¦ HX ?) -HX //
-| #i #d #e #Hdi #X #HX 
-  lapply (lift_inv_lref1_ge β€¦ HX ?) -HX //
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
-  elim (lift_inv_bind1 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
-  elim (lift_inv_flat1 β€¦ HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
-]
-qed.
-
-lemma lift_trans_be: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
-                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’
-                     d1 β‰€ d2 β†’ d2 β‰€ d1 + e1 β†’ β†‘[d1, e1 + e2] T1 β‰‘ T2.
-#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
-  >(lift_inv_sort1 β€¦ HT2) -HT2 //
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_
-  lapply (lt_to_le_to_lt β€¦ Hid1 Hd12) -Hd12 #Hid2
-  lapply (lift_inv_lref1_lt β€¦ HT2 Hid2) /2/
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21
-  lapply (lift_inv_lref1_ge β€¦ HT2 ?) -HT2
-  [ @(transitive_le β€¦ Hd21 ?) -Hd21 /2/
-  | -Hd21 /2/
-  ]
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  lapply (IHV12 β€¦ HV20 ? ?) // -IHV12 HV20 #HV10
-  lapply (IHT12 β€¦ HT20 ? ?) /2/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  lapply (IHV12 β€¦ HV20 ? ?) // -IHV12 HV20 #HV10
-  lapply (IHT12 β€¦ HT20 ? ?) /2/
-]
-qed.
-
-lemma lift_trans_le: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
-                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’ d2 β‰€ d1 β†’
-                     βˆƒβˆƒT0. β†‘[d2, e2] T1 β‰‘ T0 & β†‘[d1 + e2, e1] T0 β‰‘ T2.
-#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #X #HX #_
-  >(lift_inv_sort1 β€¦ HX) -HX /2/
-| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
-  lapply (lt_to_le_to_lt β€¦ (d1+e2) Hid1 ?) // #Hie2
-  elim (lift_inv_lref1 β€¦ HX) -HX * #Hid2 #HX destruct -X /4/
-| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
-  lapply (transitive_le β€¦ Hd21 Hid1) -Hd21 #Hid2
-  lapply (lift_inv_lref1_ge β€¦ HX ?) -HX /2/ #HX destruct -X;
-  >plus_plus_comm_23 /4/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21
-  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
-  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21
-  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
-  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
-]
-qed.
-
-lemma lift_trans_ge: βˆ€d1,e1,T1,T. β†‘[d1, e1] T1 β‰‘ T β†’
-                     βˆ€d2,e2,T2. β†‘[d2, e2] T β‰‘ T2 β†’ d1 + e1 β‰€ d2 β†’
-                     βˆƒβˆƒT0. β†‘[d2 - e1, e2] T1 β‰‘ T0 & β†‘[d1, e1] T0 β‰‘ T2.
-#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #X #HX #_
-  >(lift_inv_sort1 β€¦ HX) -HX /2/
-| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hded
-  lapply (lt_to_le_to_lt β€¦ (d1+e1) Hid1 ?) // #Hid1e
-  lapply (lt_to_le_to_lt β€¦ (d2-e1) Hid1 ?) /2/ #Hid2e
-  lapply (lt_to_le_to_lt β€¦ Hid1e Hded) -Hid1e Hded #Hid2
-  lapply (lift_inv_lref1_lt β€¦ HX ?) -HX // #HX destruct -X /3/
-| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
-  elim (lift_inv_lref1 β€¦ HX) -HX * #Hied #HX destruct -X;
-  [2: >plus_plus_comm_23] /4/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
-  elim (lift_inv_bind1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
-  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /2/ #T
-  <plus_minus /3 width=5/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
-  elim (lift_inv_flat1 β€¦ HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  elim (IHV12 β€¦ HV20 ?) -IHV12 HV20 //
-  elim (IHT12 β€¦ HT20 ?) -IHT12 HT20 /3 width=5/
-]
-qed.
index 934e22054dfa282c9d72bc50388b4c8d94a7560e..eafa007059aab0030d4d0b4de2d9aea2f5b6caea 100644 (file)
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "lambda-delta/syntax/weight.ma".
-include "lambda-delta/substitution/lift_defs.ma".
+include "lambda-delta/substitution/lift.ma".
 
 (* RELOCATION ***************************************************************)
 
diff --git a/matita/matita/lib/lambda-delta/substitution/pts.ma b/matita/matita/lib/lambda-delta/substitution/pts.ma
new file mode 100644 (file)
index 0000000..ac96235
--- /dev/null
@@ -0,0 +1,107 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/drop.ma".
+
+(* PARTIAL TELESCOPIC SUBSTITUTION ******************************************)
+
+inductive pts: lenv β†’ term β†’ nat β†’ nat β†’ term β†’ Prop β‰
+| pts_sort : βˆ€L,k,d,e. pts L (⋆k) d e (⋆k)
+| pts_lref : βˆ€L,i,d,e. pts L (#i) d e (#i)
+| pts_subst: βˆ€L,K,V,U1,U2,i,d,e.
+             d β‰€ i β†’ i < d + e β†’
+             β†“[0, i] L β‰‘ K. π•“{Abbr} V β†’ pts K V 0 (d + e - i - 1) U1 β†’
+             β†‘[0, i + 1] U1 β‰‘ U2 β†’ pts L (#i) d e U2
+| pts_bind : βˆ€L,I,V1,V2,T1,T2,d,e.
+             pts L V1 d e V2 β†’ pts (L. π•“{I} V1) T1 (d + 1) e T2 β†’
+             pts L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| pts_flat : βˆ€L,I,V1,V2,T1,T2,d,e.
+             pts L V1 d e V2 β†’ pts L T1 d e T2 β†’
+             pts L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "partial telescopic substritution"
+   'PSubst L T1 d e T2 = (pts L T1 d e T2).
+
+(* Basic properties *********************************************************)
+
+lemma pts_leq_repl: βˆ€L1,T1,T2,d,e. L1 βŠ’ T1 [d, e] β‰« T2 β†’
+                    βˆ€L2. L1 [d, e] β‰ˆ L2 β†’ L2 βŠ’ T1 [d, e] β‰« T2.
+#L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e
+[ //
+| //
+| #L1 #K1 #V #V1 #V2 #i #d #e #Hdi #Hide #HLK1 #_ #HV12 #IHV12 #L2 #HL12
+  elim (drop_leq_drop1 β€¦ HL12 β€¦ HLK1 ? ?) -HL12 HLK1 // #K2 #HK12 #HLK2
+  @pts_subst [4,5,6,8: // |1,2,3: skip | /2/ ] (**) (* /3 width=6/ is too slow *)
+| /4/
+| /3/
+]
+qed.
+
+lemma pts_refl: βˆ€T,L,d,e. L βŠ’ T [d, e] β‰« T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+lemma pts_weak: βˆ€L,T1,T2,d1,e1. L βŠ’ T1 [d1, e1] β‰« T2 β†’
+                βˆ€d2,e2. d2 β‰€ d1 β†’ d1 + e1 β‰€ d2 + e2 β†’
+                L βŠ’ T1 [d2, e2] β‰« T2.
+#L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1
+[ //
+| //
+| #L #K #V #V1 #V2 #i #d1 #e1 #Hid1 #Hide1 #HLK #_ #HV12 #IHV12 #d2 #e2 #Hd12 #Hde12
+  lapply (transitive_le β€¦ Hd12 β€¦ Hid1) -Hd12 Hid1 #Hid2
+  lapply (lt_to_le_to_lt β€¦ Hide1 β€¦ Hde12) -Hide1 #Hide2
+  @pts_subst [4,5,6,8: // |1,2,3: skip | @IHV12 /2/ ] (**) (* /4 width=6/ is too slow *)
+| /4/
+| /4/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma pts_inv_bind1_aux: βˆ€d,e,L,U1,U2. L βŠ’ U1 [d, e] β‰« U2 β†’
+                         βˆ€I,V1,T1. U1 = π•“{I} V1. T1 β†’
+                         βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & 
+                                  L. π•“{I} V1 βŠ’ T1 [d + 1, e] β‰« T2 &
+                                  U2 =  π•“{I} V2. T2.
+#d #e #L #U1 #U2 * -d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
+]
+qed.
+
+lemma pts_inv_bind1: βˆ€d,e,L,I,V1,T1,U2. L βŠ’ π•“{I} V1. T1 [d, e] β‰« U2 β†’
+                     βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & 
+                              L. π•“{I} V1 βŠ’ T1 [d + 1, e] β‰« T2 &
+                              U2 =  π•“{I} V2. T2.
+/2/ qed.
+
+lemma pts_inv_flat1_aux: βˆ€d,e,L,U1,U2. L βŠ’ U1 [d, e] β‰« U2 β†’
+                         βˆ€I,V1,T1. U1 = π•—{I} V1. T1 β†’
+                         βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & L βŠ’ T1 [d, e] β‰« T2 &
+                                  U2 =  π•—{I} V2. T2.
+#d #e #L #U1 #U2 * -d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+]
+qed.
+
+lemma pts_inv_flat1: βˆ€d,e,L,I,V1,T1,U2. L βŠ’ π•—{I} V1. T1 [d, e] β‰« U2 β†’
+                     βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & L βŠ’ T1 [d, e] β‰« T2 &
+                              U2 =  π•—{I} V2. T2.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/pts_defs.ma b/matita/matita/lib/lambda-delta/substitution/pts_defs.ma
deleted file mode 100644 (file)
index 111052f..0000000
+++ /dev/null
@@ -1,107 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/drop_defs.ma".
-
-(* PARTIAL TELESCOPIC SUBSTITUTION ******************************************)
-
-inductive pts: lenv β†’ term β†’ nat β†’ nat β†’ term β†’ Prop β‰
-| pts_sort : βˆ€L,k,d,e. pts L (⋆k) d e (⋆k)
-| pts_lref : βˆ€L,i,d,e. pts L (#i) d e (#i)
-| pts_subst: βˆ€L,K,V,U1,U2,i,d,e.
-             d β‰€ i β†’ i < d + e β†’
-             β†“[0, i] L β‰‘ K. π•“{Abbr} V β†’ pts K V 0 (d + e - i - 1) U1 β†’
-             β†‘[0, i + 1] U1 β‰‘ U2 β†’ pts L (#i) d e U2
-| pts_bind : βˆ€L,I,V1,V2,T1,T2,d,e.
-             pts L V1 d e V2 β†’ pts (L. π•“{I} V1) T1 (d + 1) e T2 β†’
-             pts L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| pts_flat : βˆ€L,I,V1,V2,T1,T2,d,e.
-             pts L V1 d e V2 β†’ pts L T1 d e T2 β†’
-             pts L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "partial telescopic substritution"
-   'PSubst L T1 d e T2 = (pts L T1 d e T2).
-
-(* Basic properties *********************************************************)
-
-lemma pts_leq_repl: βˆ€L1,T1,T2,d,e. L1 βŠ’ T1 [d, e] β‰« T2 β†’
-                    βˆ€L2. L1 [d, e] β‰ˆ L2 β†’ L2 βŠ’ T1 [d, e] β‰« T2.
-#L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e
-[ //
-| //
-| #L1 #K1 #V #V1 #V2 #i #d #e #Hdi #Hide #HLK1 #_ #HV12 #IHV12 #L2 #HL12
-  elim (drop_leq_drop1 β€¦ HL12 β€¦ HLK1 ? ?) -HL12 HLK1 // #K2 #HK12 #HLK2
-  @pts_subst [4,5,6,8: // |1,2,3: skip | /2/ ] (**) (* /3 width=6/ is too slow *)
-| /4/
-| /3/
-]
-qed.
-
-lemma pts_refl: βˆ€T,L,d,e. L βŠ’ T [d, e] β‰« T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-lemma pts_weak: βˆ€L,T1,T2,d1,e1. L βŠ’ T1 [d1, e1] β‰« T2 β†’
-                βˆ€d2,e2. d2 β‰€ d1 β†’ d1 + e1 β‰€ d2 + e2 β†’
-                L βŠ’ T1 [d2, e2] β‰« T2.
-#L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1
-[ //
-| //
-| #L #K #V #V1 #V2 #i #d1 #e1 #Hid1 #Hide1 #HLK #_ #HV12 #IHV12 #d2 #e2 #Hd12 #Hde12
-  lapply (transitive_le β€¦ Hd12 β€¦ Hid1) -Hd12 Hid1 #Hid2
-  lapply (lt_to_le_to_lt β€¦ Hide1 β€¦ Hde12) -Hide1 #Hide2
-  @pts_subst [4,5,6,8: // |1,2,3: skip | @IHV12 /2/ ] (**) (* /4 width=6/ is too slow *)
-| /4/
-| /4/
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma pts_inv_bind1_aux: βˆ€d,e,L,U1,U2. L βŠ’ U1 [d, e] β‰« U2 β†’
-                         βˆ€I,V1,T1. U1 = π•“{I} V1. T1 β†’
-                         βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & 
-                                  L. π•“{I} V1 βŠ’ T1 [d + 1, e] β‰« T2 &
-                                  U2 =  π•“{I} V2. T2.
-#d #e #L #U1 #U2 * -d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
-]
-qed.
-
-lemma pts_inv_bind1: βˆ€d,e,L,I,V1,T1,U2. L βŠ’ π•“{I} V1. T1 [d, e] β‰« U2 β†’
-                     βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & 
-                              L. π•“{I} V1 βŠ’ T1 [d + 1, e] β‰« T2 &
-                              U2 =  π•“{I} V2. T2.
-/2/ qed.
-
-lemma pts_inv_flat1_aux: βˆ€d,e,L,U1,U2. L βŠ’ U1 [d, e] β‰« U2 β†’
-                         βˆ€I,V1,T1. U1 = π•—{I} V1. T1 β†’
-                         βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & L βŠ’ T1 [d, e] β‰« T2 &
-                                  U2 =  π•—{I} V2. T2.
-#d #e #L #U1 #U2 * -d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
-]
-qed.
-
-lemma pts_inv_flat1: βˆ€d,e,L,I,V1,T1,U2. L βŠ’ π•—{I} V1. T1 [d, e] β‰« U2 β†’
-                     βˆƒβˆƒV2,T2. L βŠ’ V1 [d, e] β‰« V2 & L βŠ’ T1 [d, e] β‰« T2 &
-                              U2 =  π•—{I} V2. T2.
-/2/ qed.
index 9d1cdc3787fb3f4bb4ae289d7192091a86f9b4f4..8cd477738300287fde663a55e2ca54a44ed21cf3 100644 (file)
@@ -9,9 +9,9 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/lift_main.ma".
-include "lambda-delta/substitution/drop_main.ma".
-include "lambda-delta/substitution/pts_defs.ma".
+include "lambda-delta/substitution/lift_lift.ma".
+include "lambda-delta/substitution/drop_drop.ma".
+include "lambda-delta/substitution/pts.ma".
 
 (* PARTIAL TELESCOPIC SUBSTITUTION ******************************************)
 
@@ -115,7 +115,7 @@ lemma pts_inv_lift1_ge: βˆ€L,U1,U2,dt,et. L βŠ’ U1 [dt, et] β‰« U2 β†’
   <(arith_h1 ? ? ? e ? ?) in HV1 // #HV1
   lapply (lift_inv_lref2_ge β€¦ H β€¦ Hdei) -H #H destruct -T1;
   lapply (drop_conf_ge β€¦ HLK β€¦ HLKV ?) -HLK HLKV L // #HKV
-  elim (lift_free β€¦ HV12 d (i - e + 1) ? ? ?) -HV12; [2,3,4: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
+  elim (lift_split β€¦ HV12 d (i - e + 1) ? ? ?) -HV12; [2,3,4: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
   @ex2_1_intro
   [2: @pts_subst [4: /2/ |6,7,8: // |1,2,3: skip |5: @arith5 // ]  
   |1: skip
diff --git a/matita/matita/lib/lambda-delta/syntax/length.ma b/matita/matita/lib/lambda-delta/syntax/length.ma
new file mode 100644 (file)
index 0000000..91e1bd7
--- /dev/null
@@ -0,0 +1,22 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/lenv.ma".
+
+(* LENGTH *******************************************************************)
+
+(* the length of a local environment *)
+let rec length L β‰ match L with
+[ LSort       β‡’ 0
+| LPair L _ _ β‡’ length L + 1
+].
+
+interpretation "length (local environment)" 'card L = (length L).
index 6eebcc64e41e9caddeb32188383464cd9d0c9662..3330813ae417e2a0cdcbaecd02a98b5a789a696b 100644 (file)
@@ -11,7 +11,7 @@
   </section>
   <section name="xoa">
     <key name="output_dir">lib/lambda-delta</key>
-    <key name="objects">xoa_defs</key>    
+    <key name="objects">xoa</key>    
     <key name="notations">xoa_notation</key>
     <key name="include">basics/pts.ma</key>
     <key name="ex">2 1</key>
diff --git a/matita/matita/lib/lambda-delta/xoa.ma b/matita/matita/lib/lambda-delta/xoa.ma
new file mode 100644 (file)
index 0000000..582b2d2
--- /dev/null
@@ -0,0 +1,135 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+(* multiple existental quantifier (2, 1) *)
+
+inductive ex2_1 (A0:Type[0]) (P0,P1:A0β†’Prop) : Prop β‰
+   | ex2_1_intro: βˆ€x0. P0 x0 β†’ P1 x0 β†’ ex2_1 ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
+
+(* multiple existental quantifier (2, 2) *)
+
+inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0β†’A1β†’Prop) : Prop β‰
+   | ex2_2_intro: βˆ€x0,x1. P0 x0 x1 β†’ P1 x0 x1 β†’ ex2_2 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+
+(* multiple existental quantifier (3, 1) *)
+
+inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0β†’Prop) : Prop β‰
+   | ex3_1_intro: βˆ€x0. P0 x0 β†’ P1 x0 β†’ P2 x0 β†’ ex3_1 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
+
+(* multiple existental quantifier (3, 2) *)
+
+inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0β†’A1β†’Prop) : Prop β‰
+   | ex3_2_intro: βˆ€x0,x1. P0 x0 x1 β†’ P1 x0 x1 β†’ P2 x0 x1 β†’ ex3_2 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
+
+(* multiple existental quantifier (3, 3) *)
+
+inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0β†’A1β†’A2β†’Prop) : Prop β‰
+   | ex3_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ ex3_3 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
+
+(* multiple existental quantifier (4, 3) *)
+
+inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0β†’A1β†’A2β†’Prop) : Prop β‰
+   | ex4_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ P3 x0 x1 x2 β†’ ex4_3 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
+
+(* multiple existental quantifier (4, 4) *)
+
+inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0β†’A1β†’A2β†’A3β†’Prop) : Prop β‰
+   | ex4_4_intro: βˆ€x0,x1,x2,x3. P0 x0 x1 x2 x3 β†’ P1 x0 x1 x2 x3 β†’ P2 x0 x1 x2 x3 β†’ P3 x0 x1 x2 x3 β†’ ex4_4 ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
+
+(* multiple existental quantifier (5, 3) *)
+
+inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0β†’A1β†’A2β†’Prop) : Prop β‰
+   | ex5_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ P3 x0 x1 x2 β†’ P4 x0 x1 x2 β†’ ex5_3 ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4).
+
+(* multiple existental quantifier (5, 4) *)
+
+inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0β†’A1β†’A2β†’A3β†’Prop) : Prop β‰
+   | ex5_4_intro: βˆ€x0,x1,x2,x3. P0 x0 x1 x2 x3 β†’ P1 x0 x1 x2 x3 β†’ P2 x0 x1 x2 x3 β†’ P3 x0 x1 x2 x3 β†’ P4 x0 x1 x2 x3 β†’ ex5_4 ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
+
+(* multiple existental quantifier (6, 6) *)
+
+inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0β†’A1β†’A2β†’A3β†’A4β†’A5β†’Prop) : Prop β‰
+   | ex6_6_intro: βˆ€x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β†’ P1 x0 x1 x2 x3 x4 x5 β†’ P2 x0 x1 x2 x3 x4 x5 β†’ P3 x0 x1 x2 x3 x4 x5 β†’ P4 x0 x1 x2 x3 x4 x5 β†’ P5 x0 x1 x2 x3 x4 x5 β†’ ex6_6 ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
+
+(* multiple existental quantifier (7, 6) *)
+
+inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0β†’A1β†’A2β†’A3β†’A4β†’A5β†’Prop) : Prop β‰
+   | ex7_6_intro: βˆ€x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β†’ P1 x0 x1 x2 x3 x4 x5 β†’ P2 x0 x1 x2 x3 x4 x5 β†’ P3 x0 x1 x2 x3 x4 x5 β†’ P4 x0 x1 x2 x3 x4 x5 β†’ P5 x0 x1 x2 x3 x4 x5 β†’ P6 x0 x1 x2 x3 x4 x5 β†’ ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
+(* multiple disjunction connective (3) *)
+
+inductive or3 (P0,P1,P2:Prop) : Prop β‰
+   | or3_intro0: P0 β†’ or3 ? ? ?
+   | or3_intro1: P1 β†’ or3 ? ? ?
+   | or3_intro2: P2 β†’ or3 ? ? ?
+.
+
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
+
+(* multiple disjunction connective (4) *)
+
+inductive or4 (P0,P1,P2,P3:Prop) : Prop β‰
+   | or4_intro0: P0 β†’ or4 ? ? ? ?
+   | or4_intro1: P1 β†’ or4 ? ? ? ?
+   | or4_intro2: P2 β†’ or4 ? ? ? ?
+   | or4_intro3: P3 β†’ or4 ? ? ? ?
+.
+
+interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+
+(* multiple conjunction connective (3) *)
+
+inductive and3 (P0,P1,P2:Prop) : Prop β‰
+   | and3_intro: P0 β†’ P1 β†’ P2 β†’ and3 ? ? ?
+.
+
+interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
+
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
deleted file mode 100644 (file)
index 582b2d2..0000000
+++ /dev/null
@@ -1,135 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was generated by xoa.native: do not edit *********************)
-
-include "basics/pts.ma".
-
-(* multiple existental quantifier (2, 1) *)
-
-inductive ex2_1 (A0:Type[0]) (P0,P1:A0β†’Prop) : Prop β‰
-   | ex2_1_intro: βˆ€x0. P0 x0 β†’ P1 x0 β†’ ex2_1 ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
-
-(* multiple existental quantifier (2, 2) *)
-
-inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0β†’A1β†’Prop) : Prop β‰
-   | ex2_2_intro: βˆ€x0,x1. P0 x0 x1 β†’ P1 x0 x1 β†’ ex2_2 ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
-
-(* multiple existental quantifier (3, 1) *)
-
-inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0β†’Prop) : Prop β‰
-   | ex3_1_intro: βˆ€x0. P0 x0 β†’ P1 x0 β†’ P2 x0 β†’ ex3_1 ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
-
-(* multiple existental quantifier (3, 2) *)
-
-inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0β†’A1β†’Prop) : Prop β‰
-   | ex3_2_intro: βˆ€x0,x1. P0 x0 x1 β†’ P1 x0 x1 β†’ P2 x0 x1 β†’ ex3_2 ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
-
-(* multiple existental quantifier (3, 3) *)
-
-inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0β†’A1β†’A2β†’Prop) : Prop β‰
-   | ex3_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ ex3_3 ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
-
-(* multiple existental quantifier (4, 3) *)
-
-inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0β†’A1β†’A2β†’Prop) : Prop β‰
-   | ex4_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ P3 x0 x1 x2 β†’ ex4_3 ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
-
-(* multiple existental quantifier (4, 4) *)
-
-inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0β†’A1β†’A2β†’A3β†’Prop) : Prop β‰
-   | ex4_4_intro: βˆ€x0,x1,x2,x3. P0 x0 x1 x2 x3 β†’ P1 x0 x1 x2 x3 β†’ P2 x0 x1 x2 x3 β†’ P3 x0 x1 x2 x3 β†’ ex4_4 ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
-
-(* multiple existental quantifier (5, 3) *)
-
-inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0β†’A1β†’A2β†’Prop) : Prop β‰
-   | ex5_3_intro: βˆ€x0,x1,x2. P0 x0 x1 x2 β†’ P1 x0 x1 x2 β†’ P2 x0 x1 x2 β†’ P3 x0 x1 x2 β†’ P4 x0 x1 x2 β†’ ex5_3 ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4).
-
-(* multiple existental quantifier (5, 4) *)
-
-inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0β†’A1β†’A2β†’A3β†’Prop) : Prop β‰
-   | ex5_4_intro: βˆ€x0,x1,x2,x3. P0 x0 x1 x2 x3 β†’ P1 x0 x1 x2 x3 β†’ P2 x0 x1 x2 x3 β†’ P3 x0 x1 x2 x3 β†’ P4 x0 x1 x2 x3 β†’ ex5_4 ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
-
-(* multiple existental quantifier (6, 6) *)
-
-inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0β†’A1β†’A2β†’A3β†’A4β†’A5β†’Prop) : Prop β‰
-   | ex6_6_intro: βˆ€x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β†’ P1 x0 x1 x2 x3 x4 x5 β†’ P2 x0 x1 x2 x3 x4 x5 β†’ P3 x0 x1 x2 x3 x4 x5 β†’ P4 x0 x1 x2 x3 x4 x5 β†’ P5 x0 x1 x2 x3 x4 x5 β†’ ex6_6 ? ? ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
-
-(* multiple existental quantifier (7, 6) *)
-
-inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0β†’A1β†’A2β†’A3β†’A4β†’A5β†’Prop) : Prop β‰
-   | ex7_6_intro: βˆ€x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β†’ P1 x0 x1 x2 x3 x4 x5 β†’ P2 x0 x1 x2 x3 x4 x5 β†’ P3 x0 x1 x2 x3 x4 x5 β†’ P4 x0 x1 x2 x3 x4 x5 β†’ P5 x0 x1 x2 x3 x4 x5 β†’ P6 x0 x1 x2 x3 x4 x5 β†’ ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
-
-(* multiple disjunction connective (3) *)
-
-inductive or3 (P0,P1,P2:Prop) : Prop β‰
-   | or3_intro0: P0 β†’ or3 ? ? ?
-   | or3_intro1: P1 β†’ or3 ? ? ?
-   | or3_intro2: P2 β†’ or3 ? ? ?
-.
-
-interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
-
-(* multiple disjunction connective (4) *)
-
-inductive or4 (P0,P1,P2,P3:Prop) : Prop β‰
-   | or4_intro0: P0 β†’ or4 ? ? ? ?
-   | or4_intro1: P1 β†’ or4 ? ? ? ?
-   | or4_intro2: P2 β†’ or4 ? ? ? ?
-   | or4_intro3: P3 β†’ or4 ? ? ? ?
-.
-
-interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
-
-(* multiple conjunction connective (3) *)
-
-inductive and3 (P0,P1,P2:Prop) : Prop β‰
-   | and3_intro: P0 β†’ P1 β†’ P2 β†’ and3 ? ? ?
-.
-
-interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
-
index 96765671641676a2474d0e5fa35bb61dde01872d..f07bc89be410715965dac9ac56f5f8cfcff6d659 100644 (file)
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "lambda-delta/xoa_notation.ma".
-include "lambda-delta/xoa_defs.ma".
+include "lambda-delta/xoa.ma".
 
 lemma ex2_1_comm: βˆ€A0. βˆ€P0,P1:A0β†’Prop. (βˆƒβˆƒx0. P0 x0 & P1 x0) β†’ βˆƒβˆƒx0. P1 x0 & P0 x0.
 #A0 #P0 #P1 * /2/