From 09af7a9751464291ec3f32fb80c92fe1accdbf88 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 21 Apr 2013 15:51:01 +0000 Subject: [PATCH] - we commit the "reduction" component - we park the focalized reduction for the moment - some refactoring --- .../cnf_cif.ma => etc/cpr/cnf_cif.etc} | 0 .../cpr_aaa.ma => etc/cpr/cpr_aaa.etc} | 0 .../cpr_cpr.ma => etc/cpr/cpr_cpr.etc} | 0 .../cpr_ltpr.ma => etc/cpr/cpr_ltpr.etc} | 0 .../cpr/cpr_ltpss_dx.etc} | 0 .../cpr/cpr_ltpss_sn.etc} | 0 .../cpr_tpss.ma => etc/cpr/cpr_tpss.etc} | 0 .../lfpr.ma => etc/cpr/lfpr.etc} | 4 + .../lfpr_aaa.ma => etc/cpr/lfpr_aaa.etc} | 0 .../lfpr_cpr.ma => etc/cpr/lfpr_cpr.etc} | 0 .../lfpr_lfpr.ma => etc/cpr/lfpr_lfpr.etc} | 0 .../ltpr_aaa.ma => etc/cpr/ltpr_aaa.etc} | 0 .../cpr/ltpr_ltpss_dx.etc} | 0 .../cpr/ltpr_ltpss_sn.etc} | 0 .../ltpr_tps.ma => etc/cpr/ltpr_tps.etc} | 0 .../ltpr_tpss.ma => etc/cpr/ltpr_tpss.etc} | 0 .../delift/cpr_delift.etc} | 0 .../lambdadelta/basic_2/etc/delift/delift.etc | 4 + .../basic_2/etc/delift/delift_alt.etc | 4 + .../lambdadelta/basic_2/etc/delift/thin.etc | 4 + .../delift/tpr_delift.etc} | 0 .../cfpr.ma => etc/fpr/cfpr.etc} | 4 + .../cfpr_aaa.ma => etc/fpr/cfpr_aaa.etc} | 0 .../cfpr_cfpr.ma => etc/fpr/cfpr_cfpr.etc} | 0 .../cfpr_cpr.ma => etc/fpr/cfpr_cpr.etc} | 0 .../cfpr_ltpss.ma => etc/fpr/cfpr_ltpss.etc} | 0 .../{reducibility/fpr.ma => etc/fpr/fpr.etc} | 4 + .../fpr_cpr.ma => etc/fpr/fpr_cpr.etc} | 0 .../fpr_fpr.ma => etc/fpr/fpr_fpr.etc} | 0 .../lfpr_alt.ma => etc/fpr/lfpr_alt.etc} | 8 + .../lfpr_fpr.ma => etc/fpr/lfpr_fpr.etc} | 0 .../basic_2/reducibility/cnf_lift.ma | 85 ----- .../lambdadelta/basic_2/reducibility/cpr.ma | 111 ------ .../basic_2/reducibility/cpr_lift.ma | 180 --------- .../lambdadelta/basic_2/reducibility/ltpr.ma | 67 ---- .../basic_2/reducibility/ltpr_ldrop.ma | 45 --- .../lambdadelta/basic_2/reducibility/tpr.ma | 238 ------------ .../basic_2/reducibility/tpr_lift.ma | 121 ------ .../basic_2/reducibility/tpr_tpr.ma | 261 ------------- .../{reducibility => reduction}/cif.ma | 2 +- .../{reducibility => reduction}/cif_append.ma | 4 +- .../{reducibility => reduction}/cnf.ma | 59 ++- .../lambdadelta/basic_2/reduction/cnf_cif.ma | 28 ++ .../lambdadelta/basic_2/reduction/cnf_crf.ma | 46 +++ .../lambdadelta/basic_2/reduction/cnf_lift.ma | 47 +++ .../lambdadelta/basic_2/reduction/cpr.ma | 339 +++++++++++++++++ .../lambdadelta/basic_2/reduction/cpr_cif.ma | 52 +++ .../lambdadelta/basic_2/reduction/cpr_lift.ma | 106 ++++++ .../thnf.ma => reduction/cpr_tshf.ma} | 60 ++- .../{reducibility => reduction}/crf.ma | 26 +- .../{reducibility => reduction}/crf_append.ma | 4 +- .../lambdadelta/basic_2/reduction/lpr.ma | 77 ++++ .../lambdadelta/basic_2/reduction/lpr_aaa.ma | 72 ++++ .../lambdadelta/basic_2/reduction/lpr_cpr.ma | 355 ++++++++++++++++++ .../lambdadelta/basic_2/reduction/lpr_cpss.ma | 270 +++++++++++++ .../basic_2/reduction/lpr_ldrop.ma | 32 ++ .../ltpr_ltpr.ma => reduction/lpr_lpr.ma} | 16 +- .../lambdadelta/basic_2/reduction/lpr_lpss.ma | 23 ++ .../{reducibility => reduction}/xpr.ma | 10 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 41 +- 60 files changed, 1584 insertions(+), 1225 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cnf_cif.ma => etc/cpr/cnf_cif.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_aaa.ma => etc/cpr/cpr_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_cpr.ma => etc/cpr/cpr_cpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_ltpr.ma => etc/cpr/cpr_ltpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_ltpss_dx.ma => etc/cpr/cpr_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_ltpss_sn.ma => etc/cpr/cpr_ltpss_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_tpss.ma => etc/cpr/cpr_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr.ma => etc/cpr/lfpr.etc} (93%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr_aaa.ma => etc/cpr/lfpr_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr_cpr.ma => etc/cpr/lfpr_cpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr_lfpr.ma => etc/cpr/lfpr_lfpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_aaa.ma => etc/cpr/ltpr_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_ltpss_dx.ma => etc/cpr/ltpr_ltpss_dx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_ltpss_sn.ma => etc/cpr/ltpr_ltpss_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_tps.ma => etc/cpr/ltpr_tps.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_tpss.ma => etc/cpr/ltpr_tpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cpr_delift.ma => etc/delift/cpr_delift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/tpr_delift.ma => etc/delift/tpr_delift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cfpr.ma => etc/fpr/cfpr.etc} (92%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cfpr_aaa.ma => etc/fpr/cfpr_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cfpr_cfpr.ma => etc/fpr/cfpr_cfpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cfpr_cpr.ma => etc/fpr/cfpr_cpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/cfpr_ltpss.ma => etc/fpr/cfpr_ltpss.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/fpr.ma => etc/fpr/fpr.etc} (94%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/fpr_cpr.ma => etc/fpr/fpr_cpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/fpr_fpr.ma => etc/fpr/fpr_fpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr_alt.ma => etc/fpr/lfpr_alt.etc} (92%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/lfpr_fpr.ma => etc/fpr/lfpr_fpr.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/cif.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/cif_append.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/cnf.ma (60%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/thnf.ma => reduction/cpr_tshf.ma} (58%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/crf.ma (90%) rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/crf_append.ma (96%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/ltpr_ltpr.ma => reduction/lpr_lpr.ma} (68%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma rename matita/matita/contribs/lambdadelta/basic_2/{reducibility => reduction}/xpr.ma (93%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cnf_cif.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cnf_cif.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_cpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_cpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpss_dx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpss_dx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpss_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_ltpss_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_tpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_tpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr.etc similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr.etc index 44745490e..ea9f585a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ break ⦃ term 46 L2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L1 $L2 }. + include "basic_2/unfold/ltpss_sn.ma". include "basic_2/reducibility/ltpr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_cpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_cpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_lfpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfpr_lfpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpss_dx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpss_dx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpss_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpss_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_tps.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_tps.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_tpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_tpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpr_delift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpr_delift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc index 3cd3241bc..eda839607 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'TSubst $L $T1 $d $e $T2 }. + include "basic_2/unfold/tpss.ma". (* INVERSE BASIC TERM RELOCATION *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc index b9322cd1e..e22911032 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'TSubstAlt $L $T1 $d $e $T2 }. + include "basic_2/unfold/delift_lift.ma". (* INVERSE BASIC TERM RELOCATION *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc index 65fb76fe0..f92cd543a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'TSubst $T1 $d $e $T2 }. + include "basic_2/unfold/ltpss_sn.ma". (* BASIC LOCAL ENVIRONMENT THINNING *****************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/tpr_delift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/tpr_delift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr.etc similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr.etc index e1e3c4386..f58a52c37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }. + include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/fpr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_cfpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_cfpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_cpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_cpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/cfpr_ltpss.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr.etc similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr.etc index 391061565..3bb168f9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }. + include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr_cpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr_cpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr_fpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpr_fpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfpr_alt.etc similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfpr_alt.etc index adff7ad07..95ec60ba2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfpr_alt.etc @@ -12,6 +12,14 @@ (* *) (**************************************************************************) +notation "hvbox( L1 ⊢ ➡ ➡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnAlt $L1 $L2 }. + +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRedAlt $L1 $L2 }. + include "basic_2/grammar/lenv_px_bi.ma". include "basic_2/reducibility/fpr_cpr.ma". include "basic_2/reducibility/lfpr_fpr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfpr_fpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfpr_fpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma deleted file mode 100644 index 0e1a8551f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma +++ /dev/null @@ -1,85 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reducibility/cpr_lift.ma". -include "basic_2/reducibility/cpr_cpr.ma". -include "basic_2/reducibility/cnf.ma". - -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) - -(* Advanced inversion lemmas ************************************************) - -lemma cnf_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥. -#L #K #V #i #HLK #H -elim (lift_total V 0 (i+1)) #W #HVW -lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct -elim (lift_inv_lref2_be … HVW ? ?) -HVW // -qed-. - -lemma cnf_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄. -#a #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // -] -qed-. - -lemma cnf_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄. -#L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // -] -qed-. - -(* Advanced properties ******************************************************) - -(* Basic_1: was only: nf2_csort_lref *) -lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄. -#L #i #HLK #X #H -elim (cpr_inv_lref1 … H) // * -#K0 #V0 #V1 #HLK0 #_ #_ #_ -lapply (ldrop_mono … HLK … HLK0) -L #H destruct -qed. - -(* Basic_1: was: nf2_lref_abst *) -lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄. -#L #K #V #i #HLK #X #H -elim (cpr_inv_lref1 … H) // * -#K0 #V0 #V1 #HLK0 #_ #_ #_ -lapply (ldrop_mono … HLK … HLK0) -L #H destruct -qed. - -(* Basic_1: was: nf2_abst *) -lemma cnf_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄. -#a #I #L #V #W #T #HW #HT #X #H -elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct ->(HW … HW0) -W0 >(HT … HT0) -T0 // -qed. - -(* Basic_1: was only: nf2_appl_lref *) -lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄. -#L #V #T #HV #HT #HS #X #H -elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct ->(HV … HV0) -V0 >(HT … HT0) -T0 // -qed. - -(* Relocation properties ****************************************************) - -(* Basic_1: was: nf2_lift *) -lemma cnf_lift: ∀L0,L,T,T0,d,e. - L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. -#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H -elim (cpr_inv_lift1 … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1 -<(HLT … HT1) in HT0; -L #HT0 ->(lift_mono … HT10 … HT0) -T1 -X // -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma deleted file mode 100644 index d82299c38..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma +++ /dev/null @@ -1,111 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/tpss.ma". -include "basic_2/reducibility/tpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) - -(* Basic_1: includes: pr2_delta1 *) -definition cpr: lenv → relation term ≝ - λ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_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2. -/3 width=5/ qed-. - -(* Basic_1: was by definition: pr2_free *) -lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2. -/2 width=3/ qed. - -lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ➡ T2. -/3 width=5/ qed. - -lemma cpr_refl: ∀L,T. L ⊢ T ➡ T. -/2 width=1/ qed. - -(* 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/ -qed. - -lemma cpr_cast: ∀L,V,T1,T2. - L ⊢ T1 ➡ T2 → L ⊢ ⓝV. T1 ➡ T2. -#L #V #T1 #T2 * /3 width=3/ -qed. - -(* Note: it does not hold replacing |L1| with |L2| *) -(* Basic_1: was only: pr2_change *) -lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → - ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. -#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 -lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/ -qed. - -(* Basic inversion lemmas ***************************************************) - -(* Basic_1: was: pr2_gen_csort *) -lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ➡ T2 → T1 ➡ T2. -#T1 #T2 * #T #HT normalize #HT2 -<(tpss_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 ->(tpss_inv_sort1 … H) -H // -qed-. - -(* Basic_1: was: pr2_gen_cast *) -lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝV1. T1 ➡ U2 → ( - ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 & - U2 = ⓝV2. T2 - ) ∨ L ⊢ T1 ➡ U2. -#L #V1 #T1 #U2 * #X #H #HU2 -elim (tpr_inv_cast1 … H) -H /3 width=3/ -* #V #T #HV1 #HT1 #H destruct -elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma cpr_fwd_bind1_minus: ∀I,L,V1,T1,T. L ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b. - ∃∃V2,T2. L ⊢ ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 & - T = -ⓑ{I}V2.T2. -#I #L #V1 #T1 #T * #X #H1 #H2 #b -elim (tpr_fwd_bind1_minus … H1 b) -H1 #V0 #T0 #HT10 #H destruct -elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ -qed-. - -lemma cpr_fwd_shift1: ∀L,L1,T1,T. L ⊢ L1 @@ T1 ➡ T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#L #L1 #T1 #T * #X #H1 #H2 -elim (tpr_fwd_shift1 … H1) -H1 #L0 #T0 #HL10 #H destruct -elim (tpss_fwd_shift1 … H2) -H2 #L2 #T2 #HL02 #H destruct /2 width=4/ -qed-. - -(* Basic_1: removed theorems 6: - pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans - pr2_gen_ctail pr2_ctail - Basic_1: removed local theorems 3: - pr2_free_free pr2_free_delta pr2_delta_delta -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma deleted file mode 100644 index 0a7afddab..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma +++ /dev/null @@ -1,180 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/tpss_lift.ma". -include "basic_2/reducibility/tpr_lift.ma". -include "basic_2/reducibility/cpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) - -(* Advanced properties ******************************************************) - -lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. - ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▶* [0, |L| - i - 1] W1 → - ⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2. -#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 -lapply (ldrop_fwd_ldrop2_length … HLK) #Hi -@ex2_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *) -qed. - -lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡ T2 → - ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡ ⓑ{a,I}V2. T2. -#L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a #I -lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02 -lapply (tpss_lsubr_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 -@(ex2_intro … (ⓑ{a,I}V0.T0)) /2 width=1/ (* explicit constructors *) -qed. - -lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2. - L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2. -#a #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2 -lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2 -lapply (tpss_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 -@(ex2_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *) -qed. - -lemma cpr_beta_dx: ∀a,L,V1,V2,W,T1,T2. - V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2. -/3 width=1/ qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was: pr2_gen_lref *) -lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 → - T2 = #i ∨ - ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 ▶* [0, |L| - i - 1] T1 & - ⇧[0, i + 1] T1 ≡ T2 & - i < |L|. -#L #T2 #i * #X #H ->(tpr_inv_atom1 … H) -H #H -elim (tpss_inv_lref1 … H) -H /2 width=1/ -* /3 width=6/ -qed-. - -(* Basic_1: was pr2_gen_abbr *) -lemma cpr_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡ U2 → - (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 & - L. ⓓV ⊢ T1 ➡ T2 & - U2 = ⓓ{a}V2. T2 - ) ∨ - ∃∃T2. L.ⓓV1 ⊢ T1 ➡ T2 & ⇧[0,1] U2 ≡ T2 & a = true. -#a #L #V1 #T1 #Y * #X #H1 #H2 -elim (tpr_inv_abbr1 … H1) -H1 * -[ #V #T #T0 #HV1 #HT1 #HT0 #H destruct - elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct - lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0 - lapply (tps_weak_full … HT0) -HT0 #HT0 - lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02 - lapply (tpss_weak_full … HT02) -HT02 #HT02 - lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/ -| #T2 #HT12 #HXT2 #H destruct - elim (lift_total Y 0 1) #Z #HYZ - lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H - lapply (cpr_intro … HT12 … H) -T2 /3 width=3/ -] -qed-. - -(* Basic_1: was: pr2_gen_abst *) -lemma cpr_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡ U2 → ∀I,W. - ∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛ{a}V2. T2. -#a #L #V1 #T1 #Y * #X #H1 #H2 #I #W -elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct -elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct -lapply (tpss_lsubr_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/ -qed-. - -(* Basic_1: was pr2_gen_appl *) -lemma cpr_inv_appl1: ∀L,V1,U0,U2. L ⊢ ⓐV1. U0 ➡ U2 → - ∨∨ ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ U0 ➡ T2 & - U2 = ⓐV2. T2 - | ∃∃a,V2,W,T1,T2. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 & - U0 = ⓛ{a}W. T1 & - U2 = ⓓ{a}V2. T2 - | ∃∃a,V2,V,W1,W2,T1,T2. L ⊢ V1 ➡ V2 & L ⊢ W1 ➡ W2 & L. ⓓW2 ⊢ T1 ➡ T2 & - ⇧[0,1] V2 ≡ V & - U0 = ⓓ{a}W1. T1 & - U2 = ⓓ{a}W2. ⓐV. T2. -#L #V1 #U0 #Y * #X #H1 #H2 -elim (tpr_inv_appl1 … H1) -H1 * -[ #V #U #HV1 #HU0 #H destruct - elim (tpss_inv_flat1 … H2) -H2 #V2 #U2 #HV2 #HU2 #H destruct /4 width=5/ -| #a #V #W #T0 #T #HV1 #HT0 #H #H1 destruct - elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct - lapply (tpss_weak … HT2 0 (|L|+1) ? ?) -HT2 // /4 width=9/ -| #a #V0 #V #W #W0 #T #T0 #HV10 #HW0 #HT0 #HV0 #H #H1 destruct - elim (tpss_inv_bind1 … H2) -H2 #W2 #X #HW02 #HX #HY destruct - elim (tpss_inv_flat1 … HX) -HX #V2 #T2 #HV2 #HT2 #H destruct - elim (tpss_inv_lift1_ge … HV2 … HV0 ?) -V // [3: /2 width=1/ |2: skip ] #V shift_append_assoc normalize #H - elim (tpr_inv_bind1 … H) -H * - [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct - elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct - elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct - >append_length >HL1 >HL2 -L1 -L - @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) - | #T #_ #_ #H destruct - ] -] -qed-. - -(* Basic_1: removed theorems 3: - pr0_subst0_back pr0_subst0_fwd pr0_subst0 -*) -(* Basic_1: removed local theorems: 1: pr0_delta_tau *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma deleted file mode 100644 index 8d6b0363a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma +++ /dev/null @@ -1,121 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/tps_lift.ma". -include "basic_2/reducibility/tpr.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Relocation properties ****************************************************) - -(* Basic_1: was: pr0_lift *) -lemma tpr_lift: t_liftable tpr. -#T1 #T2 #H elim H -T1 -T2 -[ * #i #U1 #d #e #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct - [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct // - | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct // - | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct // - ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct - elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/ -| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/ -| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X1 #d #e #HX1 #X2 #HX2 - elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct - elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct - elim (lift_total T (d + 1) e) #U #HTU - @tpr_delta - [4: @(tps_lift_le … HT2 … HTU HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *) -| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct - elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/ -| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #H #U2 #HTU2 - elim (lift_inv_bind1 … H) -H #V3 #T3 #_ #HT13 #H destruct -V - elim (lift_conf_O1 … HTU2 … HT2) -T2 /3 width=4/ -| #V #T1 #T2 #_ #IHT12 #X #d #e #HX #T #HT2 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/ -] -qed. - -(* Basic_1: was: pr0_gen_lift *) -lemma tpr_inv_lift1: t_deliftable_sn tpr. -#T1 #T2 #H elim H -T1 -T2 -[ * #i #X #d #e #HX - [ lapply (lift_inv_sort2 … HX) -HX #H destruct /2 width=3/ - | lapply (lift_inv_lref2 … HX) -HX * * #Hid #H destruct /3 width=3/ - | lapply (lift_inv_gref2 … HX) -HX #H destruct /2 width=3/ - ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct - elim (IHV12 … HV01) -V1 - elim (IHT12 … HT01) -T1 /3 width=5/ -| #a #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct - elim (IHV12 … HV01) -V1 - elim (IHT12 … HT01) -T1 /3 width=5/ -| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X #d #e #HX - elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct - elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12 - elim (IHT1 … HUT1) -T1 #U #HUT #HU1 - elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2 - @ex2_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *) -| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X #d #e #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct - elim (IHV12 … HV01) -V1 #V3 #HV32 #HV03 - elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03 - elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03 - elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2 - @ex2_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *) -| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #HX - elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct - elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31 - elim (lift_div_le … HT2 … HT1 ?) -T // /3 width=5/ -| #V #T1 #T2 #_ #IHT12 #X #d #e #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct - elim (IHT12 … HT01) -T1 /3 width=3/ -] -qed-. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was pr0_gen_abst *) -lemma tpr_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 elim (tpr_inv_bind1 … H) -H * -[ #V2 #T #T2 #HV12 #HT1 #HT2 - lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /2 width=5/ -| #T2 #_ #_ #_ #H destruct -] -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma tpr_fwd_abst1: ∀a,V1,T1,U2. ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W. - ∃∃V2,T2. ⓑ{b,I}W.T1 ➡ ⓑ{b,I}W.T2 & - U2 = ⓛ{a}V2.T2. -#a #V1 #T1 #U2 #H #b #I #W elim (tpr_inv_bind1 … H) -H * -[ #V2 #T #T2 #HV12 #HT1 #HT2 - lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /3 width=4/ -| #T2 #_ #_ #_ #H destruct -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma deleted file mode 100644 index a733345bf..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma +++ /dev/null @@ -1,261 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reducibility/ltpr_tpss.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) - -(* Confluence lemmas ********************************************************) - -fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X. -/2 width=3/ qed. - -fact tpr_conf_flat_flat: - ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → - ∃∃T0. ⓕ{I} V1. T1 ➡ T0 & ⓕ{I} V2. T2 ➡ T0. -#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/ -qed. - -fact tpr_conf_flat_beta: - ∀a,V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → - U0 ➡ T2 → ⓛ{a}W0. U0 ➡ T1 → - ∃∃X. ⓐV1. T1 ➡ X & ⓓ{a}V2. T2 ➡ X. -#a #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H -elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 -elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/ -qed. - -(* Basic-1: was: - pr0_cong_upsilon_refl pr0_cong_upsilon_zeta - pr0_cong_upsilon_cong pr0_cong_upsilon_delta -*) -fact tpr_conf_flat_theta: - ∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → ⇧[O,1] V2 ≡ V → - W0 ➡ W2 → U0 ➡ U2 → ⓓ{a}W0. U0 ➡ T1 → - ∃∃X. ⓐV1. T1 ➡ X & ⓓ{a}W2. ⓐV. U2 ➡ X. -#a #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H -elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2 -elim (lift_total VV 0 1) #VVV #HVV -lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV -elim (tpr_inv_abbr1 … H) -H * -(* case 1: delta *) -[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct - elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2 - elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2 - elim (tpr_tps_conf_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 - @ex2_intro - [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] - |1:skip - |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/ - ] (**) (* /5 width=14/ is too slow *) -(* case 3: zeta *) -| -HV2 -HW02 -HVV2 #U1 #HU01 #HTU1 - elim (IH … HU01 … HU02) -HU01 -HU02 -IH // -U0 #U #HU1 #HU2 - elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #UU #HUU #HT1UU #H destruct - @(ex2_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *) -] -qed. - -fact tpr_conf_flat_cast: - ∀X2,V0,V1,T0,T1. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 → - ∃∃X. ⓝV1. T1 ➡ X & X2 ➡ X. -#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/ -qed. - -fact tpr_conf_beta_beta: - ∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → - ∃∃X. ⓓ{a}V1. T1 ➡X & ⓓ{a}V2. T2 ➡ X. -#a #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ -elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/ -qed. - -(* Basic_1: was: pr0_cong_delta pr0_delta_delta *) -fact tpr_conf_delta_delta: - ∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → - ⋆. ⓑ{I1} V1 ⊢ T1 ▶ [O, 1] TT1 → - ⋆. ⓑ{I1} V2 ⊢ T2 ▶ [O, 1] TT2 → - ∃∃X. ⓑ{a,I1} V1. TT1 ➡ X & ⓑ{a,I1} V2. TT2 ➡ X. -#a #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 -elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 -elim (tpr_tps_conf_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1 -elim (tpr_tps_conf_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2 -elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2 -@ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) -qed. - -fact tpr_conf_delta_zeta: - ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 → - T0 ➡ T2 → ⇧[O, 1] X2 ≡ T2 → - ∃∃X. +ⓓV1. TT1 ➡ X & X2 ➡ X. -#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2 -elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2 -elim (tpr_tps_conf_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT -elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2 -lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/ -qed. - -(* Basic_1: was: pr0_upsilon_upsilon *) -fact tpr_conf_theta_theta: - ∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - V0 ➡ V1 → V0 ➡ V2 → W0 ➡ W1 → W0 ➡ W2 → T0 ➡ T1 → T0 ➡ T2 → - ⇧[O, 1] V1 ≡ VV1 → ⇧[O, 1] V2 ≡ VV2 → - ∃∃X. ⓓ{a}W1. ⓐVV1. T1 ➡ X & ⓓ{a}W2. ⓐVV2. T2 ➡ X. -#a #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 -elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 -elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ #T #HT1 #HT2 -elim (lift_total V 0 1) #VV #HVV -lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1 -lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2 -@ex2_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) -qed. - -fact tpr_conf_zeta_zeta: - ∀V0:term. ∀X2,TT0,T0,T1,TT2. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{TT0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - TT0 ➡ T0 → ⇧[O, 1] T1 ≡ T0 → - TT0 ➡ TT2 → ⇧[O, 1] X2 ≡ TT2 → - ∃∃X. T1 ➡ X & X2 ➡ X. -#V0 #X2 #TT0 #T0 #T1 #TT2 #IH #HTT0 #HT10 #HTT02 #HXTT2 -elim (IH … HTT0 … HTT02) -IH -HTT0 -HTT02 // -V0 -TT0 #T #HT0 #HTT2 -elim (tpr_inv_lift1 … HT0 … HT10) -T0 #T0 #HT0 #HT10 -elim (tpr_inv_lift1 … HTT2 … HXTT2) -TT2 #TT2 #HTT2 #HXTT2 -lapply (lift_inj … HTT2 … HT0) -HTT2 #H destruct /2 width=3/ -qed. - -fact tpr_conf_tau_tau: - ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - T0 ➡ T1 → T0 ➡ X2 → - ∃∃X. T1 ➡ X & X2 ➡ X. -#V0 #T0 #X2 #T1 #IH #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /2 width=3/ -qed. - -(* Confluence ***************************************************************) - -(* Basic_1: was: pr0_confluence *) -theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → - ∃∃T. T1 ➡ T & T2 ➡ T. -#T0 @(f_ind … tw … T0) -T0 #n #IH * -[ #I #_ #X1 #X2 #H1 #H2 -n - >(tpr_inv_atom1 … H1) -X1 - >(tpr_inv_atom1 … H2) -X2 -(* case 1: atom, atom *) - // -| * [ #a ] #I #V0 #T0 #Hn #X1 #X2 #H1 #H2 - [ elim (tpr_inv_bind1 … H1) -H1 * - [ #V1 #T1 #U1 #HV01 #HT01 #HTU1 #H1 - | #T1 #HT01 #HXT1 #H11 #H12 - ] - elim (tpr_inv_bind1 … H2) -H2 * - [1,3: #V2 #T2 #U2 #HV02 #HT02 #HTU2 #H2 - |2,4: #T2 #HT02 #HXT2 #H21 #H22 - ] destruct -(* case 2: delta, delta *) - [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) -(* case 3: zeta, delta (repeated) *) - | @ex2_commute /3 width=10 by tpr_conf_delta_zeta/ -(* case 4: delta, zeta *) - | /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) -(* case 5: zeta, zeta *) - | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) - ] - | elim (tpr_inv_flat1 … H1) -H1 * - [ #V1 #T1 #HV01 #HT01 #H1 - | #b1 #V1 #W1 #U1 #T1 #HV01 #HUT1 #H11 #H12 #H13 - | #b1 #V1 #Y1 #W1 #Z1 #U1 #T1 #HV01 #HWZ1 #HUT1 #HVY1 #H11 #H12 #H13 - | #HX1 #H1 - ] - elim (tpr_inv_flat1 … H2) -H2 * - [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2 - |2,6,10,14: #b2 #V2 #W2 #U2 #T2 #HV02 #HUT2 #H21 #H22 #H23 - |3,7,11,15: #b2 #V2 #Y2 #W2 #Z2 #U2 #T2 #HV02 #HWZ2 #HUT2 #HVY2 #H21 #H22 #H23 - |4,8,12,16: #HX2 #H2 - ] destruct -(* case 6: flat, flat *) - [ /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) -(* case 7: beta, flat (repeated) *) - | @ex2_commute /3 width=8 by tpr_conf_flat_beta/ -(* case 8: theta, flat (repeated) *) - | @ex2_commute /3 width=11 by tpr_conf_flat_theta/ -(* case 9: tau, flat (repeated) *) - | @ex2_commute /3 width=6 by tpr_conf_flat_cast/ -(* case 10: flat, beta *) - | /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) -(* case 11: beta, beta *) - | /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) -(* case 12: flat, theta *) - | /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) -(* case 13: theta, theta *) - | /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) -(* case 14: flat, tau *) - | /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) -(* case 15: tau, tau *) - | /3 width=5 by tpr_conf_tau_tau/ - ] - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma index 0a536a914..dea2fedab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/crf.ma". +include "basic_2/reduction/crf.ma". (* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma index 45fd178cf..b5a92cbc3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cif_append.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/crf_append.ma". -include "basic_2/reducibility/cif.ma". +include "basic_2/reduction/crf_append.ma". +include "basic_2/reduction/cif.ma". (* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf.ma similarity index 60% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/cnf.ma index 02bbcf87a..290a08a26 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr.ma". +include "basic_2/reduction/cpr.ma". (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) @@ -24,6 +24,38 @@ interpretation (* Basic inversion lemmas ***************************************************) +lemma cnf_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥. +#L #K #V #i #HLK #H +elim (lift_total V 0 (i+1)) #W #HVW +lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct +elim (lift_inv_lref2_be … HVW ? ?) -HVW // +qed-. + +lemma cnf_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄. +#a #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnf_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄. +#L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // +] +qed-. + +lemma cnf_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥. +#L #V #T #H elim (is_lift_dec T 0 1) +[ * #U #HTU + lapply (H U ?) -H /2 width=3/ #H destruct + elim (lift_inv_pair_xy_y … HTU) +| #HT + elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12 + lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/ +] +qed-. + lemma cnf_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄. #L #V1 #T1 #HVT1 @and3_intro [ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // @@ -35,17 +67,6 @@ lemma cnf_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V ] qed-. -lemma cnf_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥. -#L #V #T #H elim (is_lift_dec T 0 1) -[ * #U #HTU - lapply (H U ?) -H /3 width=3 by cpr_tpr, tpr_zeta/ #H destruct (**) (* auto too slow without trace *) - elim (lift_inv_pair_xy_y … HTU) -| #HT - elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12 - lapply (H (+ⓓV.T2) ?) -H /3 width=3 by cpr_tpr, tpr_delta/ -HT2 #H destruct /3 width=2/ (**) (* auto too slow without trace *) -] -qed. - lemma cnf_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥. #L #V #T #H lapply (H T ?) -H /2 width=1/ #H @discr_tpair_xy_y // @@ -59,6 +80,20 @@ lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄. >(cpr_inv_sort1 … H) // qed. +(* Basic_1: was: nf2_abst *) +lemma cnf_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄. +#a #I #L #V #W #T #HW #HT #X #H +elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct +>(HW … HW0) -W0 >(HT … HT0) -T0 // +qed. + +(* Basic_1: was only: nf2_appl_lref *) +lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄. +#L #V #T #HV #HT #HS #X #H +elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct +>(HV … HV0) -V0 >(HT … HT0) -T0 // +qed. + (* Basic_1: was: nf2_dec *) axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨ ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma new file mode 100644 index 000000000..e87cdb962 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_cif.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_cif.ma". +include "basic_2/reduction/cnf_crf.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Main properties on context-sensitive irreducible terms *******************) + +theorem cif_cnf: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄. +/2 width=3 by cpr_fwd_cif/ qed. + +(* Main inversion lemmas on context-sensitive irreducible terms *************) + +theorem cnf_inv_cif: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄. +/2 width=4 by cnf_inv_crf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma new file mode 100644 index 000000000..0afff1ab0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_crf.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crf.ma". +include "basic_2/reduction/cnf.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Advanced inversion lemmas on context-sensitive reducible terms ***********) + +(* Note: this property is unusual *) +lemma cnf_inv_crf: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥. +#L #T #H elim H -L -T +[ #L #K #V #i #HLK #H + elim (cnf_inv_delta … HLK H) +| #L #V #T #_ #IHV #H + elim (cnf_inv_appl … H) -H /2 width=1/ +| #L #V #T #_ #IHT #H + elim (cnf_inv_appl … H) -H /2 width=1/ +| #I #L #V #T * #H1 #H2 destruct + [ elim (cnf_inv_zeta … H2) + | elim (cnf_inv_tau … H2) + ] +|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct + [1,3: elim (cnf_inv_abbr … H2) -H2 /2 width=1/ + |*: elim (cnf_inv_abst … H2) -H2 /2 width=1/ + ] +| #a #L #V #W #T #H + elim (cnf_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #L #V #W #T #H + elim (cnf_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma new file mode 100644 index 000000000..acbb020ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnf_lift.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_lift.ma". +include "basic_2/reduction/cnf.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: nf2_csort_lref *) +lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄. +#L #i #HL #X #H +elim (cpr_inv_lref1 … H) -H // * +#K #V1 #V2 #HLK #_ #_ +lapply (ldrop_mono … HL … HLK) -L #H destruct +qed. + +(* Basic_1: was: nf2_lref_abst *) +lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄. +#L #K #V #i #HLK #X #H +elim (cpr_inv_lref1 … H) -H // * +#K0 #V1 #V2 #HLK0 #_ #_ +lapply (ldrop_mono … HLK … HLK0) -L #H destruct +qed. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: nf2_lift *) +lemma cnf_lift: ∀L0,L,T,T0,d,e. + L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. +#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H +elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 +<(HLT … HT1) in HT0; -L #HT0 +>(lift_mono … HT10 … HT0) -T1 -X // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma new file mode 100644 index 000000000..e6ad7b2ba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -0,0 +1,339 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/cpqs.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx pr2_head_1 *) +(* Note: cpr_flat: does not hold in basic_1 *) +inductive cpr: lenv → relation term ≝ +| cpr_atom : ∀I,L. cpr L (⓪{I}) (⓪{I}) +| cpr_delta: ∀L,K,V,V2,W2,i. + ⇩[0, i] L ≡ K. ⓓV → cpr K V V2 → + ⇧[0, i + 1] V2 ≡ W2 → cpr L (#i) W2 +| cpr_bind : ∀a,I,L,V1,V2,T1,T2. + cpr L V1 V2 → cpr (L. ⓑ{I} V1) T1 T2 → + cpr L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) +| cpr_flat : ∀I,L,V1,V2,T1,T2. + cpr L V1 V2 → cpr L T1 T2 → + cpr L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) +| cpr_zeta : ∀L,V,T1,T,T2. cpr (L.ⓓV) T1 T → + ⇧[0, 1] T2 ≡ T → cpr L (+ⓓV. T1) T2 +| cpr_tau : ∀L,V,T1,T2. cpr L T1 T2 → cpr L (ⓝV. T1) T2 +| cpr_beta : ∀a,L,V1,V2,W,T1,T2. + cpr L V1 V2 → cpr (L.ⓛW) T1 T2 → + cpr L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2) +| cpr_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2. + cpr L V1 V → ⇧[0, 1] V ≡ V2 → cpr L W1 W2 → cpr (L.ⓓW1) T1 T2 → + cpr L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2) +. + +interpretation "context-sensitive parallel reduction (term)" + 'PRed L T1 T2 = (cpr L T1 T2). + +(* Basic properties *********************************************************) + +(* Note: it does not hold replacing |L1| with |L2| *) +lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. +#L1 #T1 #T2 #H elim H -L1 -T1 -T2 +[ // +| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi + lapply (ldrop_fwd_O1_length … HLK1) #H2i + elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi + shift_append_assoc normalize #H + elim (cpr_inv_bind1 … H) -H * + [ #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) + | #T #_ #_ #H destruct + ] +] +qed-. + +(* Basic_1: removed theorems 12: + pr0_subst0_back pr0_subst0_fwd pr0_subst0 + pr2_head_2 pr2_cflat clear_pr2_trans + pr2_gen_csort pr2_gen_cflat pr2_gen_cbind + pr2_subst1 + pr2_gen_ctail pr2_ctail +*) +(* Basic_1: removed local theorems 4: + pr0_delta_tau pr0_cong_delta + pr2_free_free pr2_free_delta +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma new file mode 100644 index 000000000..2366a0865 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cif.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cif.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Advanced forward lemmas on context-sensitive irreducible terms ***********) + +lemma cpr_fwd_cif: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. +#L #T1 #T2 #H elim H -L -T1 -T2 +[ // +| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H + elim (cif_inv_delta … HLK ?) // +| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct + lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct + lapply (IHT1 … HT1) -IHT1 #H destruct // + | elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=2/ + ] +| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cif_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (cif_inv_ri2 … H) /2 width=1/ + ] +| #L #V1 #T1 #T #T2 #_ #_ #_ #H + elim (cif_inv_ri2 … H) /2 width=1/ +| #L #V1 #T1 #T2 #_ #_ #H + elim (cif_inv_ri2 … H) /2 width=1/ +| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (cif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (cif_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. + +lemma cpss_fwd_cif_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1. +/3 width=3 by cpr_fwd_cif, cpss_cpr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma new file mode 100644 index 000000000..8c3d56e31 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/ldrop_ldrop.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Relocation properties ****************************************************) + +(* Basic_1: includes: pr0_lift pr2_lift *) +lemma cpr_lift: l_liftable cpr. +#K #T1 #T2 #H elim H -K -T1 -T2 +[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2 + >(lift_mono … H1 … H2) -H1 -H2 // +| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/ + ] +| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ +| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ +| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct + elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ +| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ +| #a #K #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /4 width=5/ +| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct + elim (lift_trans_ge … HV2 … HV3 ?) -V2 // /4 width=5/ +] +qed. + +(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) +lemma cpr_inv_lift1: l_deliftable_sn cpr. +#L #U1 #U2 #H elim H -L -U1 -U2 +[ * #L #i #K #d #e #_ #T1 #H + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ + ] +| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV + elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 + elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus plus_minus // (cpr_inv_sort1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 + elim (cpr_inv_lref1 … H) -H + [ #H destruct + elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ + | * #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/ + ] +| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpr_inv_abbr1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/ + | #T2 #HT12 #HT2 #H destruct -IHV1 + @(aaa_inv_lift (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/ + ] +| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpr_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/ + | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct + lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 + lapply (IHT1 (ⓛ{b}W1.U2) … HL12) -IHT1 /2 width=1/ -L1 #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct + lapply (lsuba_aaa_trans … HU2 (L2.ⓓV2) ?) -HU2 /2 width=2/ /2 width=3/ + | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct + lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2 + lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H + elim (aaa_inv_abbr … H) -H /3 width=3/ + ] +| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpr_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/ + | -IHV1 /2 width=1/ + ] +] +qed-. + +lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A. +/2 width=5 by aaa_cpr_lpr_conf/ qed-. + +lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A. +/2 width=5 by aaa_cpr_lpr_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma new file mode 100644 index 000000000..1d83a1314 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma @@ -0,0 +1,355 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/fsup.ma". +include "basic_2/reduction/lpr_ldrop.ma". + +(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) + +(* Main properties on context-sensitive parallel reduction for terms ********) + +fact cpr_conf_lpr_atom_atom: + ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ➡ T & L2 ⊢ ⓪{I} ➡ T. +/2 width=3/ qed-. + +fact cpr_conf_lpr_atom_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V2. K0 ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ #i ➡ T & L2 ⊢ T2 ➡ T. +#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct +elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ +qed-. + +(* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) +fact cpr_conf_lpr_delta_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V1. K0 ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → + ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX → + ∀V2. KX ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ T1 ➡ T & L2 ⊢ T2 ➡ T. +#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 +#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +lapply (ldrop_mono … H … HLK0) -H #H destruct +elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 +elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 +lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ +qed-. + +fact cpr_conf_lpr_bind_bind: + ∀a,I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ➡ T & L2 ⊢ ⓑ{a,I}V2.T2 ➡ T. +#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ +qed-. + +fact cpr_conf_lpr_bind_zeta: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓓV0 ⊢ T0 ➡ T1 → + ∀T2. L0.ⓓV0 ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ +ⓓV1.T1 ➡ T & L2 ⊢ X2 ➡ T. +#L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 // /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2 +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ /3 width=3/ +qed-. + +fact cpr_conf_lpr_zeta_zeta: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀T1. L0.ⓓV0 ⊢ T0 ➡ T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 → + ∀T2. L0.ⓓV0 ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ X1 ➡ T & L2 ⊢ X2 ➡ T. +#L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 +#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2 +elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1 +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2 +lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/ +qed-. + +fact cpr_conf_lpr_flat_flat: + ∀I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ➡ T & L2 ⊢ ⓕ{I}V2.T2 ➡ T. +#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ +qed-. + +fact cpr_conf_lpr_flat_tau: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1,T1. L0 ⊢ T0 ➡ T1 → ∀T2. L0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓝV1.T1 ➡ T & L2 ⊢ T2 ➡ T. +#L0 #V0 #T0 #IH #V1 #T1 #HT01 +#T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/ +qed-. + +fact cpr_conf_lpr_tau_tau: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀T1. L0 ⊢ T0 ➡ T1 → ∀T2. L0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ T1 ➡ T & L2 ⊢ T2 ➡ T. +#L0 #V0 #T0 #IH #T1 #HT01 +#T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/ +qed-. + +fact cpr_conf_lpr_flat_beta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ ⓛ{a}W0.T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0.ⓛW0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓐV1.T1 ➡ T & L2 ⊢ ⓓ{a}V2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW1)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +lapply (cpr_lsubr_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ /3 width=5/ +qed-. + +(* Basic-1: includes: + pr0_cong_upsilon_refl pr0_cong_upsilon_zeta + pr0_cong_upsilon_cong pr0_cong_upsilon_delta +*) +fact cpr_conf_lpr_flat_theta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ ⓓ{a}W0.T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → + ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓓW0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓐV1.T1 ➡ T & L2 ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H +#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (lift_total V 0 1) #U #HVU +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ #HU2 +elim (cpr_inv_abbr1 … H) -H * +[ #W1 #T1 #HW01 #HT01 #H destruct + elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ + elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 /4 width=7/ +| #T1 #HT01 #HXT1 #H destruct + elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 + elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 /2 width=1/ #Y #HYT #HXY + @(ex2_intro … (ⓐV.Y)) /2 width=1/ /3 width=5/ (**) (* auto /4 width=9/ is too slow *) +] +qed-. + +fact cpr_conf_lpr_beta_beta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓛW0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0.ⓛW0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓓ{a}V1.T1 ➡ T & L2 ⊢ ⓓ{a}V2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HT01 … HT02 (L1.ⓛW0) … (L2.ⓛW0)) /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2 +lapply (cpr_lsubr_trans … HT1 (L1.ⓓV1) ?) -HT1 /2 width=1/ +lapply (cpr_lsubr_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ /3 width=5/ +qed-. + +(* Basic_1: was: pr0_upsilon_upsilon *) +fact cpr_conf_lpr_theta_theta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → + ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀U1. ⇧[O, 1] V1 ≡ U1 → + ∀W1. L0 ⊢ W0 ➡ W1 → ∀T1. L0.ⓓW0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → + ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓓW0 ⊢ T0 ➡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → + ∃∃T. L1 ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & L2 ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 +#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ +elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 +elim (lift_total V 0 1) #U #HVU +lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1/ +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ /4 width=7/ +qed-. + +theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. +#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] +[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpr_inv_atom1 … H1) -H1 + elim (cpr_inv_atom1 … H2) -H2 + [ #H2 #H1 destruct + /2 width=1 by cpr_conf_lpr_atom_atom/ + | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct + /3 width=10 by cpr_conf_lpr_atom_delta/ + | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct + /4 width=10 by ex2_commute, cpr_conf_lpr_atom_delta/ + | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 + * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct + /3 width=17 by cpr_conf_lpr_delta_delta/ + ] +| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpr_inv_bind1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #T1 #HT01 #HXT1 #H11 #H12 + ] + elim (cpr_inv_bind1 … H2) -H2 * + [1,3: #V2 #T2 #HV02 #HT02 #H2 + |2,4: #T2 #HT02 #HXT2 #H21 #H22 + ] destruct + [ /3 width=10 by cpr_conf_lpr_bind_bind/ + | /4 width=11 by ex2_commute, cpr_conf_lpr_bind_zeta/ + | /3 width=11 by cpr_conf_lpr_bind_zeta/ + | /3 width=12 by cpr_conf_lpr_zeta_zeta/ + ] +| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpr_inv_flat1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #HX1 #H1 + | #a1 #V1 #Y1 #Z1 #T1 #HV01 #HZT1 #H11 #H12 #H13 + | #a1 #V1 #U1 #Y1 #W1 #Z1 #T1 #HV01 #HVU1 #HYW1 #HZT1 #H11 #H12 #H13 + ] + elim (cpr_inv_flat1 … H2) -H2 * + [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2 + |2,6,10,14: #HX2 #H2 + |3,7,11,15: #a2 #V2 #Y2 #Z2 #T2 #HV02 #HZT2 #H21 #H22 #H23 + |4,8,12,16: #a2 #V2 #U2 #Y2 #W2 #Z2 #T2 #HV02 #HVU2 #HYW2 #HZT2 #H21 #H22 #H23 + ] destruct + [ /3 width=10 by cpr_conf_lpr_flat_flat/ + | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_tau/ + | /4 width=11 by ex2_commute, cpr_conf_lpr_flat_beta/ + | /4 width=14 by ex2_commute, cpr_conf_lpr_flat_theta/ + | /3 width=8 by cpr_conf_lpr_flat_tau/ + | /3 width=7 by cpr_conf_lpr_tau_tau/ + | /3 width=11 by cpr_conf_lpr_flat_beta/ + | /3 width=11 by cpr_conf_lpr_beta_beta/ + | /3 width=14 by cpr_conf_lpr_flat_theta/ + | /3 width=17 by cpr_conf_lpr_theta_theta/ + ] +] +qed-. + +(* Basic_1: includes: pr0_confluence pr2_confluence *) +theorem cpr_conf: ∀L. confluent … (cpr L). +/2 width=6 by cpr_conf_lpr/ qed-. + +(* Properties on context-sensitive parallel reduction for terms *************) + +lemma lpr_cpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡ L1 → + ∃∃T. L1 ⊢ T0 ➡ T & L1 ⊢ T1 ➡ T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/ +qed-. + +lemma lpr_cpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡ L1 → + ∃∃T. L1 ⊢ T0 ➡ T & L0 ⊢ T1 ➡ T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ +qed-. + +lemma fsup_cpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➡ U2 → + ∃∃L,U1. L1 ⊢ ➡ L & L ⊢ T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (ldrop_lpr_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K +lapply (cpr_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma new file mode 100644 index 000000000..c5cb57721 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma @@ -0,0 +1,270 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpss_ldrop.ma". +include "basic_2/reduction/lpr_ldrop.ma". + +(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) + +(* Properties on context-sensitive parallel substitution for terms **********) + +fact cpr_cpss_conf_lpr_lpss_atom_atom: + ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ▶* T & L2 ⊢ ⓪{I} ➡ T. +/2 width=3/ qed-. + +fact cpr_cpss_conf_lpr_lpss_atom_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ➡ T. +#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct +elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_delta_atom: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V1. K0 ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ #i ➡ T. +#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 #L1 #HL01 #L2 #HL02 +elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpss_inv_pair1 … H2) -H2 #K2 #V2 #HK02 #HV02 #H destruct +elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 /3 width=9/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_delta_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V1. K0 ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → + ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX → + ∀V2. KX ⊢ VX ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ➡ T. +#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 +#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +lapply (ldrop_mono … H … HLK0) -H #H destruct +elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 +elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 +lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_bind_bind: + ∀a,I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ▶* T & L2 ⊢ ⓑ{a,I}V2.T2 ➡ T. +#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_bind_zeta: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀T1. L0.ⓓV0 ⊢ T0 ➡ T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0.ⓓV0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ X1 ▶* T & L2 ⊢ +ⓓV2.T2 ➡ T. +#L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 (L1.ⓓV2) … (L2.ⓓV2)) -IH -HT01 -HT02 // /2 width=1/ /3 width=1/ -L0 -V0 -T0 #T #HT1 #HT2 +elim (cpss_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ /3 width=9/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_flat_flat: + ∀I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ▶* T & L2 ⊢ ⓕ{I}V2.T2 ➡ T. +#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_flat_tau: + ∀L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀T1. L0 ⊢ T0 ➡ T1 → ∀V2,T2. L0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ ⓝV2.T2 ➡ T. +#L0 #V0 #T0 #IH #T1 #HT01 +#V2 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_flat_beta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓛW0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0 ⊢ ⓛ{a}W0.T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓓ{a}V1.T1 ▶* T & L2 ⊢ ⓐV2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #X #H #L1 #HL01 #L2 #HL02 +elim (cpss_inv_bind1 … H) -H #W2 #T2 #HW02 #HT02 #H destruct +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HT01 … HT02 (L1.ⓛW2) … (L2.ⓛW2)) /2 width=1/ /3 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +lapply (cpss_lsubr_trans … HT1 (L1.ⓓV1) ?) -HT1 /2 width=1/ /3 width=5/ +qed-. + +fact cpr_cpss_conf_lpr_lpss_flat_theta: + ∀a,L0,V0,W0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 + ) → + ∀V1. L0 ⊢ V0 ➡ V1 → ∀U1. ⇧[O, 1] V1 ≡ U1 → + ∀W1. L0 ⊢ W0 ➡ W1 → ∀T1. L0.ⓓW0 ⊢ T0 ➡ T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0 ⊢ ⓓ{a}W0.T0 ▶* T2 → + ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓓ{a}W1.ⓐU1.T1 ▶* T & L2 ⊢ ⓐV2.T2 ➡ T. +#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 +#V2 #HV02 #X #H #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (lift_total V 0 1) #U #HVU +lapply (cpss_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1/ #HU1 +elim (cpss_inv_bind1 … H) -H #W2 #T2 #HW02 #HT02 #H destruct +elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ +elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 +/4 width=9 by ex2_intro, cpr_theta, cpss_bind, cpss_flat/ (**) (* auto too slow without trace *) +qed-. + +lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss. +#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] +[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpr_inv_atom1 … H1) -H1 + elim (cpss_inv_atom1 … H2) -H2 + [ #H2 #H1 destruct + /2 width=1 by cpr_cpss_conf_lpr_lpss_atom_atom/ + | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct + /3 width=10 by cpr_cpss_conf_lpr_lpss_atom_delta/ + | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct + /3 width=10 by cpr_cpss_conf_lpr_lpss_delta_atom/ + | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 + * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct + /3 width=17 by cpr_cpss_conf_lpr_lpss_delta_delta/ + ] +| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2 + elim (cpr_inv_bind1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #T1 #HT01 #HXT1 #H11 #H12 + ] destruct + [ /3 width=10 by cpr_cpss_conf_lpr_lpss_bind_bind/ + | /3 width=11 by cpr_cpss_conf_lpr_lpss_bind_zeta/ + ] +| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2 + elim (cpr_inv_flat1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #HX1 #H1 + | #a1 #V1 #Y1 #Z1 #T1 #HV01 #HZT1 #H11 #H12 #H13 + | #a1 #V1 #U1 #Y1 #W1 #Z1 #T1 #HV01 #HVU1 #HYW1 #HZT1 #H11 #H12 #H13 + ] destruct + [ /3 width=10 by cpr_cpss_conf_lpr_lpss_flat_flat/ + | /3 width=8 by cpr_cpss_conf_lpr_lpss_flat_tau/ + | /3 width=11 by cpr_cpss_conf_lpr_lpss_flat_beta/ + | /3 width=14 by cpr_cpss_conf_lpr_lpss_flat_theta/ + ] +] +qed-. + +(* Basic_1: includes: pr0_subst1 *) +lemma cpr_cpss_conf: ∀L. confluent2 … (cpr L) (cpss L). +/2 width=6 by cpr_cpss_conf_lpr_lpss/ qed-. + +lemma cpr_lpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T1 ▶* T & L1 ⊢ T0 ➡ T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpr_cpss_conf_lpr_lpss … HT01 T0 … L1 … HL01) // /2 width=1/ -L0 /2 width=3/ +qed-. + +lemma cpr_lpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L0 ⊢ T1 ▶* T & L1 ⊢ T0 ➡ T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpr_cpss_conf_lpr_lpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ +qed-. + +(* Basic_1: includes: pr0_subst1_fwd *) +lemma lpr_cpss_conf: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ➡ L1 → + ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ➡ T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpr_cpss_conf_lpr_lpss ?? T0 … HT01 … HL01 L0) // -HT01 -HL01 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma new file mode 100644 index 000000000..2ea40eeb4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.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/relocation/ldrop_lpx_sn.ma". +include "basic_2/reduction/cpr_lift.ma". +include "basic_2/reduction/lpr.ma". + +(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) + +(* Properies on local environment slicing ***********************************) + +(* Basic_1: includes: wcpr0_drop *) +lemma lpr_ldrop_conf: dropable_sn lpr. +/3 width=5 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-. + +(* Basic_1: includes: wcpr0_drop_back *) +lemma ldrop_lpr_trans: dedropable_sn lpr. +/3 width=9 by lpx_sn_liftable_dedropable, cpr_lift/ qed-. + +lemma lpr_ldrop_trans_O1: dropable_dx lpr. +/2 width=3 by lpx_sn_dropable/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma similarity index 68% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index 4a27a6e70..ab77692dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -12,18 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/tpr_tpr.ma". -include "basic_2/reducibility/ltpr.ma". +include "basic_2/reduction/lpr_cpr.ma". -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) +(* SN PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ******************************) (* Main properties **********************************************************) -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/ -#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/ -qed. +theorem lpr_conf: confluent … lpr. +/3 width=6 by lpx_sn_conf, cpr_conf_lpr/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma new file mode 100644 index 000000000..34aaa4e12 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpr_cpss.ma". + +(* SN PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ******************************) + +(* Properties on sn parallel substitution on local environments *************) + +lemma lpr_lpss_conf: confluent2 … lpr lpss. +/3 width=6 by lpx_sn_conf, cpr_cpss_conf_lpr_lpss/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma index 4efbd3545..8cec0b050 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/ssta.ma". -include "basic_2/reducibility/cpr.ma". +include "basic_2/reduction/cpr.ma". lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w. #x #y #z #w #H