# check ######################################################################
-pr2/clen pr2_gen_cbind
-pr2/clen pr2_gen_cflat
-pr2/fwd pr2_gen_sort
-pr2/fwd pr2_gen_lref
-pr2/fwd pr2_gen_abst
-pr2/fwd pr2_gen_cast
-pr2/fwd pr2_gen_csort
-pr2/fwd pr2_gen_appl
-pr2/fwd pr2_gen_abbr
pr2/fwd pr2_gen_void
-pr2/fwd pr2_gen_lift
-pr2/pr2 pr2_confluence__pr2_free_free
-pr2/pr2 pr2_confluence__pr2_free_delta
-pr2/pr2 pr2_confluence__pr2_delta_delta
-pr2/pr2 pr2_confluence
-pr2/props pr2_thin_dx
-pr2/props pr2_head_1
-pr2/props pr2_head_2
-pr2/props clear_pr2_trans
-pr2/props pr2_cflat
pr2/props pr2_ctail
-pr2/props pr2_change
-pr2/props pr2_lift
-pr2/subst1 pr2_delta1
-pr2/subst1 pr2_subst1
-pr2/subst1 pr2_gen_cabbr
+
+
+# waiting ####################################################################
+
pr3/fwd pr3_gen_sort
pr3/fwd pr3_gen_abst
pr3/fwd pr3_gen_cast
sty1/props sty1_cast2
subst0/dec dnf_dec2
subst0/dec dnf_dec
-subst1/fwd subst1_gen_lift_ge
-subst1/fwd subst1_gen_lift_lt
-subst1/fwd subst1_gen_lift_eq
-subst1/props subst1_lift_ge
-subst1/props subst1_lift_lt
subst1/props subst1_ex
-subst1/props subst1_lift_S
-subst1/subst1 subst1_subst1
-subst1/subst1 subst1_subst1_back
-subst1/subst1 subst1_trans
-subst1/subst1 subst1_confluence_lift
subst/fwd subst_sort
subst/fwd subst_lref_lt
subst/fwd subst_lref_eq
(* *)
(**************************************************************************)
-(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS
+(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
* Specification started: 2011 April 17
+ * Confluence of context-free parallel reduction closed: 2011 September 6
* - Patience on me so that I gain peace and perfection! -
* [ suggested invocation to start formal specifications with ]
*)
include "Ground-2/list.ma".
+include "Ground-2/star.ma".
include "Basic-2/notation.ma".
(* ITEMS ********************************************************************)
(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-inductive leq: lenv → nat → nat → lenv → Prop ≝
-| leq_sort: ∀d,e. leq (⋆) d e (⋆)
-| leq_OO: ∀L1,L2. leq L1 0 0 L2
-| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V)
+inductive leq: nat → nat → relation lenv ≝
+| leq_sort: ∀d,e. leq d e (⋆) (⋆)
+| leq_OO: ∀L1,L2. leq 0 0 L1 L2
+| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
+ leq 0 (e + 1) (L1. 𝕓{I} V) (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)
+ leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
.
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
+
+definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L1,s1,s2. R L1 s1 s2 →
+ ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
(* Basic properties *********************************************************)
+lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -H s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
+]
+qed.
+
lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
#d elim d -d
[ #e elim e -e // #e #IHe #L elim L -L /2/
(* HOMOMORPHIC TERMS ********************************************************)
-inductive thom: term → term → Prop ≝
+inductive thom: relation term ≝
| thom_atom: ∀I. thom (𝕒{I}) (𝕒{I})
| thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2)
| thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] →
notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
non associative with precedence 45
- for @{ 'RLift $T1 $d $e $T2 }.
+ for @{ 'RLift $d $e $T1 $T2 }.
notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
non associative with precedence 45
- for @{ 'RDrop $L1 $d $e $L2 }.
+ for @{ 'RDrop $d $e $L1 $L2 }.
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 }.
+(* Unfold *******************************************************************)
+
+notation "hvbox( T1 break [ d , break e ] ≫* break T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $T1 $d $e $T2 }.
+
+notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+
(* Reduction ****************************************************************)
notation "hvbox( T1 ⇒ break T2 )"
notation "hvbox( L1 ⊢ ⇒ break L2 )"
non associative with precedence 45
for @{ 'CPRed $L1 $L2 }.
+
+(* Computation **************************************************************)
+
+notation "hvbox( T1 ⇒* break T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $T1 $T2 }.
+
+notation "hvbox( L ⊢ break term 90 T1 ⇒* break T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $L $T1 $T2 }.
+
+notation "hvbox( L1 ⊢ ⇒* break L2 )"
+ non associative with precedence 45
+ for @{ 'CPRedStar $L1 $L2 }.
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-definition cpr: lenv → term → term → Prop ≝
+(* Basic-1: includes: pr2_delta1 *)
+definition cpr: lenv → relation term ≝
λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2.
interpretation
(* Basic properties *********************************************************)
+(* Basic-1: was by definition: pr2_free *)
lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
/2/ qed.
#I #L #V1 #V2 #T1 #T2 * /3 width=5/
qed.
+(* Basic-1: was only: pr2_gen_cbind *)
lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
/3 width=5/
qed.
-(* NOTE: new property *)
+(* Note: new property *)
+(* Basic-1: was only: pr2_thin_dx *)
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/
(* Basic inversion lemmas ***************************************************)
-lemma cpr_inv_lsort: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
+(* Basic-1: was: pr2_gen_csort *)
+lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
#T1 #T2 * #T #HT normalize #HT2
<(tps_inv_refl_O2 … HT2) -HT2 //
qed.
+(* Basic-1: was: pr2_gen_sort *)
+lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
+#L #T2 #k * #X #H
+>(tpr_inv_atom1 … H) -H #H
+>(tps_inv_sort1 … H) -H //
+qed.
+
+(* Basic-1: was: pr2_gen_lref *)
+lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
+ T2 = #i ∨
+ ∃∃K,T. ↓[0, i] L ≡ K. 𝕓{Abbr} T & ↑[0, i + 1] T ≡ T2 &
+ i < |L|.
+#L #T2 #i * #X #H
+>(tpr_inv_atom1 … H) -H #H
+elim (tps_inv_lref1 … H) -H /2/
+* #K #T #_ #Hi #HLK #HTT2 /3/
+qed.
+(*
+(* Basic-1: was: pr2_gen_cast *)
+lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
+ ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 &
+ U2 = 𝕔{Cast} V2. T2
+ ) ∨ L ⊢ T1 ⇒ U2.
+#L #V1 #T1 #U2 * #X #H #HU2
+elim (tpr_inv_cast1 … H) -H /3/
+* #V #T #HV1 #HT1 #H whd (* >H in HU2; *) destruct -X;
+elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
+*)
(* Basic forward lemmas *****************************************************)
lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
| normalize /3/
].
qed.
+
+(* Basic-1: removed theorems 5:
+ pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+*)
+
+(*
+pr2/fwd pr2_gen_appl
+pr2/fwd pr2_gen_abbr
+pr2/pr2 pr2_confluence__pr2_free_free
+pr2/pr2 pr2_confluence__pr2_free_delta
+pr2/pr2 pr2_confluence__pr2_delta_delta
+pr2/pr2 pr2_confluence
+pr2/props pr2_change
+pr2/subst1 pr2_subst1
+pr2/subst1 pr2_gen_cabbr
+*)
--- /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 "Basic-2/reduction/tpr_tpr.ma".
+include "Basic-2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Main properties **********************************************************)
+(*
+(* Basic-1: was: pr2_confluence *)
+theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 →
+ ∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T.
+#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
+elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2
+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 "Basic-2/reduction/tpr_lift.ma".
+include "Basic-2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Relocation properties ****************************************************)
+
+(* Basic-1: was: pr2_lift *)
+
+(* Basic-1: was: pr2_gen_lift *)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic-1: was: pr2_gen_abst *)
+lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
+/2/ qed.
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
-inductive lcpr: lenv → lenv → Prop ≝
+inductive lcpr: relation lenv ≝
| lcpr_sort: lcpr (⋆) (⋆)
| lcpr_item: ∀K1,K2,I,V1,V2.
lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-inductive ltpr: lenv → lenv → Prop ≝
+inductive ltpr: relation lenv ≝
| ltpr_sort: ltpr (⋆) (⋆)
| ltpr_item: ∀K1,K2,I,V1,V2.
ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
#L1 #K1 #d #e #H elim H -H L1 K1 d e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
-| #L1 #K1 #I #V1 #HLK1 #_ #X #H
- <(drop_inv_refl … HLK1) -HLK1 K1;
+| #K1 #I #V1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
#L1 #K1 #d #e #H elim H -H L1 K1 d e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
-| #L1 #K1 #I #V1 #HLK1 #_ #X #H
- >(drop_inv_refl … HLK1) -HLK1 L1;
+| #K1 #I #V1 #X #H
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* Basic-1: includes: pr0_delta1 *)
-inductive tpr: term → term → Prop ≝
+inductive tpr: relation term ≝
| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
include "Basic-2/substitution/tps_lift.ma".
include "Basic-2/reduction/tpr.ma".
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
(* Relocation properties ****************************************************)
(* Basic-1: was: pr0_lift *)
(* DROPPING *****************************************************************)
(* Basic-1: includes: drop_skip_bind *)
-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
+inductive drop: nat → nat → relation lenv ≝
+| drop_atom: ∀d,e. drop d e (⋆) (⋆)
+| drop_pair: ∀L,I,V. drop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
+| drop_drop: ∀L1,L2,I,V,e. drop 0 e L1 L2 → drop 0 (e + 1) (L1. 𝕓{I} V) 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)
+ drop d e L1 L2 → ↑[d,e] V2 ≡ V1 →
+ drop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
.
-interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2).
+interpretation "dropping" 'RDrop d e L1 L2 = (drop d e L1 L2).
(* Basic inversion lemmas ***************************************************)
fact 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
+#d #e #L1 #L2 * -d e L1 L2
[ //
-| #L1 #L2 #I #V #_ #IHL12 #H1 #H2
- >(IHL12 H1 H2) -IHL12 H1 H2 L1 //
-| #L1 #L2 #I #V #e #_ #_ #_ #H
+| //
+| #L1 #L2 #I #V #e #_ #_ #H
elim (plus_S_eq_O_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #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.
-fact drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
+fact drop_inv_atom1_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
+| #L #I #V #H destruct
| #L1 #L2 #I #V #e #_ #H destruct
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
]
qed.
(* Basic-1: was: drop_gen_sort *)
-lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆.
+lemma drop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆.
/2 width=5/ qed.
fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
(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/
+| #L #I #V #_ #K #J #W #HX destruct -L I V /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)
]
L2 = K2. 𝕓{I} V2.
#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)
+| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z
/2 width=5/
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)
+| #L #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/
(* Basic-1: was by definition: drop_refl *)
lemma drop_refl: ∀L. ↓[0, 0] L ≡ L.
-#L elim L -L /2/
+#L elim L -L //
qed.
lemma drop_drop_lt: ∀L1,L2,I,V,e.
↓[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
+ lapply (drop_inv_atom1 … H) -H #H destruct
| #L1 #L2 #I #K1 #V #i #_ #_ #H
elim (lt_zero_false … H)
| #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie
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
+[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … 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/
lemma drop_fwd_drop2_length: ∀L1,I2,K2,V2,e.
↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|.
#L1 elim L1 -L1
-[ #I2 #K2 #V2 #e #H lapply (drop_inv_sort1 … H) -H #H destruct
+[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … 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 //
lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e.
#L1 elim L1 -L1
-[ #L2 #e #H >(drop_inv_sort1 … H) -H //
+[ #L2 #e #H >(drop_inv_atom1 … H) -H //
| #K1 #I1 #V1 #IHL1 #L2 #e #H
elim (drop_inv_O1 … H) -H * #He #H
[ -IHL1; destruct -e L2 //
∀L2. ↓[d, e] L ≡ L2 → L1 = L2.
#d #e #L #L1 #H elim H -H d e L L1
[ #d #e #L2 #H
- >(drop_inv_sort1 … H) -H L2 //
-| #K1 #K2 #I #V #HK12 #_ #L2 #HL12
- <(drop_inv_refl … HK12) -HK12 K2
+ >(drop_inv_atom1 … H) -H L2 //
+| #K #I #V #L2 #HL12
<(drop_inv_refl … HL12) -HL12 L2 //
| #L #K #I #V #e #_ #IHLK #L2 #H
lapply (drop_inv_drop1 … H ?) -H /2/
↓[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 //
+ >(drop_inv_atom1 … H) -H L2 //
+| //
| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
lapply (drop_inv_drop1 … H ?) -H /2/ #HL2
<minus_plus_comm /3/
↓[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
+ lapply (drop_inv_atom1 … H) -H #H destruct
+| #L #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)
∃∃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;
+ >(drop_inv_atom1 … H) -H L2 /2/
+| #K #I #V #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;
∀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 //
+ >(drop_inv_atom1 … H) -H L2 //
+| //
| /3/
| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
lapply (lt_to_le_to_lt 0 … Hde2) // #He2
(* Basic-1: includes:
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
*)
-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))
+inductive lift: nat → nat → relation term ≝
+| lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k)
+| lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
+| lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(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 d e V1 V2 → lift (d + 1) e T1 T2 →
+ lift d e (𝕓{I} V1. T1) (𝕓{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)
+ lift d e V1 V2 → lift d e T1 T2 →
+ lift d e (𝕗{I} V1. T1) (𝕗{I} V2. T2)
.
-interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
+interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
(* Basic properties *********************************************************)
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* Basic-1: includes: csubst1_bind *)
-inductive ltps: lenv → nat → nat → lenv → Prop ≝
-| ltps_atom: ∀d,e. ltps (⋆) d e (⋆)
-| ltps_pair: ∀L,I,V. ltps (L. 𝕓{I} V) 0 0 (L. 𝕓{I} V)
+inductive ltps: nat → nat → relation lenv ≝
+| ltps_atom: ∀d,e. ltps d e (⋆) (⋆)
+| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
| ltps_tps2: ∀L1,L2,I,V1,V2,e.
- ltps L1 0 e L2 → L2 ⊢ V1 [0, e] ≫ V2 →
- ltps (L1. 𝕓{I} V1) 0 (e + 1) L2. 𝕓{I} V2
+ ltps 0 e L1 L2 → L2 ⊢ V1 [0, e] ≫ V2 →
+ ltps 0 (e + 1) (L1. 𝕓{I} V1) L2. 𝕓{I} V2
| ltps_tps1: ∀L1,L2,I,V1,V2,d,e.
- ltps L1 d e L2 → L2 ⊢ V1 [d, e] ≫ V2 →
- ltps (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
+ ltps d e L1 L2 → L2 ⊢ V1 [d, e] ≫ V2 →
+ ltps (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
.
interpretation "parallel substritution (local environment)"
- 'PSubst L1 d e L2 = (ltps L1 d e L2).
+ 'PSubst L1 d e L2 = (ltps d e L1 L2).
(* Basic properties *********************************************************)
∀L2,e2. ↓[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H //
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
| //
| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
lapply (plus_le_weak … He12) #He2
∀L2,e2. ↓[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H //
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
| //
| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
lapply (plus_le_weak … He12) #He2
∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
| /2/
| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
| /2/
| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
]
qed.
+(* Basic-1: was: subst1_subst1_back *)
lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
]
qed.
+(* Basic-1: was: subst1_subst1 *)
lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L1 [d1, e1] ≫ L0 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
-inductive tps: lenv → term → nat → nat → term → Prop ≝
-| tps_atom : ∀L,I,d,e. tps L (𝕒{I}) d e (𝕒{I})
+inductive tps: nat → nat → lenv → relation term ≝
+| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
- ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps L (#i) d e W
+ ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps d e L (#i) W
| tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
- tps L V1 d e V2 → tps (L. 𝕓{I} V2) T1 (d + 1) e T2 →
- tps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+ tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
+ tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
| tps_flat : ∀L,I,V1,V2,T1,T2,d,e.
- tps L V1 d e V2 → tps L T1 d e T2 →
- tps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+ tps d e L V1 V2 → tps d e L T1 T2 →
+ tps d e L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
.
interpretation "parallel substritution (term)"
- 'PSubst L T1 d e T2 = (tps L T1 d e T2).
+ 'PSubst L T1 d e T2 = (tps d e L T1 T2).
(* Basic properties *********************************************************)
lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2.
/2 width=6/ qed.
-(* Basic-1: removed theorems 23:
+(* Basic-1: removed theorems 25:
subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
subst0_confluence_lift subst0_tlt
- subst1_head subst1_gen_head
+ subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift
*)
(* Relocation properties ****************************************************)
+(* Basic-1: was: subst1_lift_lt *)
lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
∀L,U1,U2,d,e. ↓[d, e] L ≡ K →
↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 →
]
qed.
+(* Basic-1: was: subst1_lift_ge *)
lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
∀L,U1,U2,d,e. ↓[d, e] L ≡ K →
↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 →
]
qed.
+(* Basic-1: was: subst1_gen_lift_lt *)
lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
dt + et ≤ d →
]
qed.
+(* Basic-1: was: subst1_gen_lift_ge *)
lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
d + e ≤ dt →
]
qed.
+(* Basic-1: was: subst1_gen_lift_eq *)
lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e.
L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H elim H -H L U1 U2 d e
]
qed.
(*
- Theorem subst0_gen_lift_ge : (u,t1,x:?; i,h,d:?) (subst0 i u (lift h d t1) x) ->
- (le (plus d h) i) ->
- (EX t2 | x = (lift h d t2) & (subst0 (minus i h) u t1 t2)).
-
Theorem subst0_gen_lift_rev_ge: (t1,v,u2:?; i,h,d:?)
(subst0 i v t1 (lift h d u2)) ->
(le (plus d h) i) ->
qed.
(* Note: the constant 1 comes from tps_subst *)
+(* Basic-1: was: subst1_trans *)
theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 →
∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e →
L ⊢ T1 [d, e] ≫ T2.
--- /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 "Basic-2/substitution/tps.ma".
+
+(* PARTIAL UNFOLD ON TERMS **************************************************)
+
+definition tpss: nat → nat → lenv → relation term ≝
+ λd,e,L. TC … (tps d e L).
+
+interpretation "partial unfold (term)"
+ 'PSubstStar L T1 d e T2 = (tpss d e L T1 T2).
+
+(* Basic properties *********************************************************)
+
--- /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 "basics/star.ma".
+include "Ground-2/xoa_props.ma".
+
+(* PROPERTIES of RELATIONS **************************************************)
+
+definition confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
+ ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & R a2 a.
+
+lemma TC_strip: ∀A,R. confluent A R →
+ ∀a0,a1. TC … R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & TC … R a2 a.
+#A #R #HR #a0 #a1 #H elim H -H a1
+[ #a1 #Ha01 #a2 #Ha02
+ elim (HR … Ha01 … Ha02) -HR a0 /3/
+| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
+ elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
+ elim (HR … Ha1 … Ha0) -HR a /4/
+]
+qed.
+
+lemma TC_confluent: ∀A,R. confluent A R → confluent A (TC … R).
+#A #R #HR #a0 #a1 #H elim H -H a1
+[ #a1 #Ha01 #a2 #Ha02
+ elim (TC_strip … HR … Ha02 … Ha01) -HR a0 /3/
+| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
+ elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
+ elim (TC_strip … HR … Ha0 … Ha1) -HR a /4/
+]
+qed.
+
+lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
+/2/ qed.
+
projects / helm.git / commitdiff