| ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙.
/2 width=3 by cpg_inv_cast1_aux/ qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpg_inv_zero1_pair: ∀Rt,c,h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[Rt, c, h] T2 →
+ ∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
+ | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ I = Abbr & c = cV
+ | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ I = Abst & c = cV+𝟘𝟙.
+#Rt #c #h #I #G #K #V1 #T2 #H elim (cpg_inv_zero1 … H) -H /2 width=1 by or3_intro0/
+* #z #Y #X1 #X2 #HX12 #HXT2 #H1 #H2 destruct /3 width=5 by or3_intro1, or3_intro2, ex4_2_intro/
+qed-.
+
+lemma cpg_inv_lref1_pair: ∀Rt,c,h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 →
+ (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
+ ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2.
+#Rt #c #h #I #G #L #V #T2 #i #H elim (cpg_inv_lref1 … H) -H /2 width=1 by or_introl/
+* #Z #Y #X #T #HT #HT2 #H destruct /3 width=3 by ex2_intro, or_intror/
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma cpg_fwd_bind1_minus: ∀Rt,c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[Rt, c, h] T → ∀p.
(* Advanced inversion lemmas ************************************************)
+lemma cpx_inv_zero1_pair: ∀h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[h] T2 →
+ T2 = #0 ∨
+ ∃∃V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2.
+#h #I #G #L #V1 #T2 * #c #H elim (cpg_inv_zero1_pair … H) -H *
+/4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/
+qed-.
+
+lemma cpx_inv_lref1_pair: ∀h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[h] T2 →
+ T2 = #(⫯i) ∨
+ ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2.
+#h #I #G #L #V #T2 #i * #c #H elim (cpg_inv_lref1_pair … H) -H *
+/4 width=3 by ex2_intro, ex_intro, or_introl, or_intror/
+qed-.
+
lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
U2 = ⓕ{I}V2.T2
let length l s = max l (String.length s)
+let split s =
+try
+ let i = String.rindex s '.' in
+ if i = 0 then s, "" else
+ String.sub s 0 i, String.sub s i (String.length s - i)
+with Not_found -> s, ""
+
+let compare s1 s2 =
+ let n1, e1 = split s1 in
+ let n2, e2 = split s2 in
+ let e = String.compare e1 e2 in
+ if e = 0 then String.compare n1 n2 else e
+
let write l c s =
let pre, post = if List.mem s !hl then color, normal else "", "" in
let spc = String.make (l - String.length s) ' ' in
let main =
Arg.parse [] process help;
let files = Sys.readdir "." in
- Array.fast_sort String.compare files;
let l = Array.fold_left length 0 files in
if cols < l then failwith "window too small";
+ Array.fast_sort compare files;
let c = Array.fold_left (write l) 0 files in
- if 0 < c && c < cols then print_newline ()
+ if 0 < c && c < cols then print_newline ();
--- /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/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_transition/lfpr_lfpx.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+lemma cpr_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-.
+
+lemma lfpr_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=4 by lfpx_aaa_conf, lfpr_fwd_lfpx/ 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/static/aaa_drops.ma".
+include "basic_2/static/lsuba_aaa.ma".
+include "basic_2/rt_transition/lfpx_fqup.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+(* Note: lemma 500 *)
+(* Basic_2A1: was: cpx_lpx_aaa_conf *)
+lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#h #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
+[ #G #L1 #s #X2 #HX
+ elim (cpx_inv_sort1 … HX) -HX //
+| #I #G #L1 #V1 #B #_ #IH #X2 #HX #Y #HY
+ elim (lfpx_inv_zero_pair_sn … HY) -HY #L2 #V2 #HL12 #HV12 #H destruct
+ elim (cpx_inv_zero1_pair … HX) -HX
+ [ #H destruct /3 width=1 by aaa_zero/
+ | -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
+ ]
+| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY
+ elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct
+ elim (cpx_inv_lref1_pair … HX) -HX
+ [ #H destruct /3 width=1 by aaa_lref/
+ | * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
+ ]
+| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #HX #L2 #HL12
+ elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
+ elim (cpx_inv_abbr1 … HX) -HX *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/
+ | #T2 #HT12 #HXT2 #H destruct -IHV
+ /4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
+ ]
+| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
+ elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
+ elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=2 by lfpx_pair_repl_dx, aaa_abst/
+| #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
+ elim (lfpx_inv_flat … HL12) -HL12 #HV #HT
+ elim (cpx_inv_appl1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
+ | #q #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
+ lapply (IHV … HV12 … HV) -IHV -HV12 -HV #HV2
+ lapply (IHT (ⓛ{q}W2.U2) … HT) -IHT -HT /2 width=1 by cpx_bind/ -L1 #H
+ elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
+ /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/
+ | #q #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
+ lapply (aaa_lifts G L2 … B … (L2.ⓓW2) … HV2) -HV2 /3 width=2 by drops_drop, drops_refl/ #HV2
+ lapply (IHT (ⓓ{q}W2.U2) … HT) -IHT -HT /2 width=1 by cpx_bind/ -L1 #H
+ elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
+ ]
+| #G #L1 #V1 #T1 #A #_ #_ #IHV #IHT #X2 #HX #L2 #HL12
+ elim (lfpx_inv_flat … HL12) -HL12 #HV #HT
+ elim (cpx_inv_cast1 … HX) -HX
+ [ * #V2 #T2 #HV12 #HT12 #H destruct ] /3 width=1 by aaa_cast/
+]
+qed-.
+
+lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/2 width=6 by cpx_aaa_conf_lfpx/ qed-.
+
+lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/2 width=6 by cpx_aaa_conf_lfpx/ 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/static/aaa_lift.ma".
-include "basic_2/static/lsuba_aaa.ma".
-include "basic_2/reduction/lpx_drop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on atomic arity assignment for terms **************************)
-
-(* Note: lemma 500 *)
-lemma cpx_lpx_aaa_conf: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, o] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
-[ #o #L1 #s #X #H
- elim (cpx_inv_sort1 … H) -H // * //
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
- elim (cpx_inv_lref1 … H) -H
- [ #H destruct
- elim (lpx_drop_conf … HLK1 … HL12) -L1 #X #H #HLK2
- elim (lpx_inv_pair1 … H) -H
- #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
- | * #J #Y #Z #V2 #H #HV12 #HV2
- lapply (drop_mono … H … HLK1) -H #H destruct
- elim (lpx_drop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
- elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
- /3 width=8 by aaa_lift, drop_fwd_drop2/
- ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_abbr1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
- | #T2 #HT12 #HT2 #H destruct -IHV1
- /4 width=8 by lpx_pair, aaa_inv_lift, drop_drop/
- ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=1 by lpx_pair, aaa_abst/
-| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_appl1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
- | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
- lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
- lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
- elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/
- | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
- lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by drop_drop/ #HV2
- lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
- elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
- ]
-| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_cast1 … H) -H
- [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
- | -IHV1 /2 width=1 by/
- | -IHT1 /2 width=1 by/
- ]
-]
-qed-.
-
-lemma cpx_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/2 width=7 by cpx_lpx_aaa_conf/ qed-.
-
-lemma lpx_aaa_conf: ∀h,o,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/2 width=7 by cpx_lpx_aaa_conf/ qed-.
-
-lemma cpr_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/3 width=5 by cpx_aaa_conf, cpr_cpx/ qed-.
-
-lemma lpr_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/3 width=5 by lpx_aaa_conf, lpr_lpx/ qed-.
cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma
-lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma
+lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma
cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
cpr.ma cpr_drops.ma
-lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_lfpx.ma lfpr_lfpr.ma
+lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma
}
]
[ { "context-sensitive rt-reduction" * } {
- [ "lpx_lleq" + "lpx_aaa" * ]
+ [ "lpx_lleq" * ]
[ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
}
]
*)
[ { "t-bound context-sensitive rt-transition" * } {
- [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_lfpx" + "lfpr_lfpr" * ]
+ [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
[ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
[ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
}
]
[ { "uncounted context-sensitive rt-transition" * } {
- [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" * ]
+ [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
}
]
projects / helm.git / commitdiff