(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-(* *****************************************************************)
+(* Syntax *******************************************************************)
notation "hvbox( β )"
non associative with precedence 90
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 }.
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
non associative with precedence 45
for @{ 'PSubst $L $T1 $d $e $T2 }.
-(* reduction ****************************************************************)
+(* Reduction ****************************************************************)
notation "hvbox( T1 β break T2 )"
non associative with precedence 45
--- /dev/null
+(*
+ ||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 ***************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(*
+ ||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.
+++ /dev/null
-(*
- ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
(* *)
(**************************************************************************)
-include "lambda-delta/reduction/lpr_defs.ma".
+include "lambda-delta/reduction/lpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
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 *********************************)
--- /dev/null
+(*
+ ||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.
+++ /dev/null
-(*
- ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(*
+ ||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.
+++ /dev/null
-(*
- ||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.
--- /dev/null
+(*
+ ||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.
+++ /dev/null
-(*
- ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
(**************************************************************************)
include "lambda-delta/syntax/weight.ma".
-include "lambda-delta/substitution/lift_defs.ma".
+include "lambda-delta/substitution/lift.ma".
(* RELOCATION ***************************************************************)
--- /dev/null
+(*
+ ||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.
+++ /dev/null
-(*
- ||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.
\ /
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 ******************************************)
<(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
--- /dev/null
+(*
+ ||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).
</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>
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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).
-
(**************************************************************************)
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/
projects / helm.git / commitdiff