let mk_exists ooch noch c v =
let description = "multiple existental quantifier" in
let prec = "non associative with precedence 20\n" in
- let name s = P.sprintf "%s%u_%u" s c v in
+ let name s =
+ if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
+ in
let o_name = name "ex" in
let i_name = "'Ex" in
PACKAGES = ground_2 basic_2 apps_2
all:
+ ../../matitac.opt
# xoa ########################################################################
[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
elim (lt_or_eq_or_gt i d) #Hid
[ -HLK >(tri_lt ?????? Hid) /3 width=3/
- | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)
+ | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)
| -HLK >(tri_gt ?????? Hid) /3 width=3/
]
| * /3 width=1/ /4 width=1/
[ /2 width=3/
| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
- @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
+ @(ex2_intro … HT10) -T1 (**) (* explicit constructors *)
@(cprs_strap1 … T3 …) /2 width=1/ -HT32
@(cprs_strap1 … HT0) -HT0 /3 width=3/
]
(* Basic properties *********************************************************)
-(* Basic_1: was: flt_wf__q_ind *)
-
-(* Basic_1: was: flt_wf_ind *)
-axiom fw_ind: ∀R:relation2 lenv term.
- (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) →
- ∀L,T. R L T.
-
(* Basic_1: was: flt_shift *)
lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
normalize //
normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
qed.
-(* Basic_1: removed theorems 6:
+(* Basic_1: removed theorems 7:
flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
+ flt_wf_ind
*)
+(* Basic_1: removed local theorems 1: q_ind *)
elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
qed.
-lemma lpx_conf: ∀R. Confluent ? R → Confluent … (lpx R).
+lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R).
#R #HR #L0 #L1 #H elim H -L1
[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/
| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
/3 width=1/ qed.
-(* Basic eliminators ********************************************************)
-
-axiom lw_ind: ∀R:predicate lenv.
- (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
- ∀L. R L.
-
(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
(* Basic_1: note: clt_thead should be renamed clt_ctail *)
#T elim T -T //
qed.
-(* Basic eliminators ********************************************************)
-
-axiom tw_ind: ∀R:predicate term.
- (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
- ∀T. R T.
-
(* Basic_1: removed theorems 11:
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
- removed local theorems 1: q_ind
*)
+(* Basic_1: removed local theorems 1: q_ind *)
lemma cpr_bind_sn: ∀a,I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
#a #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
-@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
+@ex2_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
qed.
(* Basic_1: was only: pr2_gen_cbind *)
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
-@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
+@ex2_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
(* Basic_1: was only: pr2_head_1 *)
⇧[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_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
+@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 #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a
lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
lapply (tpss_lsubs_trans … HT02 (L.ⓛV2) ?) -HT02 /2 width=1/ #HT02
-@(ex2_1_intro … (ⓛ{a}V0.T0)) /2 width=1/ (* explicit constructors *)
+@(ex2_intro … (ⓛ{a}V0.T0)) /2 width=1/ (* explicit constructors *)
qed.
lemma cpr_beta: ∀a,L,V1,V2,W,T1,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_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
-@(ex2_1_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
+@(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.
#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
<(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I
lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
-@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
+@(ex2_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
qed.
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_1_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
+ @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 (IHW12 … HW01) -W1 #W3 #HW32 #HW03
elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
- @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+ @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 (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_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
- @ex2_1_intro
+ @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/
| -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_1_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
+ @(ex2_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
]
qed.
elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
-@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
+@ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
fact tpr_conf_delta_zeta:
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_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
+@ex2_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
qed.
fact tpr_conf_zeta_zeta:
elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
elim (lift_total VV2 0 1) #VV #H2VV
lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
- @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+ @ex2_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
[ #H1 #_ #K2 #H2
lapply (ldrop_inv_refl … H1) -H1 #H1
lapply (ldrop_inv_refl … H2) -H2 #H2 destruct //
- | #e #_ #H1 #H1e #K2 #H2
+ | #e #_ #H1 #H #K2 #H2
+ lapply (le_plus_to_le_r … H) -H
lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
- lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // /3 width=4/
+ lapply (ldrop_inv_ldrop1 … H2 ?) -H2 //
+ <minus_plus_m_m /2 width=4/
]
]
qed-.
#L elim L -L //
#L #I #V #IHL #d @(nat_ind_plus … d) -d
[ #e @(nat_ind_plus … e) -e //
- #e #_ #HH
- >(HH I L V 0 ? ? ?) // /5 width=6/
-| /5 width=6/
+ #e #_ #H0
+ >(H0 I L V 0 ? ? ?) //
+ /5 width=6 by sfr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
+| #d #_ #e #H0
+ /5 width=6 by sfr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
]
qed.
-lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
+lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
dd + ee ≤ d → ≽ [dd, ee] L2.
#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
@(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
qed.
-lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
+lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
d + e ≤ dd → ≽ [dd - e, ee] L2.
#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
| >(lift_inv_lref2_ge … H ?) -H //
lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
- @ex2_1_intro [2: /2 width=1/ | skip ] -Hd1e12
+ @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
@lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
]
| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
elim (lt_or_ge i j)
[ -Hide -Hjde
>(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=4/
- | -Hdi -Hdj #Hid
- generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *)
- >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
+ | -Hdi -Hdj #Hij
+ lapply (plus_minus_m_m … Hjde) -Hjde /3 width=8/
]
| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
[ /2 width=3/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
elim (lt_or_ge i j)
- [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /4 width=4/
+ [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=8/
| -Hdi -Hdj
>(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/
]
lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
#V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
- @ex2_1_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+ @ex2_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
]
| #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie
#V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
- @ex2_1_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+ @ex2_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
| #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (le_inv_plus_l … Hdetd) #_ #Hedt
[ /2 width=3/
| #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
elim (tps_inv_lref1 … H) -H
- [ #HX destruct /4 width=4/
+ [ #HX destruct /3 width=6/
| -Hd1 -Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2
lapply (ldrop_mono … HLK1 … HLK2) -HLK1 -HLK2 #H destruct
>(lift_mono … HVT1 … HVT2) -HVT1 -HVT2 /2 width=3/
[ /2 width=3/
| #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2
elim (tps_inv_lref1 … H1) -H1
- [ #H destruct /4 width=4/
+ [ #H destruct /3 width=6/
| -HLK1 -HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded
[ -Hd1 -Hde2
lapply (transitive_le … Hded Hd2) -Hded -Hd2 #H
| #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2
- <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
+ <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /3 width=8/
| #L #a #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
qed.
lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
-#L #T1 @(fw_ind … L T1) -L -T1 #L #T1 elim T1 -T1
-[ * #i #IH #T2 #d #e #H
+#L #T1 @(f2_ind … fw … L T1) -L -T1 #n #IH #L *
+[ * #i #Hn #T2 #d #e #H destruct
[ >(delift_inv_sort1 … H) -H //
| elim (delift_inv_lref1 … H) -H * /2 width=1/
#K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
lapply (IH … HV12) // -H /2 width=6/
| >(delift_inv_gref1 … H) -H //
]
-| * [ #a ] #I #V1 #T1 #_ #_ #IH #X #d #e #H
+| * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
[ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12) -HV12 // #HV12
elim (lift_total V 0 (i+1)) #U #HVU
lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
lapply (lift_conf_be … HVU2 … HV2U ?) //
->commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
+>commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
qed.
-fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
- ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
-#L #T @(fw_ind … L T) -L -T #L #T #IH * * /2 width=2/
-[ #i #d #e #Hde #HL #H destruct
+lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
+ ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
+#L #T1 @(f2_ind … fw … L T1) -L -T1
+#n #IH #L * * /2 width=2/
+[ #i #H #d #e #Hde #HL destruct
elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
lapply (lt_to_le_to_lt … Hide Hde) #Hi
lapply (ldrop_fwd_O1_length … HLK0) #H
lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
[1,2: /2 width=1/ | <minus_n_O <minus_plus ] #HK
- elim (IH … HKL … HK ?) -IH -HKL -HK
- [3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
+ elim (IH … HKL … HK) -IH -HKL -HK
+ [2: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
elim (lift_total V2 0 d) /3 width=7/
-| #a #I #V1 #T1 #d #e #Hde #HL #H destruct
- elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
- elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12
+| #a #I #V1 #T1 #H #d #e #Hde #HL destruct
+ elim (IH … V1 … Hde HL) // #V2 #HV12
+ elim (IH (L.ⓑ{I}V1) T1 … (d+1) e ??) -IH // [2,3: /2 width=1/ ] -Hde -HL #T2 #HT12
lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
-| #I #V1 #T1 #d #e #Hde #HL #H destruct
- elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
- elim (IH … T1 … Hde HL ?) -IH -Hde -HL [3,4: // |2: skip ] /3 width=2/
+| #I #V1 #T1 #H #d #e #Hde #HL destruct
+ elim (IH … V1 … Hde HL) // #V2 #HV12
+ elim (IH … T1 … Hde HL) -IH -Hde -HL // /3 width=2/
]
-qed.
-
-lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
- ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
-/2 width=2/ qed-.
+qed-.
(* Advanced inversion lemmas ************************************************)
@(bi_TC_ind_dx … IH1 IH2 ? ? H)
qed-.
+(* Baic inversion lemmas ****************************************************)
+
+lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+ ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_r/ qed-.
+
+lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+ ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_l/ qed-.
+
(* Basic properties *********************************************************)
lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
(* Advanced forward lemmas **************************************************)
-fact lift_frsupp_trans_aux: ∀L2,U0. (
- ∀L,K,U1,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
- ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
- #{L, U1} < #{L2, U0} →
- ∃T2. ⇧[d + |K|, e] T2 ≡ U2
- ) →
- ∀L1,K,U1,U2. ⦃L1, U1⦄ ⧁+ ⦃L2 @@ K, U2⦄ →
- ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
- L2 = L1 → U0 = U1 →
- ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#L2 #U0 #IH #L1 #X #U1 #U2 #H @(frsupp_ind_dx … H) -L1 -U1 /2 width=5 by lift_frsup_trans/
-#L1 #L #U1 #U #HL1 #HL2 #_ #T1 #d #e #HTU1 #H1 #H2 destruct
-elim (frsup_fwd_append … HL1) #K1 #H destruct
-elim (frsupp_fwd_append … HL2) #K >append_assoc #H
-elim (append_inj_dx … H ?) -H // #_ #H destruct
-<append_assoc in HL2; #HL2
-elim (lift_frsup_trans … HTU1 … HL1) -T1 #T #HTU
-lapply (frsup_fwd_fw … HL1) -HL1 #HL1
-elim (IH … HL2 … HTU ?) -IH -HL2 -T // -L1 -U1 -U /2 width=2/
-qed-.
-
lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#L #U1 @(fw_ind … L U1) -L -U1 /3 width=10 by lift_frsupp_trans_aux/
+#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH
+#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct
+elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ *
+#L0 #U0 #HL0 #HL
+elim (frsup_fwd_append … HL0) #K0 #H destruct
+elim (frsupp_fwd_append … HL) #L0 >append_assoc #H
+elim (append_inj_dx … H ?) -H // #_ #H destruct
+<append_assoc in HL; #HL
+elim (lift_frsup_trans … HTU1 … HL0) -T1 #T #HTU
+lapply (frsup_fwd_fw … HL0) -HL0 #HL0
+elim (IH … HL … HTU) -IH -HL -T // -L -U1 -U0 /2 width=2/
qed-.
(**************************************************************************)
include "basic_2/unfold/tpss_tpss.ma".
-include "basic_2/unfold/tpss_alt.ma".
include "basic_2/unfold/ltpss_dx_tpss.ma".
(* DX PARTIAL UNFOLD ON LOCAL ENVIRONMENTS **********************************)
]
qed.
-fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
- L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
- Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+#L1 #T2 @(f2_ind … fw … L1 T2) -L1 -T2 #n #IH #L1 *
+[ #I #Hn #W2 #d #e #H #L0 #HL01 destruct
+ elim (tpss_inv_atom1 … H) -H // *
+ #K1 #V1 #V2 #i #Hdi #Hide #HLK1 #HV12 #HVW2 #H destruct
lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tpss_fwd_tw … HV01) #H2
lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
- lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
- [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
-| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
- lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
- lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+ lapply (IH … HV02 … HK01) -IH -HV02 -HK01
+ [ normalize /2 width=1/ | /2 width=6/ ]
+| * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
+ [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+ lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+ lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
+ lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
+ lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+ | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+ lapply (IH … HVW2 … HL0) -HVW2 //
+ lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
]
qed.
-lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
- ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
-
lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
/3 width=3/ qed.
(* Main properties **********************************************************)
-fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
- ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
- ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-#K @(lw_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
-[ -IH /2 width=3/
-| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ /2 width=3/
- | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
- ]
-| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ -IH #d2 #e2 #H1 #H2 destruct
- | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- ]
-| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ -IH #d2 #e2 #H1 #H2 destruct
- | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- ]
-]
-qed.
-
theorem ltpss_dx_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-/2 width=7/ qed.
+#L0 @(f_ind … lw … L0) -L0 #n #IH *
+[ #_ #L1 #d1 #e1 #H1 #L2 #d2 #e2 #H2 -n
+ >(ltpss_dx_inv_atom1 … H1) -L1
+ >(ltpss_dx_inv_atom1 … H2) -L2 /2 width=3/
+| #K0 #I0 #V0 #Hn #L1 #d1 #e1 #H1 #L2 #d2 #e2 #H2 destruct
+ elim (eq_or_gt d1) #Hd1 [ elim (eq_or_gt e1) #He1 ] destruct
+ [ lapply (ltpss_dx_inv_refl_O2 … H1) -H1 #H1
+ | elim (ltpss_dx_inv_tpss21 … H1 … He1) -H1 #K1 #V1 #HK01 #HV01 #H1
+ | elim (ltpss_dx_inv_tpss11 … H1 … Hd1) -H1 #K1 #V1 #HK01 #HV01 #H1
+ ] destruct
+ elim (eq_or_gt d2) #Hd2 [1,3,5: elim (eq_or_gt e2) #He2 ] destruct
+ [1,3,5: lapply (ltpss_dx_inv_refl_O2 … H2) -H2 #H2
+ |2,4,6: elim (ltpss_dx_inv_tpss21 … H2 … He2) -H2 #K2 #V2 #HK02 #HV02 #H2
+ |7,8,9: elim (ltpss_dx_inv_tpss11 … H2 … Hd2) -H2 #K2 #V2 #HK02 #HV02 #H2
+ ] destruct
+ [1: -IH /2 width=3/
+ |2,3,4,7: -IH /3 width=5/
+ |5,6,8,9:
+ elim (IH … HK01 … HK02) // -K0 #K #HK1 #HK2
+ elim (ltpss_dx_tpss_conf … HV01 … HK1) -HV01 #W1 #HW1 #HVW1
+ elim (ltpss_dx_tpss_conf … HV02 … HK2) -HV02 #W2 #HW2 #HVW2
+ elim (tpss_conf_eq … HW1 … HW2) -V0 #V #HW1 #HW2
+ lapply (tpss_trans_eq … HVW1 HW1) -W1
+ lapply (tpss_trans_eq … HVW2 HW2) -W2 /3 width=5/
+ ]
+]
+qed.
#L0 #L1 #d1 #e1 #H #L2 #d2 #e2 #HL02
lapply (ltpss_sn_ltpssa … H) -H #HL01
elim (ltpssa_strip … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
qed.
(* Note: this should go in ltpss_sn_ltpss_sn.ma *)
lapply (ltpss_sn_ltpssa … H1) -H1 #HL01
lapply (ltpss_sn_ltpssa … H2) -H2 #HL02
elim (ltpssa_conf … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
qed.
(**************************************************************************)
include "basic_2/unfold/tpss_tpss.ma".
-include "basic_2/unfold/tpss_alt.ma".
include "basic_2/unfold/ltpss_sn_tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* Advanced properties ******************************************************)
-fact ltpss_sn_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
- L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ⊢ ▶* [d, e] L1 →
- Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ⊢ ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+#L1 #T2 @(f2_ind … fw … L1 T2) -L1 -T2 #n #IH #L1 *
+[ #I #Hn #W2 #d #e #H #L0 #HL01 destruct
+ elim (tpss_inv_atom1 … H) -H // *
+ #K1 #V1 #V2 #i #Hdi #Hide #HLK1 #HV12 #HVW2 #H destruct
lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
elim (ltpss_sn_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltpss_sn_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
- lapply (IH … HV12 … HK01 ? ?) -IH -HV12 -HK01 [1,3: // |2,4: skip | normalize /2 width=1/ ] #HV12
+ lapply (IH … HV12 … HK01) -IH -HV12 -HK01 [ normalize /2 width=1/ ] #HV12
lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
-| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
- lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
- lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+| * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
+ [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+ lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+ lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
+ lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
+ lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+ | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+ lapply (IH … HVW2 … HL0) -HVW2 //
+ lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
]
qed.
-lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
- ∀L0. L0 ⊢ ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
-
lemma ltpss_sn_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ⊢ ▶* [d, e] L1 →
L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
/3 width=3/ qed.
| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: >commutative_plus /2 width=1/ ]
- /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
+ /3 width=7 by ex2_intro, step/ (**) (* just /3 width=7/ is too slow *)
]
qed.
definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
-definition Confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
- ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
- ∃∃a. R a1 a & R a2 a.
-
definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R.
∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2.
elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
- elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=3/
+ elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5/
]
qed.
elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
- elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=3/
+ elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5/
]
qed.
elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02
- elim (IHa … Ha0) -a /4 width=3/
+ elim (IHa … Ha0) -a /4 width=5/
]
qed.
elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02
- elim (IHa … Ha0) -a /4 width=3/
+ elim (IHa … Ha0) -a /4 width=5/
]
qed.
elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/
]
qed.
+
+lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+ R a1 b1 a2 b2 ∨
+ ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/
+qed-.
+
+lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+ R a1 b1 a2 b2 ∨
+ ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx ?????????? H) -a1 -b1
+[ /2 width=1/
+| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/
+]
+qed-.
-->
</section>
<section name="xoa">
- <key name="output_dir">contribs/lambda_delta/ground_2/</key>
+ <key name="output_dir">contribs/lambdadelta/ground_2/</key>
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
<key name="ex">1 2</key>
<key name="ex">1 3</key>
- <key name="ex">2 1</key>
<key name="ex">2 2</key>
<key name="ex">2 3</key>
<key name="ex">3 1</key>
interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0).
-(* multiple existental quantifier (2, 1) *)
-
-inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
- | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
-
(* multiple existental quantifier (2, 2) *)
inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
(* multiple existental quantifier (3, 1) *)
-inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
- | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
+inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+ | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ?
.
-interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2).
(* multiple existental quantifier (3, 2) *)
(* multiple existental quantifier (4, 1) *)
-inductive ex4_1 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
- | ex4_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4_1 ? ? ? ? ?
+inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
+ | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ?
.
-interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4_1 ? P0 P1 P2 P3).
+interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3).
(* multiple existental quantifier (4, 2) *)
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }.
-(* multiple existental quantifier (2, 1) *)
-
-notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
-
-notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
-
(* multiple existental quantifier (2, 2) *)
notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
interpretation "logical false" 'false = False.
interpretation "logical true" 'true = True.
-
-lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2 width=3/
-qed.
-baseuri=cic:/matita/lambda_delta/
+baseuri=cic:/matita/lambdadelta/
theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
#n #m #lenm (elim lenm) /3/ qed.
+theorem eq_or_gt: ∀n. 0 = n ∨ 0 < n.
+#n elim (le_to_or_lt_eq 0 n ?) // /2 width=1/
+qed-.
+
theorem increasing_to_le2: ∀f:nat → nat. increasing f →
∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
#f #incr #m #lem (elim lem)
R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2.
#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/
qed.
-
+
lemma bi_TC_reflexive: ∀A,B,R. bi_reflexive A B R →
bi_reflexive A B (bi_TC … R).
/2 width=1/ qed.
projects / helm.git / commitdiff