lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T.
/2 width=1/ qed.
-axiom xprs_strap1: ∀h,g,L,T1,T,T2.
+lemma xprs_strap1: ∀h,g,L,T1,T,T2.
⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-(**) (* NTypeChecker failure
-/2 width=3/ qed.
-*)
-axiom xprs_strap2: ∀h,g,L,T1,T,T2.
+/2 width=3 by step/ qed. (**) (* NTypeChecker failure without trace *)
+
+lemma xprs_strap2: ∀h,g,L,T1,T,T2.
⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-(**) (* NTypeChecker failure
-/2 width=3/ qed.
-*)
+/2 width=3 by TC_strap/ qed. (**) (* NTypeChecker failure without trace *)
+
(* Basic inversion lemmas ***************************************************)
(*
axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
-(*
#L #T #U #H @(xprs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
-*)*)
+*)
#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
qed.
+(* Note: lemma 750 *)
lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2.
#L1 elim L1 -L1
[ * normalize //
--- /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/reducibility/crf.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+definition cif: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥.
+
+interpretation "context-sensitive irreducibility (term)"
+ 'NotReducible L T = (cif L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cif_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥.
+/3 width=3/ qed-.
+
+lemma cif_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
+/3 width=1/ qed-.
+
+lemma cif_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄.
+/4 width=1/ qed-.
+
+lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I.
+#a * [ elim a -a ]
+[ #L #V #T #H elim (H ?) -H /3 width=1/
+|*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+]
+qed-.
+
+lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
+#L #V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // #a * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
+qed-.
+
+lemma cif_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
+ ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+* #L #V #T #H
+[ elim (cif_inv_appl … H) -H /2 width=1/
+| elim (cif_inv_ri2 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tif_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄.
+/2 width=2 by trf_inv_atom/ qed.
+
+lemma cif_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
+#a #I #L #V #T #HI #HV #HT #H
+elim (crf_inv_ib2 … HI H) -HI -H /2 width=1/
+qed.
+
+lemma cif_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄.
+#L #V #T #HV #HT #H1 #H2
+elim (crf_inv_appl … H2) -H2 /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/reducibility/crf_append.ma".
+include "basic_2/reducibility/cif.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+(* Advanved properties ******************************************************)
+
+lemma cif_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄.
+/3 width=2 by crf_inv_labst_last/ qed.
+
+lemma cif_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄.
+/3 width=2 by crf_inv_trf/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cif_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
+
+lemma cif_inv_tif: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
interpretation
"context-sensitive normality (term)"
- 'Normal L T = (cnf L T).
+ 'Normal L T = (cnf L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+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 //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+ [ elim (lift_total V1 0 1) #V2 #HV12
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #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 /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 //
+qed-.
(* Basic properties *********************************************************)
--- /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/tps_lift.ma".
+include "basic_2/unfold/tpss.ma".
+include "basic_2/reducibility/cif.ma".
+include "basic_2/reducibility/cnf_lift.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Main properties **********************************************************)
+
+lemma tps_cif_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▶[d, e] T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+[ //
+| #L #K #V #W #i #d #e #_ #_ #HLK #_ #H -d -e
+ elim (cif_inv_delta … HLK ?) //
+| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H
+ elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
+ lapply (IHV12 … HV1) -IHV12 -HV1 #H destruct /3 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H
+ elim (cif_inv_flat … H) -H #HV1 #HT1 #_ #_ /3 width=1/
+]
+qed.
+
+lemma tpss_cif_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▶*[d, e] T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 #HT1
+lapply (IHT1 HT1) -IHT1 #H destruct /2 width=5/
+qed.
+
+lemma tpr_cif_eq: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#T1 #T2 #H elim H -T1 -T2
+[ //
+| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #L #H
+ [ elim (cif_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (cif_inv_ri2 … H) /2 width=1/
+ ]
+| #a #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #L #H
+ elim (cif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #L #H
+ [ lapply (tps_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+ elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
+ lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
+ lapply (IHT1 … HT1) -IHT1 #H destruct
+ lapply (tps_cif_eq … HT2 ?) -HT2 //
+ | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
+ elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+ ]
+| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #L #H
+ elim (cif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #V1 #T1 #T #T2 #_ #_ #_ #L #H
+ elim (cif_inv_ri2 … H) /2 width=1/
+| #V1 #T1 #T2 #_ #_ #L #H
+ elim (cif_inv_ri2 … H) /2 width=1/
+]
+qed.
+
+lemma cpr_cif_eq: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 * #T0 #HT10 #HT02 #HT1
+lapply (tpr_cif_eq … HT10 … HT1) -HT10 #H destruct /2 width=5/
+qed.
+
+theorem cif_cnf: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄.
+/3 width=3/ qed.
+
+(* Note: this property is unusual *)
+lemma cnf_crf_false: ∀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.
+
+theorem cnf_cif: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/2 width=4/ qed.
(**************************************************************************)
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
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
+fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
#I #L #T * -L -T
[ #L #K #V #i #HLK #H1 #H2 destruct
lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
/2 width=6/ qed-.
-fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
- L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄.
-#a #L #W #U #T * -T
+fact trf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+#L #T * -L -T
+[ #L #K #V #j #HLK #i #H destruct /2 width=3/
+| #L #V #T #_ #i #H destruct
+| #L #V #T #_ #i #H destruct
+| #J #L #V #T #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #L #V #W #T #i #H destruct
+| #a #L #V #W #T #i #H destruct
+]
+qed.
+
+lemma trf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+/2 width=3/ qed-.
+
+fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
+#a #I #L #W #U #T #HI * -T
[ #L #K #V #i #_ #H destruct
| #L #V #T #_ #H destruct
| #L #V #T #_ #H destruct
| #J #L #V #T #H1 #H2 destruct
elim H1 -H1 #H destruct
+ elim HI -HI #H destruct
| #b #J #L #V #T #_ #HV #H destruct /2 width=1/
| #b #J #L #V #T #_ #HT #H destruct /2 width=1/
| #b #L #V #W #T #H destruct
]
qed.
-lemma crf_inv_abst: ∀a,L,W,T. L ⊢ 𝐑⦃ⓛ{a}W.T⦄ → L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃T⦄.
-/2 width=4/ qed-.
+lemma crf_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
+/2 width=5/ qed-.
fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
/2 width=3/ qed-.
-
(* *)
(**************************************************************************)
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/ldrop_append.ma".
include "basic_2/reducibility/crf.ma".
(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
-(* advanced inversion lemmas ************************************************)
-(*
-lemma crf_inv_labst_last: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ → ⇩[0, |L1|-1] L1 ≡ ⋆.ⓛW →
- ∀L2. ⇩[|L1|-1, 1] L1 ≡ L2 → L2 ⊢ 𝐑⦃T⦄.
+(* Advanved properties ******************************************************)
+
+lemma crf_labst_last: ∀L,T,W. L ⊢ 𝐑⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄.
+#L #T #W #H elim H -L -T /2 width=1/
+#L #K #V #i #HLK
+lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … (⋆.ⓛW)) -HLK /2 width=2/ -Hi /2 width=3/
+qed.
+
+lemma crf_trf: ∀T,W. ⋆ ⊢ 𝐑⦃T⦄ → ⋆.ⓛW ⊢ 𝐑⦃T⦄.
+#T #W #H lapply (crf_labst_last … W H) //
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact crf_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ →
+ ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄.
#L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
-[ #L1 #K1 #V1 #i #HLK1 #HL1 #L2 #HL12 destruct
- lapply (ldrop_fwd_ldrop2_length … HLK1) #H
- elim (le_to_or_lt_eq i (|L1|-1) ?) /2 width=1/ -H #Hi destruct [ -HL1 | - HL12 ]
- [ elim (ldrop_conf_lt … HL12 … HLK1 ?) -HLK1 -HL12 // -Hi /2 width=3/
- | lapply (ldrop_mono … HL1 … HLK1) -HL1 -HLK1 #H destruct
+[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
+ lapply (ldrop_fwd_ldrop2_length … HLK1)
+ >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
+ elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct
+ [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
+ normalize #H destruct /2 width=3/
+ | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
+ lapply (ldrop_inv_refl … H) -H #H destruct
]
-| #a #I #L1 #V #T #HI #_
- normalize <minus_plus_m_m #IHT #HL1 #L2 #HL12
- lapply (ldrop_fwd_ldrop2_length … HL1) #H
- lapply (ltn_to_ltO … H) -H #H
- @(crf_ib2_dx … HI) @IHT
- [ @ldrop_ldrop_lt //
- | @ldrop_skip_lt //
+| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
]
qed.
-
lemma crf_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐑⦃T⦄.
-#L2 #T #H elim H -L2 -T
-[ #L2 #K2 #V2 #i #HLK2 #L1 #HL12
-*)
+/2 width=4/ qed-.
+
+lemma crf_inv_trf: ∀T,W. ⋆.ⓛW ⊢ 𝐑⦃T⦄ → ⋆ ⊢ 𝐑⦃T⦄.
+/2 width=4/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
+lemma thnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
normalize /2 width=1/
qed-.
]
qed.
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
+lemma thnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
/3 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/reducibility/trf.ma".
-
-(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
-
-definition tif: predicate term ≝ λT. 𝐑⦃T⦄ → ⊥.
-
-interpretation "context-free irreducibility (term)"
- 'NotReducible T = (tif T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tif_inv_abbr: ∀V,T. 𝐈⦃ⓓV.T⦄ → ⊥.
-/2 width=1/ qed-.
-
-lemma tif_inv_abst: ∀V,T. 𝐈⦃ⓛV.T⦄ → 𝐈⦃V⦄ ∧ 𝐈⦃T⦄.
-/4 width=1/ qed-.
-
-lemma tif_inv_appl: ∀V,T. 𝐈⦃ⓐV.T⦄ → ∧∧ 𝐈⦃V⦄ & 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#V #T #HVT @and3_intro /3 width=1/
-generalize in match HVT; -HVT elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
-qed-.
-
-lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓝV.T⦄ → ⊥.
-/2 width=1/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tif_atom: ∀I. 𝐈⦃⓪{I}⦄.
-/2 width=4/ qed.
-
-lemma tif_abst: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐈⦃ⓛV.T⦄.
-#V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2 width=1/
-qed.
-
-lemma tif_appl: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐒⦃T⦄ → 𝐈⦃ⓐV.T⦄.
-#V #T #HV #HT #S #H
-elim (trf_inv_appl … 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/reducibility/tpr.ma".
-
-(* CONTEXT-FREE NORMAL TERMS ************************************************)
-
-definition tnf: predicate term ≝ NF … tpr (eq …).
-
-interpretation
- "context-free normality (term)"
- 'Normal T = (tnf T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tnf_inv_abst: ∀a,V,T. 𝐍⦃ⓛ{a}V.T⦄ → 𝐍⦃V⦄ ∧ 𝐍⦃T⦄.
-#a #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
-]
-qed-.
-
-lemma tnf_inv_appl: ∀V,T. 𝐍⦃ⓐV.T⦄ → ∧∧ 𝐍⦃V⦄ & 𝐍⦃T⦄ & 𝐒⦃T⦄.
-#V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
-| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
- [ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /2 width=3/ -HV12 #H destruct
- | lapply (H (ⓓ{a}V1.U1) ?) -H /2 width=1/ #H destruct
-]
-qed-.
-
-lemma tnf_inv_abbr: ∀V,T. 𝐍⦃+ⓓV.T⦄ → ⊥.
-#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 (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
- lapply (H (+ⓓV.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
-]
-qed.
-
-lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓝV.T⦄ → ⊥.
-#V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
-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/tps_lift.ma".
-include "basic_2/reducibility/tif.ma".
-include "basic_2/reducibility/tnf.ma".
-
-(* CONTEXT-FREE NORMAL TERMS ************************************************)
-
-(* Main properties properties ***********************************************)
-
-lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈⦃T1⦄ → T1 = T2.
-#T1 #T2 #H elim H -T1 -T2
-[ //
-| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (tif_inv_cast … H)
- ]
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
- [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
- | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
- elim (tif_inv_abst … H) -H #HV1 #HT1
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- ]
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (tif_inv_abbr … H)
-| #V1 #T1 #T2 #_ #_ #H
- elim (tif_inv_cast … H)
-]
-qed.
-
-theorem tif_tnf: ∀T1. 𝐈⦃T1⦄ → 𝐍⦃T1⦄.
-/3 width=1/ qed.
-
-(* Note: this property is unusual *)
-lemma tnf_trf_false: ∀T1. 𝐑⦃T1⦄ → 𝐍⦃T1⦄ → ⊥.
-#T1 #H elim H -T1
-[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #H elim (tnf_inv_abbr … H)
-| #V #T #H elim (tnf_inv_cast … H)
-| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-qed.
-
-theorem tnf_tif: ∀T1. 𝐍⦃T1⦄ → 𝐈⦃T1⦄.
-/2 width=3/ qed.
-
-lemma tnf_abst: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐍⦃ⓛV.T⦄.
-/4 width=1/ qed.
-
-lemma tnf_appl: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐒⦃T⦄ → 𝐍⦃ⓐV.T⦄.
-/4 width=1/ qed.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/
qed.
-lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+lemma ldrop_O1_le: ∀i,L. i ≤ |L| → ∃K. ⇩[0, i] L ≡ K.
+#i @(nat_ind_plus … i) -i /2 width=2/
+#i #IHi *
+[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct
+| #L #I #V normalize #H
+ elim (IHi L ?) -IHi /2 width=1/ -H /3 width=2/
+]
+qed.
+
+lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
#L elim L -L
[ #i #H elim (lt_zero_false … H)
-| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/ #i #_ #H
- lapply (lt_plus_to_lt_l … H) -H #Hi
- elim (IHL i ?) // /3 width=4/
+| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/
+ #i #_ normalize #H
+ elim (IHL i ? ) -IHL /2 width=1/ -H /3 width=4/
]
qed.
(* Properties on append for local environments ******************************)
-lemma ldrop_append_O1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
- |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ d = 0 → e ≤ |L1| →
+ ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/
+#d #e #_ #H #L -d
+lapply (le_n_O_to_eq … H) -H //
+qed-.
+
+lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
+ ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
+
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //
#L2 #I #V #IHL2 #e #H #H1e
elim (ldrop_inv_O1 … H) -H * #H2e #HL12 destruct
>commutative_plus normalize #H destruct
| <minus_plus >minus_minus_comm /3 width=1/
]
-qed.
+qed-.
-lemma ldrop_append_O1_lt: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e < |L2| →
- ∃∃K2. ⇩[0, e] L2 ≡ K2 & K = L1 @@ K2.
-#K #L1 #L2 elim L2 -L2
-[ #e #_ #H elim (lt_zero_false … H)
-| #L2 #I #V #IHL2 #e normalize #HL12 #H1e
- elim (ldrop_inv_O1 … HL12) -HL12 * #H2e #HL12 destruct
- [ -H1e -IHL2 /3 width=3/
- | elim (IHL2 … HL12 ?) -IHL2 -HL12 /2 width=1/ -H1e #K2 #HLK2 #H destruct /3 width=3/
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+ ∀K2. ⇩[0, e] L2 ≡ K2 → K = L1 @@ K2.
+#K #L1 #L2 elim L2 -L2 normalize
+[ #e #H1 #H2 #K2 #H3
+ lapply (le_n_O_to_eq … H2) -H2 #H2
+ lapply (ldrop_inv_atom1 … H3) -H3 #H3 destruct
+ >(ldrop_inv_refl … H1) -H1 //
+| #L2 #I #V #IHL2 #e @(nat_ind_plus … e) -e [ -IHL2 ]
+ [ #H1 #_ #K2 #H2
+ lapply (ldrop_inv_refl … H1) -H1 #H1
+ lapply (ldrop_inv_refl … H2) -H2 #H2 destruct //
+ | #e #_ #H1 #H1e #K2 #H2
+ lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
+ lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // /3 width=4/
]
]
-qed.
+qed-.
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
- elim (ldrop_O1 … Hi) -Hi #I #K #V1 #HLK
+ elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
<key name="or">3</key>
<key name="or">4</key>
<key name="and">3</key>
+ <key name="and">4</key>
</section>
</helm_registry>
interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
+(* multiple conjunction connective (4) *)
+
+inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝
+ | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ?
+.
+
+interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3).
+
non associative with precedence 35
for @{ 'And $P0 $P1 $P2 }.
+(* multiple conjunction connective (4) *)
+
+notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2 break & term 34 P3)"
+ non associative with precedence 35
+ for @{ 'And $P0 $P1 $P2 $P3 }.
+
["-tptppath",Arg.String
(fun s -> Helm_registry.set_string "matita.tptppath" s),
"Where to find the Axioms/ and Problems/ directory"];
- MatitaInit.initialize_all ()
+ MatitaInit.initialize_all ();
+ MatitaMisc.reset_font_size ()
;;
let _ =
projects / helm.git / commitdiff