[ #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/
]
>(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
(**************************************************************************)
(* 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
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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/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.
(* 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 →
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-.
(* 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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/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-.
(**************************************************************************)
include "Basic_2/substitution/ldrop.ma".
+include "Basic_2/unfold/gr2_minus.ma".
include "Basic_2/unfold/lifts.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
(**************************************************************************)
include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2.ma".
+include "Basic_2/unfold/gr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
(**************************************************************************)
include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/unfold/gr2_minus.ma".
include "Basic_2/unfold/lifts.ma".
(* GENERIC TERM RELOCATION **************************************************)
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-.
(* 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 *********************************************************)
projects / helm.git / commitdiff