From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 29 Jul 2012 17:41:46 +0000 (+0000)
Subject: - context free computation for terms and local environments
X-Git-Tag: make_still_working~1589
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f79d97a42a84f94d37ad9589fcce46149ee23d12;p=helm.git
- context free computation for terms and local environments
---
diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 70d162599..178f0d0a8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -170,17 +170,11 @@ pr0/fwd pr0_gen_void
pr0/dec nf0_dec
pr0/subst1 pr0_subst1_back
pr0/subst1 pr0_subst1_fwd
-pr1/pr1 pr1_strip
-pr1/pr1 pr1_confluence
-pr1/props pr1_pr0
-pr1/props pr1_t
-pr1/props pr1_head_1
-pr1/props pr1_head_2
-pr1/props pr1_comp
+
pr1/props pr1_eta
+
pr2/fwd pr2_gen_void
pr3/fwd pr3_gen_void
-pr3/pr1 pr3_pr1
pr3/props pr3_eta
sn3/props sns3_lifts
sty1/cnt sty1_cnt
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index 0891cb00c..ae0c1ae62 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -13,6 +13,7 @@
(**************************************************************************)
include "basic_2/reducibility/cnf.ma".
+include "basic_2/computation/tprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@@ -68,6 +69,11 @@ lemma cprs_flat_dx: âI,L,V1,V2. L ⢠V1 â¡ V2 â âT1,T2. L ⢠T1 â¡* T2
@(cprs_strap1 ⦠IHT2) -IHT2 /2 width=1/
qed.
+(* Basic_1: was: pr3_pr1 *)
+lemma tprs_cprs: âT1,T2. T1 â¡* T2 â âL. L ⢠T1 â¡* T2.
+#T1 #T2 #H @(tprs_ind ⦠H) -T2 /2 width=1/ /3 width=3/
+qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: pr3_gen_sort *)
@@ -94,6 +100,9 @@ lemma cprs_inv_cnf1: âL,T,U. L ⢠T â¡* U â L ⢠ðâ¦T⦠â T = U.
lapply (H2T0 ⦠H1T0) -H1T0 #H destruct /2 width=1/
qed-.
+lemma tprs_inv_cnf1: âT,U. T â¡* U â â ⢠ðâ¦T⦠â T = U.
+/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-.
+
(* Basic_1: removed theorems 10:
clear_pr3_trans pr3_cflat pr3_gen_bind
pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma
new file mode 100644
index 000000000..b7b0e1094
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+definition ltprs: relation lenv â TC ⦠ltpr.
+
+interpretation
+ "context-free parallel computation (environment)"
+ 'PRedStar L1 L2 = (ltprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltprs_ind: âL1. âR:predicate lenv. R L1 â
+ (âL,L2. L1 â¡* L â L â¡ L2 â R L â R L2) â
+ âL2. L1 â¡* L2 â R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind ⦠HL1 IHL1 ⦠HL12) //
+qed-.
+
+lemma ltprs_ind_dx: âL2. âR:predicate lenv. R L2 â
+ (âL1,L. L1 â¡ L â L â¡* L2 â R L â R L1) â
+ âL1. L1 â¡* L2 â R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx ⦠HL2 IHL2 ⦠HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_refl: reflexive ⦠ltprs.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprs_inv_atom1: âL2. â â¡* L2 â L2 = â.
+#L2 #H @(ltprs_ind ⦠H) -L2 //
+#L #L2 #_ #HL2 #IHL1 destruct
+>(ltpr_inv_atom1 ⦠HL2) -L2 //
+qed-.
+
+lemma ltprs_inv_pair1: âI,K1,L2,V1. K1. â{I} V1 â¡* L2 â
+ ââK2,V2. K1 â¡* K2 & V1 â¡* V2 & L2 = K2. â{I} V2.
+#I #K1 #L2 #V1 #H @(ltprs_ind ⦠H) -L2 /2 width=5/
+#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+elim (ltpr_inv_pair1 ⦠HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
+qed-.
+
+lemma ltprs_inv_atom2: âL1. L1 â¡* â â L1 = â.
+#L1 #H @(ltprs_ind_dx ⦠H) -L1 //
+#L1 #L #HL1 #_ #IHL2 destruct
+>(ltpr_inv_atom2 ⦠HL1) -L1 //
+qed-.
+
+lemma ltprs_inv_pair2: âI,L1,K2,V2. L1 â¡* K2. â{I} V2 â
+ ââK1,V1. K1 â¡* K2 & V1 â¡* V2 & L1 = K1. â{I} V1.
+#I #L1 #K2 #V2 #H @(ltprs_ind_dx ⦠H) -L1 /2 width=5/
+#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+elim (ltpr_inv_pair2 ⦠HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltprs_fwd_length: âL1,L2. L1 â¡* L2 â |L1| = |L2|.
+#L1 #L2 #H @(ltprs_ind ⦠H) -L2 //
+#L #L2 #_ #HL2 #IHL1
+>IHL1 -L1 >(ltpr_fwd_length ⦠HL2) -HL2 //
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma
new file mode 100644
index 000000000..7d532c973
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* alternative definition of ltprs *)
+definition ltprsa: relation lenv â lpx tprs.
+
+interpretation
+ "context-free parallel computation (environment) alternative"
+ 'PRedStarAlt L1 L2 = (ltprsa L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_ltprsa: âL1,L2. L1 â¡* L2 â L1 â¡â¡* L2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprsa_ltprs: âL1,L2. L1 â¡â¡* L2 â L1 â¡* L2.
+/2 width=1/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma
new file mode 100644
index 000000000..a7c320089
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+lemma ltprs_ldrop_conf: dropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ldrop_ltprs_trans: dedropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ltprs_ldrop_trans_O1: dropable_dx ltprs.
+/2 width=3/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma
new file mode 100644
index 000000000..e529ee31a
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltprs_strip: âL1. âL:term. L â¡* L1 â âL2. L â¡ L2 â
+ ââL0. L1 â¡ L0 & L2 â¡* L0.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem ltprs_conf: Confluent ⦠ltprs.
+/3 width=3/ qed.
+
+theorem ltprs_trans: Transitive ⦠ltprs.
+/2 width=3/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma
new file mode 100644
index 000000000..b094e66c1
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma
@@ -0,0 +1,87 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Basic_1: includes: pr1_pr0 *)
+definition tprs: relation term â TC ⦠tpr.
+
+interpretation "context-free parallel computation (term)"
+ 'PRedStar T1 T2 = (tprs T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma tprs_ind: âT1. âR:predicate term. R T1 â
+ (âT,T2. T1 â¡* T â T â¡ T2 â R T â R T2) â
+ âT2. T1 â¡* T2 â R T2.
+#T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind ⦠HT1 IHT1 ⦠HT12) //
+qed-.
+
+lemma tprs_ind_dx: âT2. âR:predicate term. R T2 â
+ (âT1,T. T1 â¡ T â T â¡* T2 â R T â R T1) â
+ âT1. T1 â¡* T2 â R T1.
+#T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx ⦠HT2 IHT2 ⦠HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tprs_refl: reflexive ⦠tprs.
+/2 width=1/ qed.
+
+lemma tprs_strap1: âT1,T,T2. T1 â¡* T â T â¡ T2 â T1 â¡* T2.
+/2 width=3/ qed.
+
+lemma tprs_strap2: âT1,T,T2. T1 â¡ T â T â¡* T2 â T1 â¡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was only: pr1_head_1 *)
+lemma tprs_pair_sn: âI,T1,T2. T1 â¡ T2 â âV1,V2. V1 â¡* V2 â
+ â¡{I} V1. T1 â¡* â¡{I} V2. T2.
+* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind ⦠H) -V2
+[1,3: /3 width=1/
+|2,4: #V #V2 #_ #HV2 #IHV1
+ @(tprs_strap1 ⦠IHV1) -IHV1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was only: pr1_head_2 *)
+lemma tprs_pair_dx: âI,V1,V2. V1 â¡ V2 â âT1,T2. T1 â¡* T2 â
+ â¡{I} V1. T1 â¡* â¡{I} V2. T2.
+* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind ⦠H) -T2
+[1,3: /3 width=1/
+|2,4: #T #T2 #_ #HT2 #IHT1
+ @(tprs_strap1 ⦠IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tprs_inv_atom1: âU2,k. âk â¡* U2 â U2 = âk.
+#U2 #k #H @(tprs_ind ⦠H) -U2 //
+#U #U2 #_ #HU2 #IHU1 destruct
+>(tpr_inv_atom1 ⦠HU2) -HU2 //
+qed-.
+
+lemma tprs_inv_cast1: âW1,T1,U2. âW1.T1 â¡* U2 â T1 â¡* U2 â¨
+ ââW2,T2. W1 â¡* W2 & T1 â¡* T2 & U2 = âW2.T2.
+#W1 #T1 #U2 #H @(tprs_ind ⦠H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (tpr_inv_cast1 ⦠HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma
new file mode 100644
index 000000000..d0d173470
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_lift.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tprs_inv_abst1: âa,V1,T1,U2. â{a}V1. T1 â¡* U2 â
+ ââV2,T2. V1 â¡* V2 & T1 â¡* T2 & U2 = â{a}V2. T2.
+#a #V1 #T1 #U2 #H @(tprs_ind ⦠H) -U2 /2 width=5/
+#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
+elim (tpr_inv_abst1 ⦠HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma tprs_inv_abst: âa,V1,V2,T1,T2. â{a}V1. T1 â¡* â{a}V2. T2 â
+ V1 â¡* V2 ⧠T1 â¡* T2.
+#a #V1 #V2 #T1 #T2 #H
+elim (tprs_inv_abst1 ⦠H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_lift: t_liftable tprs.
+/3 width=7/ qed.
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_inv_lift1: t_deliftable_sn tprs.
+/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma
new file mode 100644
index 000000000..232244510
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_tpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: pr1_strip *)
+lemma tprs_strip: âT1,T. T â¡* T1 â âT2. T â¡ T2 â
+ ââT0. T1 â¡ T0 & T2 â¡* T0.
+/3 width=3/ qed.
+
+(* Main propertis ***********************************************************)
+
+(* Basic_1: was: pr1_confluence *)
+theorem tprs_conf: Confluent ⦠tprs.
+/3 width=3/ qed.
+
+(* Basic_1: was: pr1_t *)
+theorem tprs_trans: Transitive ⦠tprs.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr1_comp *)
+lemma tprs_pair: âI,V1,V2. V1 â¡* V2 â âT1,T2. T1 â¡* T2 â
+ â¡{I} V1. T1 â¡* â¡{I} V2. T2.
+#I #V1 #V2 #H @(tprs_ind ⦠H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
+@(tprs_trans ⦠(â¡{I}V.T2)) /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
index fd3034456..1b0c88e02 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
@@ -18,59 +18,53 @@ include "basic_2/grammar/lenv_length.ma".
inductive lpx (R:relation term): relation lenv â
| lpx_stom: lpx R (â) (â)
-| lpx_pair: âK1,K2,I,V1,V2.
+| lpx_pair: âI,K1,K2,V1,V2.
lpx R K1 K2 â R V1 V2 â lpx R (K1. â{I} V1) (K2. â{I} V2)
.
-(* Basic properties *********************************************************)
-
-lemma lpx_refl: âR. reflexive ? R â reflexive ⦠(lpx R).
-#R #HR #L elim L -L // /2 width=1/
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact lpx_inv_atom1_aux: âR,L1,L2. lpx R L1 L2 â L1 = â â L2 = â.
#R #L1 #L2 * -L1 -L2
[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
]
qed-.
lemma lpx_inv_atom1: âR,L2. lpx R (â) L2 â L2 = â.
/2 width=4 by lpx_inv_atom1_aux/ qed-.
-fact lpx_inv_pair1_aux: âR,L1,L2. lpx R L1 L2 â âK1,I,V1. L1 = K1. â{I} V1 â
+fact lpx_inv_pair1_aux: âR,L1,L2. lpx R L1 L2 â âI,K1,V1. L1 = K1. â{I} V1 â
ââK2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. â{I} V2.
#R #L1 #L2 * -L1 -L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
]
qed-.
-lemma lpx_inv_pair1: âR,K1,I,V1,L2. lpx R (K1. â{I} V1) L2 â
+lemma lpx_inv_pair1: âR,I,K1,V1,L2. lpx R (K1. â{I} V1) L2 â
ââK2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. â{I} V2.
/2 width=3 by lpx_inv_pair1_aux/ qed-.
fact lpx_inv_atom2_aux: âR,L1,L2. lpx R L1 L2 â L2 = â â L1 = â.
#R #L1 #L2 * -L1 -L2
[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
]
qed-.
lemma lpx_inv_atom2: âR,L1. lpx R L1 (â) â L1 = â.
/2 width=4 by lpx_inv_atom2_aux/ qed-.
-fact lpx_inv_pair2_aux: âR,L1,L2. lpx R L1 L2 â âK2,I,V2. L2 = K2. â{I} V2 â
+fact lpx_inv_pair2_aux: âR,L1,L2. lpx R L1 L2 â âI,K2,V2. L2 = K2. â{I} V2 â
ââK1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. â{I} V1.
#R #L1 #L2 * -L1 -L2
-[ #K2 #I #V2 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
]
qed-.
-lemma lpx_inv_pair2: âR,L1,K2,I,V2. lpx R L1 (K2. â{I} V2) â
+lemma lpx_inv_pair2: âR,I,L1,K2,V2. lpx R L1 (K2. â{I} V2) â
ââK1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. â{I} V1.
/2 width=3 by lpx_inv_pair2_aux/ qed-.
@@ -79,3 +73,59 @@ lemma lpx_inv_pair2: âR,L1,K2,I,V2. lpx R L1 (K2. â{I} V2) â
lemma lpx_fwd_length: âR,L1,L2. lpx R L1 L2 â |L1| = |L2|.
#R #L1 #L2 #H elim H -L1 -L2 normalize //
qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: âR. reflexive ? R â reflexive ⦠(lpx R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
+
+lemma lpx_trans: âR. Transitive ? R â Transitive ⦠(lpx R).
+#R #HR #L1 #L #H elim H -L //
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 ⦠H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma lpx_conf: âR. Confluent ? R â Confluent ⦠(lpx R).
+#R #HR #L0 #L1 #H elim H -L1
+[ #X #H >(lpx_inv_atom1 ⦠H) -X /2 width=3/
+| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
+ elim (lpx_inv_pair1 ⦠H) -H #K2 #V2 #HK02 #HV02 #H destruct
+ elim (IHK01 ⦠HK02) -K0 #K #HK1 #HK2
+ elim (HR ⦠HV01 ⦠HV02) -HR -V0 /3 width=5/
+]
+qed.
+
+lemma lpx_TC_inj: âR,L1,L2. lpx R L1 L2 â lpx (TC ⦠R) L1 L2.
+#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+lemma lpx_TC_step: âR,L1,L. lpx (TC ⦠R) L1 L â
+ âL2. lpx R L L2 â lpx (TC ⦠R) L1 L2.
+#R #L1 #L #H elim H -L /2 width=1/
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 ⦠H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma TC_lpx_pair_dx: âR. reflexive ? R â
+ âI,K,V1,V2. TC ⦠R V1 V2 â
+ TC ⦠(lpx R) (K.â{I}V1) (K.â{I}V2).
+#R #HR #I #K #V1 #V2 #H elim H -V2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma TC_lpx_pair_sn: âR. reflexive ? R â
+ âI,V,K1,K2. TC ⦠(lpx R) K1 K2 â
+ TC ⦠(lpx R) (K1.â{I}V) (K2.â{I}V).
+#R #HR #I #V #K1 #K2 #H elim H -K2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma lpx_TC: âR,L1,L2. TC ⦠(lpx R) L1 L2 â lpx (TC ⦠R) L1 L2.
+#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/
+qed.
+
+lemma lpx_inv_TC: âR. reflexive ? R â
+ âL1,L2. lpx (TC ⦠R) L1 L2 â TC ⦠(lpx R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index b396acf55..a115260b9 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -326,6 +326,10 @@ notation "hvbox( L ⢠break term 46 T1 â¡* break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
+notation "hvbox( T1 â¡â¡* break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStarAlt $T1 $T2 }.
+
notation "hvbox( L1 ⢠â¡* break term 46 L2 )"
non associative with precedence 45
for @{ 'CPRedStar $L1 $L2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma
index aaeb2064c..4a27a6e70 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma
@@ -22,7 +22,7 @@ include "basic_2/reducibility/ltpr.ma".
theorem ltpr_conf: âL0:lenv. âL1. L0 â¡ L1 â âL2. L0 â¡ L2 â
ââL. L1 â¡ L & L2 â¡ L.
#L0 #L1 #H elim H -L0 -L1 /2 width=3/
-#K0 #K1 #I #V0 #V1 #_ #HV01 #IHK01 #L2 #H
+#I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #L2 #H
elim (ltpr_inv_pair1 ⦠H) -H #K2 #V2 #HK02 #HV02 #H destruct
elim (IHK01 ⦠HK02) -K0 #K #HK1 #HK2
elim (tpr_conf ⦠HV01 HV02) -V0 /3 width=5/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index e7353d7de..c93d3cd18 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -215,6 +215,34 @@ lemma ldrop_lsubs_ldrop2_abbr: âL1,L2,d,e. L1 â¼ [d, e] L2 â
]
qed.
+lemma dropable_sn_TC: âR. dropable_sn R â dropable_sn (TC ⦠R).
+#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
+[ #L2 #HL12
+ elim (HR ⦠HLK1 ⦠HL12) -HR -L1 /3 width=3/
+| #L #L2 #_ #HL2 * #K #HK1 #HLK
+ elim (HR ⦠HLK ⦠HL2) -HR -L /3 width=3/
+]
+qed.
+
+lemma dedropable_sn_TC: âR. dedropable_sn R â dedropable_sn (TC ⦠R).
+#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12
+ elim (HR ⦠HLK1 ⦠HK12) -HR -K1 /3 width=3/
+| #K #K2 #_ #HK2 * #L #HL1 #HLK
+ elim (HR ⦠HLK ⦠HK2) -HR -K /3 width=3/
+]
+qed.
+
+lemma dropable_dx_TC: âR. dropable_dx R â dropable_dx (TC ⦠R).
+#R #HR #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #K2 #e #HLK2
+ elim (HR ⦠HL12 ⦠HLK2) -HR -L2 /3 width=3/
+| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
+ elim (HR ⦠HL2 ⦠HLK2) -HR -L2 #K #HLK #HK2
+ elim (IHL1 ⦠HLK) -L /3 width=5/
+]
+qed.
+
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: drop_S *)
diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma
index 18f028acc..3517eff98 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma
@@ -20,6 +20,13 @@ include "ground_2/notation.ma".
definition Decidable: Prop â Prop â λR. R ⨠(R â â¥).
+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.
+
+definition Transitive: âA. âR: relation A. Prop â λA,R.
+ âa1,a0. R a1 a0 â âa2. R a0 a2 â R a1 a2.
+
definition confluent2: âA. âR1,R2: relation A. Prop â λA,R1,R2.
âa0,a1. R1 a0 a1 â âa2. R2 a0 a2 â
ââa. R2 a1 a & R1 a2 a.