--- /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 "static_2/syntax/tdpos.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-transition for terms *********************)
+
+lemma cpm_tdeq_fwd_tdpos_sn (a) (h) (o) (n) (G):
+ ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → 𝐏[h,o]⦃T1⦄ →
+ ∧∧ T1 = T2 & 0 = n.
+#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2
+@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2
+[ /2 width=1 by conj/
+| #L #s #_ #H1 #H
+ elim (tdpos_inv_sort … H) -H #d #H2
+ lapply (deg_mono … H2 H1) -H1 -H2 #H destruct
+| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #H
+ elim (tdpos_inv_pair … H) -H #_ #HT1
+ elim IH // -IH -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #H -a -m -q -G -L -W -U1
+ elim (tdpos_inv_pair … H) -H #_ #HT1
+ elim IH // -IH -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #H
+ elim (tdpos_inv_pair … H) -H #HU1 #HT1
+ elim IHU // -IHU -HU1 #H1 #H2 destruct
+ elim IHT // -IHT -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpm_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
+ ∨∨ ∧∧ T1 = T2 & 0 = n | (T1 ≛[h,o] T2 → ⊥).
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #HT12
+elim (tdeq_dec h o T1 T2) #H
+/3 width=9 by cpm_tdeq_fwd_tdpos_sn, or_intror, or_introl/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predstar_7.ma".
include "basic_2/dynamic/cnv_cpm_trans.ma".
include "basic_2/dynamic/cnv_cpm_conf.ma".
+include "basic_2/dynamic/cnv_cpms_tdpos.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2.
- ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n.
-
-interpretation
- "context-sensitive parallel stratified t-bound rt-computarion (term)"
- 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2).
+(* Sub confluence propery with t-bound rt-computation for terms *************)
-definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+fact cnv_cpms_conf_lpr_refl_refl_aux (h) (G0) (L1) (L2) (T0:term):
+ ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[h] T & ⦃G0,L2⦄ ⊢ T0 ➡*[h] T.
+/2 width=3 by ex2_intro/ qed-.
-(* Sub confluence propery with t-bound rt-computation for terms *************)
+fact cnv_cpms_conf_lpr_refl_step_aux (a) (h) (o) (G0) (L0) (T0) (m21) (m22):
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
+ ⦃G0,L0⦄ ⊢ T0 ![a,h] →
+ ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛[h,o] X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
+ ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[m21+m22,h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[h] T.
+#a #h #o #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0
+#X2 #HX02 #HnX02 #T2 #HXT2
+#L1 #HL01 #L2 #HL02
+lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
+elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) //
+<minus_n_O <minus_O_n #Y1 #HXY1 #HTY1
+elim (cnv_cpms_strip_lpr_sub … IH1 … HXT2 0 X2 … HL02 L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ]
+<minus_n_O <minus_O_n #Y2 #HTY2 #HXY2 -HXT2
+elim (IH1 … HXY1 … HXY2 … HL01 … HL02) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ]
+-a -o -L0 -X2 <minus_n_O <minus_O_n #Y #HY1 #HY2
+lapply (cpms_trans … HTY1 … HY1) -Y1 #HT0Y
+lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y
+/2 width=3 by ex2_intro/
+qed-.
-fact cnv_cpsms_conf_lpr_aux (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpsms_conf_lpr a h o G1 L1 T1.
-#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0
-#n1 #T1 * #m11 #m12 #X1 #HnX01 #HX01 #HXT1 #H1
-#n2 #T2 * #m21 #m22 #X2 #HnX02 #HX02 #HXT2 #H2
-#L1 #HL01 #L2 #HL02 destruct
+fact cnv_cpms_conf_lpr_step_step_aux (a) (h) (o) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
+ ⦃G0,L0⦄ ⊢ T0 ![a,h] →
+ ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → (T0 ≛[h,o] X1 → ⊥) → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 →
+ ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛[h,o] X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
+ ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T.
+#a #h #o #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0
+#X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2
+#L1 #HL01 #L2 #HL02
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
/2 width=3 by ex2_intro/
qed-.
+
+fact cnv_cpms_conf_lpr_aux (a) (h) (o):
+ ∀G0,L0,T0. 𝐏[h,o]⦃T0⦄ →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_conf_lpr a h G1 L1 T1.
+#a #h #o #G #L #T #H0 #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT
+#HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct
+elim (cpms_fwd_tdpos_sn … HT0 H0 … HT01) *
+elim (cpms_fwd_tdpos_sn … HT0 H0 … HT02) *
+-H0 -HT01 -HT02
+[ #H21 #H22 #H11 #H12 destruct -a -o -L0
+ <minus_n_O
+ /2 width=1 by cnv_cpms_conf_lpr_refl_refl_aux/
+| #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 #H11 #H12 destruct
+ <minus_n_O <minus_O_n
+ @(cnv_cpms_conf_lpr_refl_step_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
+| #H21 #H22 #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
+ <minus_n_O <minus_O_n
+ @ex2_commute @(cnv_cpms_conf_lpr_refl_step_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
+| #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
+ @(cnv_cpms_conf_lpr_step_step_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
+]
+qed-.
+++ /dev/null
-(*
-axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
- ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
- ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
-axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
-
-lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
- ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
- elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
- [ #H #_ destruct //
- | #s #H #_ #_ #_ destruct //
- ]
-| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
- elim (cnv_inv_bind … H0) #HV1 #_
- elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
- /3 width=6 by cnv_bind/
-| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
- elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
- elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
- @(cnv_appl … Hm … HVW1)
-
-(* Properties with restricted rt-transition for terms ***********************)
-
-lemma pippo (a) (h) (o) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
- ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
- ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
- ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
- elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
- [ #H1 #H2 destruct /2 width=4 by ex3_intro/
- | #s #H1 #H2 #H3 #Hs destruct
- elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
- /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
- ]
-| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
- elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
- elim (cpm_inv_bind1 … HX2) -HX2 *
- [ #V2 #T2 #HV12 #HT2 #H destruct
- elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
- @(ex3_intro … (ⓑ{p,I}V2.T0))
- [ /2 width=1 by cpm_bind/
- |
- | /2 width=1 by tdeq_pair/
-
-*)
--- /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/dynamic/cnv_cpm_tdpos.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-computation for terms ********************)
+
+lemma cpms_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
+ ∨∨ ∧∧ T1 = T2 & 0 = n
+ | ∃∃n1,n2,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T & (T1 ≛[h,o] T → ⊥) & ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2=n.
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #H
+@(cpms_ind_dx … H) -n -T2
+[ /3 width=1 by or_introl, conj/
+| #n1 #n2 #T #T2 #HT1 * *
+ [ #H1 #H2 #HT2 destruct -HT1
+ elim (cpm_fwd_tdpos_sn … H1T1 H2T1 … HT2) -H1T1 -H2T1
+ [ * #H1 #H2 destruct -HT2 /3 width=1 by or_introl, conj/
+ | #HnT2 >commutative_plus in ⊢ (??%); /4 width=7 by ex4_3_intro, or_intror/
+ ]
+ | #m1 #m2 #T0 #H1T10 #H2T10 #HT0 #H #HT2 destruct -H1T1 -H2T1 -HT1
+ >associative_plus in ⊢ (??%); /4 width=7 by cpms_step_dx, ex4_3_intro, or_intror/
+ ]
+]
+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/dynamic/cnv_cpm_trans.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Far properties for preservation ******************************************)
-
-fact cnv_cpms_trans_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
-#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct
-@(cpms_ind_dx … H) -n -T2
-[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 //
-| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct
- @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH
- /3 width=4 by cpms_fpbg_trans/
-]
-qed-.
+++ /dev/null
-cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
-cnv_preserve_far.ma cnv_cpm_trans.ma cnv_cpm_conf.ma
-lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma lsubv_lsubv.ma
--- /dev/null
+(*
+axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
+ ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
+axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
+
+lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
+#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
+#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H #_ destruct //
+ | #s #H #_ #_ #_ destruct //
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
+ elim (cnv_inv_bind … H0) #HV1 #_
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
+ /3 width=6 by cnv_bind/
+| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
+ elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
+ elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
+ @(cnv_appl … Hm … HVW1)
+
+(* Properties with restricted rt-transition for terms ***********************)
+
+lemma pippo (a) (h) (o) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
+#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
+#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H1 #H2 destruct /2 width=4 by ex3_intro/
+ | #s #H1 #H2 #H3 #Hs destruct
+ elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
+ /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
+ elim (cpm_inv_bind1 … HX2) -HX2 *
+ [ #V2 #T2 #HV12 #HT2 #H destruct
+ elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
+ @(ex3_intro … (ⓑ{p,I}V2.T0))
+ [ /2 width=1 by cpm_bind/
+ |
+ | /2 width=1 by tdeq_pair/
+
+*)
--- /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/dynamic/cnv_cpm_trans.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Far properties for preservation ******************************************)
+
+fact cnv_cpms_trans_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct
+@(cpms_ind_dx … H) -n -T2
+[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 //
+| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct
+ @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH
+ /3 width=4 by cpms_fpbg_trans/
+]
+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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 n, break term 46 h, break term 46 o ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRedStar $n $h $o $G $L $T1 $T2 }.
*)
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
}
]
}
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( 𝐏 [ term 46 h, term 46 o ] ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'Positive $h $o $T }.
--- /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 "static_2/notation/relations/positive_3.ma".
+include "static_2/syntax/item_sd.ma".
+include "static_2/syntax/term.ma".
+
+(* DEGREE POSITIVITY ON TERMS ***********************************************)
+
+inductive tdpos (h) (o): predicate term ≝
+| tdpos_sort: ∀s,d. deg h o s (↑d) → tdpos h o (⋆s)
+| tdpos_lref: ∀i. tdpos h o (#i)
+| tdpos_gref: ∀l. tdpos h o (§l)
+| tdpos_pair: ∀I,V,T. tdpos h o V → tdpos h o T → tdpos h o (②{I}V.T)
+.
+
+interpretation
+ "context-free degree positivity (term)"
+ 'Positive h o T = (tdpos h o T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tdpos_inv_sort_aux (h) (o):
+ ∀X. 𝐏[h,o]⦃X⦄ → ∀s. X = ⋆s → ∃d. deg h o s (↑d).
+#h #o #H *
+[ #s #d #Hsd #x #H destruct /2 width=2 by ex_intro/
+| #i #x #H destruct
+| #l #x #H destruct
+| #I #V #T #_ #_ #x #H destruct
+]
+qed-.
+
+lemma tdpos_inv_sort (h) (o): ∀s. 𝐏[h,o]⦃⋆s⦄ → ∃d. deg h o s (↑d).
+/2 width=3 by tdpos_inv_sort_aux/ qed-.
+
+fact tdpos_inv_pair_aux (h) (o): ∀X. 𝐏[h,o]⦃X⦄ → ∀I,V,T. X = ②{I}V.T →
+ ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+#h #o #H *
+[ #s #d #_ #Z #X1 #X2 #H destruct
+| #i #Z #X1 #X2 #H destruct
+| #l #Z #X1 #X2 #H destruct
+| #I #V #T #HV #HT #Z #X1 #X2 #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma tdpos_inv_pair (h) (o): ∀I,V,T. 𝐏[h,o]⦃②{I}V.T⦄ →
+ ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+/2 width=4 by tdpos_inv_pair_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+axiom tdpos_total (h): ∀T. ∃o. 𝐏[h,o]⦃T⦄.
[ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
}
]
+ [ { "degree positivity" * } {
+ [ [ "for terms" ] "tdpos" + "( 𝐏[?,?]⦃?⦄ )" * ]
+ }
+ ]
[ { "degree-based equivalence" * } {
[ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
[ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
projects / helm.git / commitdiff