From ca9cf24217384150ed1474dacba7b7dbb8836dbf Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 27 Jan 2012 21:01:01 +0000
Subject: [PATCH] support for abstract candidates of reducibility closed! ...
---
.../Basic_2/computation/acp_aaa.ma | 2 +-
.../Basic_2/computation/acp_cr.ma | 2 +-
.../lambda_delta/Basic_2/grammar/aarity.ma | 1 +
.../contribs/lambda_delta/Basic_2/names.txt | 1 +
.../lambda_delta/Basic_2/static/aaa_aaa.ma | 39 ++++++++++
.../lambda_delta/Basic_2/static/aaa_lift.ma | 47 ++++++++++++
.../lambda_delta/Basic_2/static/aaa_lifts.ma | 30 ++++++++
.../lambda_delta/Basic_2/unfold/gr2.ma | 60 ++++++++++-----
.../lambda_delta/Basic_2/unfold/gr2_gr2.ma | 10 ++-
.../lambda_delta/Basic_2/unfold/gr2_minus.ma | 76 +++++++++++++++++++
.../lambda_delta/Basic_2/unfold/gr2_plus.ma | 40 ++++++++++
.../lambda_delta/Basic_2/unfold/ldrops.ma | 1 +
.../lambda_delta/Basic_2/unfold/lifts.ma | 2 +-
.../lambda_delta/Basic_2/unfold/lifts_lift.ma | 28 ++++++-
.../Basic_2/unfold/lifts_vector.ma | 11 ++-
15 files changed, 325 insertions(+), 25 deletions(-)
create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma
create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma
create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma
create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma
create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
index 0f70ef703..a65a8b81d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
@@ -44,7 +44,7 @@ theorem aacr_aaa_csubc_lifts: âRR,RS,RP.
[ #K2 #HK20 #H destruct
generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2
[ elim (lift_total V0 0 (i0 +1)) #V #HV0
- elim (lifts_lift_trans ⦠HV10 ⦠HV0 ⦠Hi0 Hdes0) -HV10 #V2 #HV12 #HV2
+ elim (lifts_lift_trans ⦠Hi0 ⦠Hdes0 ⦠HV10 ⦠HV0) -HV10 #V2 #HV12 #HV2
@(s4 ⦠HB ⦠â ⦠HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *)
| @(s2 ⦠HB ⦠â) // /2 width=3/
]
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
index 9f94d8969..46f864522 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
@@ -127,7 +127,7 @@ lemma aacr_acr: âRR,RS,RP. acp RR RS RP â acr RR RS RP (λL,T. RP L T) â
>(at_mono ⦠Hi1 ⦠Hi0) in HL02; -i1 #HL02
elim (ldrops_inv_skip2 ⦠Hdes0 ⦠H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
- elim (lifts_lift_trans ⦠HVW1 ⦠HW12 ⦠Hdes0) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
+ elim (lifts_lift_trans ⦠Hdes0 ⦠HVW1 ⦠HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono ⦠HV13 ⦠HV12) in HVW2; -V3 #HVW2
@(s4 ⦠IHA ⦠(V0 :: V0s) ⦠HW12 HL02) /3 width=4/
| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
index 61a9666b5..15418582b 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
@@ -13,6 +13,7 @@
(**************************************************************************)
(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
+ * Support for abstract candidates of reducibility closed: 2012 January 27
* Confluence of context-sensitive parallel reduction closed: 2011 September 21
* Confluence of context-free parallel reduction closed: 2011 September 6
* Specification started: 2011 April 17
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt
index cc9bb6936..dfa83ebdd 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/names.txt
@@ -23,6 +23,7 @@ i,j : local reference position index (de Bruijn's)
k : sort index
p,q : global reference position
t,u : local reference position level (de Bruijn's)
+x,y,z : reserved: transient objet denoted by a small letter
NAMING CONVENTIONS FOR CONSTRUCTORS
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma
new file mode 100644
index 000000000..4f9bb7dc3
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/ldrop_ldrop.ma".
+include "Basic_2/static/aaa.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Main properties **********************************************************)
+
+theorem aaa_mono: âL,T,A1. L ⢠T ÷ A1 â âA2. L ⢠T ÷ A2 â A1 = A2.
+#L #T #A1 #H elim H -L -T -A1
+[ #L #k #A2 #H
+ >(aaa_inv_sort ⦠H) -H //
+| #I1 #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
+ elim (aaa_inv_lref ⦠H) -H #I2 #K2 #V2 #HLK2 #HA2
+ lapply (ldrop_mono ⦠HLK1 ⦠HLK2) -L #H destruct /2 width=1/
+| #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+ elim (aaa_inv_abbr ⦠H) -H /2 width=1/
+| #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
+ elim (aaa_inv_abst ⦠H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/
+| #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+ elim (aaa_inv_appl ⦠H) -H #B2 #_ #HA2
+ lapply (IHA1 ⦠HA2) -L #H destruct //
+| #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
+ elim (aaa_inv_cast ⦠H) -H /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma
new file mode 100644
index 000000000..edf08147e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_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/substitution/ldrop_ldrop.ma".
+include "Basic_2/static/aaa.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties concerning basic relocation ***********************************)
+
+lemma aaa_lift: âL1,T1,A. L1 ⢠T1 ÷ A â âL2,d,e. â©[d, e] L2 â¡ L1 â
+ âT2. â§[d, e] T1 â¡ T2 â L2 ⢠T2 ÷ A.
+#L1 #T1 #A #H elim H -L1 -T1 -A
+[ #L1 #k #L2 #d #e #_ #T2 #H
+ >(lift_inv_sort1 ⦠H) -H //
+| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
+ elim (lift_inv_lref1 ⦠H) -H * #Hid #H destruct
+ [ elim (ldrop_trans_le ⦠HL21 ⦠HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 ⦠H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+ /3 width=8/
+ | lapply (ldrop_trans_ge ⦠HL21 ⦠HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+ elim (lift_inv_bind1 ⦠H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+ elim (lift_inv_bind1 ⦠H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+ elim (lift_inv_flat1 ⦠H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /3 width=4/
+| #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
+ elim (lift_inv_flat1 ⦠H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /3 width=4/
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma
new file mode 100644
index 000000000..156e75c9d
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/ldrops.ma".
+include "Basic_2/static/aaa_lift.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties concerning generic relocation *********************************)
+
+lemma aaa_lifts: âL1,L2,T2,A,des. â©*[des] L2 â¡ L1 â âT1. â§*[des] T1 â¡ T2 â
+ L1 ⢠T1 ÷ A â L2 ⢠T2 ÷ A.
+#L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
+[ #L #T1 #H #HT1
+ <(lifts_inv_nil ⦠H) -H //
+| #L1 #L #L2 #des #d #e #_ #HL2 #IHL1 #T1 #H #HT1
+ elim (lifts_inv_cons ⦠H) -H /3 width=9/
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma
index a33f018c2..0896b6ba3 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma
@@ -16,14 +16,6 @@ include "Basic_2/grammar/term_vector.ma".
(* GENERIC RELOCATION WITH PAIRS ********************************************)
-let rec pluss (des:list2 nat nat) (i:nat) on des â match des with
-[ nil2 â â
-| cons2 d e des â {d + i, e} :: pluss des i
-].
-
-interpretation "plus (generic relocation with pairs)"
- 'plus x y = (pluss x y).
-
inductive at: list2 nat nat â relation nat â
| at_nil: âi. at â i i
| at_lt : âdes,d,e,i1,i2. i1 < d â
@@ -35,13 +27,47 @@ inductive at: list2 nat nat â relation nat â
interpretation "application (generic relocation with pairs)"
'RAt i1 des i2 = (at des i1 i2).
-inductive minuss: nat â relation (list2 nat nat) â
-| minuss_nil: âi. minuss i â â
-| minuss_lt : âdes1,des2,d,e,i. i < d â minuss i des1 des2 â
- minuss i ({d, e} :: des1) ({d - i, e} :: des2)
-| minuss_ge : âdes1,des2,d,e,i. d ⤠i â minuss (e + i) des1 des2 â
- minuss i ({d, e} :: des1) des2
-.
+(* Basic inversion lemmas ***************************************************)
+
+fact at_inv_nil_aux: âdes,i1,i2. @[i1] des â¡ i2 â des = â â i1 = i2.
+#des #i1 #i2 * -des -i1 -i2
+[ //
+| #des #d #e #i1 #i2 #_ #_ #H destruct
+| #des #d #e #i1 #i2 #_ #_ #H destruct
+]
+qed.
+
+lemma at_inv_nil: âi1,i2. @[i1] â â¡ i2 â i1 = i2.
+/2 width=3/ qed-.
+
+fact at_inv_cons_aux: âdes,i1,i2. @[i1] des â¡ i2 â
+ âd,e,des0. des = {d, e} :: des0 â
+ i1 < d ⧠@[i1] des0 â¡ i2 â¨
+ d ⤠i1 ⧠@[i1 + e] des0 ⡠i2.
+#des #i1 #i2 * -des -i1 -i2
+[ #i #d #e #des #H destruct
+| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/
+| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/
+]
+qed.
+
+lemma at_inv_cons: âdes,d,e,i1,i2. @[i1] {d, e} :: des â¡ i2 â
+ i1 < d ⧠@[i1] des â¡ i2 â¨
+ d ⤠i1 ⧠@[i1 + e] des ⡠i2.
+/2 width=3/ qed-.
+
+lemma at_inv_cons_lt: âdes,d,e,i1,i2. @[i1] {d, e} :: des â¡ i2 â
+ i1 < d â @[i1] des â¡ i2.
+#des #d #e #i1 #e2 #H
+elim (at_inv_cons ⦠H) -H * // #Hdi1 #_ #Hi1d
+lapply (le_to_lt_to_lt ⦠Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
+elim (lt_refl_false ⦠Hd)
+qed-.
-interpretation "minus (generic relocation with pairs)"
- 'RMinus des1 i des2 = (minuss i des1 des2).
+lemma at_inv_cons_ge: âdes,d,e,i1,i2. @[i1] {d, e} :: des â¡ i2 â
+ d ⤠i1 â @[i1 + e] des â¡ i2.
+#des #d #e #i1 #e2 #H
+elim (at_inv_cons ⦠H) -H * // #Hi1d #_ #Hdi1
+lapply (le_to_lt_to_lt ⦠Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
+elim (lt_refl_false ⦠Hd)
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma
index dd2d34d07..438605e85 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma
@@ -18,4 +18,12 @@ include "Basic_2/unfold/gr2.ma".
(* Main properties **********************************************************)
-axiom at_mono: âdes,i,i1. @[i] des â¡ i1 â âi2. @[i] des â¡ i2 â i1 = i2.
+theorem at_mono: âdes,i,i1. @[i] des â¡ i1 â âi2. @[i] des â¡ i2 â i1 = i2.
+#des #i #i1 #H elim H -des -i -i1
+[ #i #x #H <(at_inv_nil ⦠H) -x //
+| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H
+ lapply (at_inv_cons_lt ⦠H Hid) -H -Hid /2 width=1/
+| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H
+ lapply (at_inv_cons_ge ⦠H Hdi) -H -Hdi /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma
new file mode 100644
index 000000000..5e3144c93
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/gr2.ma".
+
+(* GENERIC RELOCATION WITH PAIRS ********************************************)
+
+inductive minuss: nat â relation (list2 nat nat) â
+| minuss_nil: âi. minuss i â â
+| minuss_lt : âdes1,des2,d,e,i. i < d â minuss i des1 des2 â
+ minuss i ({d, e} :: des1) ({d - i, e} :: des2)
+| minuss_ge : âdes1,des2,d,e,i. d ⤠i â minuss (e + i) des1 des2 â
+ minuss i ({d, e} :: des1) des2
+.
+
+interpretation "minus (generic relocation with pairs)"
+ 'RMinus des1 i des2 = (minuss i des1 des2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact minuss_inv_nil1_aux: âdes1,des2,i. des1 â i â¡ des2 â des1 = â â des2 = â .
+#des1 #des2 #i * -des1 -des2 -i
+[ //
+| #des1 #des2 #d #e #i #_ #_ #H destruct
+| #des1 #des2 #d #e #i #_ #_ #H destruct
+]
+qed.
+
+lemma minuss_inv_nil1: âdes2,i. â â i â¡ des2 â des2 = â .
+/2 width=4/ qed-.
+
+fact minuss_inv_cons1_aux: âdes1,des2,i. des1 â i â¡ des2 â
+ âd,e,des. des1 = {d, e} :: des â
+ d ⤠i ⧠des â e + i â¡ des2 â¨
+ ââdes0. i < d & des â i â¡ des0 &
+ des2 = {d - i, e} :: des0.
+#des1 #des2 #i * -des1 -des2 -i
+[ #i #d #e #des #H destruct
+| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
+| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/
+]
+qed.
+
+lemma minuss_inv_cons1: âdes1,des2,d,e,i. {d, e} :: des1 â i â¡ des2 â
+ d ⤠i ⧠des1 â e + i â¡ des2 â¨
+ ââdes. i < d & des1 â i â¡ des &
+ des2 = {d - i, e} :: des.
+/2 width=3/ qed-.
+
+lemma minuss_inv_cons1_ge: âdes1,des2,d,e,i. {d, e} :: des1 â i â¡ des2 â
+ d ⤠i â des1 â e + i â¡ des2.
+#des1 #des2 #d #e #i #H
+elim (minuss_inv_cons1 ⦠H) -H * // #des #Hid #_ #_ #Hdi
+lapply (lt_to_le_to_lt ⦠Hid Hdi) -Hid -Hdi #Hi
+elim (lt_refl_false ⦠Hi)
+qed-.
+
+lemma minuss_inv_cons1_lt: âdes1,des2,d,e,i. {d, e} :: des1 â i â¡ des2 â
+ i < d â
+ ââdes. des1 â i â¡ des & des2 = {d - i, e} :: des.
+#des1 #des2 #d #e #i #H
+elim (minuss_inv_cons1 ⦠H) -H * /2 width=3/ #Hdi #_ #Hid
+lapply (lt_to_le_to_lt ⦠Hid Hdi) -Hid -Hdi #Hi
+elim (lt_refl_false ⦠Hi)
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma
new file mode 100644
index 000000000..938f955b9
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/gr2.ma".
+
+(* GENERIC RELOCATION WITH PAIRS ********************************************)
+
+let rec pluss (des:list2 nat nat) (i:nat) on des â match des with
+[ nil2 â â
+| cons2 d e des â {d + i, e} :: pluss des i
+].
+
+interpretation "plus (generic relocation with pairs)"
+ 'plus x y = (pluss x y).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma pluss_inv_nil2: âi,des. des + i = â â des = â .
+#i * // normalize
+#d #e #des #H destruct
+qed.
+
+lemma pluss_inv_cons2: âi,d,e,des2,des. des + i = {d, e} :: des2 â
+ ââdes1. des1 + i = des2 & des = {d - i, e} :: des1.
+#i #d #e #des2 * normalize
+[ #H destruct
+| #d1 #e1 #des1 #H destruct /2 width=3/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
index 78f4dd6af..d271fe2c6 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
@@ -13,6 +13,7 @@
(**************************************************************************)
include "Basic_2/substitution/ldrop.ma".
+include "Basic_2/unfold/gr2_minus.ma".
include "Basic_2/unfold/lifts.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
index 40f4325b1..57405868f 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
@@ -13,7 +13,7 @@
(**************************************************************************)
include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2.ma".
+include "Basic_2/unfold/gr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
index 8bec02119..b10b3c17b 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
@@ -13,6 +13,7 @@
(**************************************************************************)
include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/unfold/gr2_minus.ma".
include "Basic_2/unfold/lifts.ma".
(* GENERIC TERM RELOCATION **************************************************)
@@ -31,7 +32,28 @@ lemma lifts_lift_trans_le: âT1,T,des. â§*[des] T1 â¡ T â âT2. â§[0, 1]
qed-.
(* Basic_1: was: lift1_free (right to left) *)
-axiom lifts_lift_trans: âT1,T0,des0. â§*[des0] T1 â¡ T0 â
- âT2,i0. â§[O, i0 + 1] T0 â¡ T2 â
- âdes,i. @[i] des â¡ i0 â des + 1 â i + 1 â¡ des0 + 1 â
+lemma lifts_lift_trans: âdes,i,i0. @[i] des â¡ i0 â
+ âdes0. des + 1 â i + 1 â¡ des0 + 1 â
+ âT1,T0. â§*[des0] T1 â¡ T0 â
+ âT2. â§[O, i0 + 1] T0 â¡ T2 â
ââT. â§[0, i + 1] T1 â¡ T & â§*[des] T â¡ T2.
+#des elim des -des normalize
+[ #i #x #H1 #des0 #H2 #T1 #T0 #HT10 #T2
+ <(at_inv_nil ⦠H1) -x #HT02
+ lapply (minuss_inv_nil1 ⦠H2) -H2 #H
+ >(pluss_inv_nil2 ⦠H) in HT10; -des0 #H
+ >(lifts_inv_nil ⦠H) -T1 /2 width=3/
+| #d #e #des #IHdes #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
+ elim (at_inv_cons ⦠H1) -H1 * #Hid #Hi0
+ [ elim (minuss_inv_cons1_lt ⦠H2 ?) -H2 [2: /2 width=1/ ] #des1 #Hdes1 <plus_minus // <minus_plus <plus_minus_m_m /2 width=1/ #H
+ elim (pluss_inv_cons2 ⦠H) -H #des2 #H1 #H2 destruct
+ elim (lifts_inv_cons ⦠HT10) -HT10 #T >minus_plus #HT1 #HT0
+ elim (IHdes ⦠Hi0 ⦠Hdes1 ⦠HT0 ⦠HT02) -IHdes -Hi0 -Hdes1 -T0 #T0 #HT0 #HT02
+ elim (lift_trans_le ⦠HT1 ⦠HT0 ?) -T /2 width=1/ #T #HT1 <plus_minus_m_m /2 width=1/ /3 width=5/
+ | >commutative_plus in Hi0; #Hi0
+ lapply (minuss_inv_cons1_ge ⦠H2 ?) -H2 [ /2 width=1/ ] <associative_plus #Hdes0
+ elim (IHdes ⦠Hi0 ⦠Hdes0 ⦠HT10 ⦠HT02) -IHdes -Hi0 -Hdes0 -T0 #T0 #HT0 #HT02
+ elim (lift_split ⦠HT0 d (i+1) ? ? ?) -HT0 /2 width=1/ /3 width=5/
+ ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
index f3ec86b2d..2bd579d01 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
@@ -29,9 +29,18 @@ interpretation "generic relocation (vector)"
(* Basic inversion lemmas ***************************************************)
-axiom lifts_inv_applv1: âV1s,U1,T2,des. â§*[des] ⶠV1s. U1 â¡ T2 â
+lemma lifts_inv_applv1: âV1s,U1,T2,des. â§*[des] ⶠV1s. U1 â¡ T2 â
ââV2s,U2. â§*[des] V1s â¡ V2s & â§*[des] U1 â¡ U2 &
T2 = ⶠV2s. U2.
+#V1s elim V1s -V1s normalize
+[ #T1 #T2 #des #HT12
+ @(ex3_2_intro) [3,4: // |1,2: skip | // ] (**) (* explicit constructor *)
+| #V1 #V1s #IHV1s #T1 #X #des #H
+ elim (lifts_inv_flat1 ⦠H) -H #V2 #Y #HV12 #HY #H destruct
+ elim (IHV1s ⦠HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct
+ @(ex3_2_intro) [4: // |3: /2 width=2/ |1,2: skip | // ] (**) (* explicit constructor *)
+]
+qed-.
(* Basic properties *********************************************************)
--
2.39.2