- property S5 of the candidates of reducibility almost proved ...
--- /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 "Ground_2/tri.ma".
+include "Basic_2/substitution/lift.ma".
+include "Apps_2/functional/notation.ma".
+
+(* RELOCATION ***************************************************************)
+
+let rec flift d e U on U ≝ match U with
+[ TAtom I ⇒ match I with
+ [ Sort _ ⇒ U
+ | LRef i ⇒ #(tri … i d i (i + e) (i + e))
+ | GRef _ ⇒ U
+ ]
+| TPair I V T ⇒ match I with
+ [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T)
+ | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T)
+ ]
+].
+
+interpretation "functional relocation" 'Lift d e T = (flift d e T).
+
+(* Main properties **********************************************************)
+
+theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T.
+#T elim T -T
+[ * #i #d #e //
+ elim (lt_or_eq_or_gt i d) #Hid normalize
+ [ >(tri_lt ?????? Hid) /2 width=1/
+ | /2 width=1/
+ | >(tri_gt ?????? Hid) /3 width=2/
+ ]
+| * /2/
+]
+qed.
+
+(* Main inversion properties ************************************************)
+
+theorem flift_inv_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2.
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
+[ #i #d #e #Hid >(tri_lt ?????? Hid) //
+| #i #d #e #Hid
+ elim (le_to_or_lt_eq … Hid) -Hid #Hid
+ [ >(tri_gt ?????? Hid) //
+ | destruct //
+ ]
+]
+qed-.
+
+(* Derived properties *******************************************************)
+
+lemma flift_join: ∀e1,e2,T. ⇧[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
+#e1 #e2 #T
+lapply (flift_lift T 0 (e1+e2)) #H
+elim (lift_split … H e1 e1 ? ? ?) -H // #U #H
+>(flift_inv_lift … H) -H //
+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 "functional" COMPONENT ********************************)
+
+notation "hvbox( ↑ [ d , break e ] break T )"
+ non associative with precedence 55
+ for @{ 'Lift $d $e $T }.
+
+notation "hvbox( [ d ← break V ] break T )"
+ non associative with precedence 55
+ for @{ 'Subst $V $d $T }.
+
+notation "hvbox( T1 ⇨ break T2 )"
+ non associative with precedence 45
+ for @{ 'SRed $T1 $T2 }.
--- /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/grammar/term_vector.ma".
+include "Basic_2/grammar/genv.ma".
+
+(* REDUCTION AND TYPE MACHINE ***********************************************)
+
+(* machine local environment *)
+inductive xenv: Type[0] ≝
+| XAtom: xenv (* empty *)
+| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
+.
+
+interpretation "atom (ext. local environment)"
+ 'Star = XAtom.
+
+interpretation "environment construction (quad)"
+ 'DxItem4 L I u K V = (XQuad L I u K V).
+
+(* machine stack *)
+definition stack: Type[0] ≝ list2 xenv term.
+
+(* machine status *)
+record rtm: Type[0] ≝
+{ rg: genv; (* global environment *)
+ ru: nat; (* current de Bruijn's level *)
+ re: xenv; (* extended local environment *)
+ rs: stack; (* application stack *)
+ rt: term (* code *)
+}.
+
+(* initial state *)
+definition rtm_i: genv → term → rtm ≝
+ λG,T. mk_rtm G 0 (⋆) (⟠) T.
+
+(* update code *)
+definition rtm_t: rtm → term → rtm ≝
+ λM,T. match M with
+ [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T
+ ].
+
+(* update closure *)
+definition rtm_u: rtm → xenv → term → rtm ≝
+ λM,E,T. match M with
+ [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T
+ ].
+
+(* get global environment *)
+definition rtm_g: rtm → genv ≝
+ λM. match M with
+ [ mk_rtm G _ _ _ _ ⇒ G
+ ].
+
+(* get local reference level *)
+definition rtm_l: rtm → nat ≝
+ λM. match M with
+ [ mk_rtm _ u E _ _ ⇒ match E with
+ [ XAtom ⇒ u
+ | XQuad _ _ u _ _ ⇒ u
+ ]
+ ].
+
+(* get stack *)
+definition rtm_s: rtm → stack ≝
+ λM. match M with
+ [ mk_rtm _ _ _ S _ ⇒ S
+ ].
+
+(* get code *)
+definition rtm_c: rtm → term ≝
+ λM. match M with
+ [ mk_rtm _ _ _ _ T ⇒ 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 "Apps_2/functional/rtm.ma".
+
+(* REDUCTION AND TYPE MACHINE ***********************************************)
+
+(* transitions *)
+inductive rtm_step: relation rtm ≝
+| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i.
+ rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1)))
+ (mk_rtm G u E S (#i))
+| rtm_ldelta: ∀G,u,E,t,F,V,S.
+ rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0))
+ (mk_rtm G u F S V)
+| rtm_ltype : ∀G,u,E,t,F,V,S.
+ rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
+ (mk_rtm G u F S V)
+| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
+ rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
+ (mk_rtm G u E S (§p))
+| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
+ rtm_step (mk_rtm (G. ⓓV) u E S (§p))
+ (mk_rtm G u E S V)
+| rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
+ rtm_step (mk_rtm (G. ⓛV) u E S (§p))
+ (mk_rtm G u E S V)
+| rtm_tau : ∀G,u,E,S,W,T.
+ rtm_step (mk_rtm G u E S (ⓣW. T))
+ (mk_rtm G u E S T)
+| rtm_appl : ∀G,u,E,S,V,T.
+ rtm_step (mk_rtm G u E S (ⓐV. T))
+ (mk_rtm G u E ({E, V} :: S) T)
+| rtm_beta : ∀G,u,E,F,V,S,W,T.
+ rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
+ (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
+| rtm_push : ∀G,u,E,W,T.
+ rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
+ (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
+| rtm_theta : ∀G,u,E,S,V,T.
+ rtm_step (mk_rtm G u E S (ⓓV. T))
+ (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
+.
+
+interpretation "sequential reduction (RTM)"
+ 'SRed O1 O2 = (rtm_step O1 O2).
--- /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/delift_lift.ma".
+include "Apps_2/functional/lift.ma".
+
+(* CORE SUBSTITUTION ********************************************************)
+
+let rec fsubst W d U on U ≝ match U with
+[ TAtom I ⇒ match I with
+ [ Sort _ ⇒ U
+ | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
+ | GRef _ ⇒ U
+ ]
+| TPair I V T ⇒ match I with
+ [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
+ | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
+ ]
+].
+
+interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
+
+(* Main properties **********************************************************)
+
+theorem fsubst_delift: ∀K,V,T,L,d.
+ ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
+#K #V #T elim T -T
+[ * #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_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)
+ | -HLK >(tri_gt ?????? Hid) /3 width=3/
+ ]
+| * /3 width=1/ /4 width=1/
+]
+qed.
+
+(* Main inversion properties ************************************************)
+
+theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
+ L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
+#K #V #T1 elim T1 -T1
+[ * #i #L #T2 #d #HLK #H
+ [ -HLK >(delift_fwd_sort1 … H) -H //
+ | elim (lt_or_eq_or_gt i d) #Hid normalize
+ [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/
+ | destruct
+ elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
+ >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
+ | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/
+ ]
+ | -HLK >(delift_fwd_gref1 … H) -H //
+ ]
+| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
+ [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
+ | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
+ ]
+]
+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/lift_vector.ma".
+include "Basic_2/computation/cprs_tstc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Vector form of forward lemmas involving same top term constructor ********)
+
+lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡ U →
+ ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U.
+#L #V1s #V2s * -V1s -V2s /3 width=1/
+#V1s #V2s #V1a #V2a #HV12a * -V1s -V2s /2 width=1 by cpr_fwd_theta/ -HV12a
+#V1s #V2s #V1b #V2b #_ #_ #V #U #T #H
+elim (cpr_inv_appl1_simple … H ?) -H //
+#V0 #T0 #_ #_ #H destruct /2 width=1/
+qed-.
+
+axiom cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U →
+ ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U.
\ No newline at end of file
(**************************************************************************)
include "Basic_2/computation/acp_aaa.ma".
-include "Basic_2/computation/csn_cr.ma".
+include "Basic_2/computation/csn_lcpr_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-(* Main properties **********************************************************)
+(* Properties concerning atomic arity assignment ****************************)
-theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T.
+lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
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/computation/acp_cr.ma".
-include "Basic_2/computation/csn_lcpr.ma".
-include "Basic_2/computation/csn_vector.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Advanced properties ******************************************************)
-(*
-
-(* Basic_1: was only: sn3_appl_appls *)
-lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 →
- (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
- 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
-#L *
-[ #V #T1 #HV
- @csn_appl_simple_tstc //
-| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1
- @csn_appl_simple_tstc // -HV
- [ @H2T1
-]
-qed.
-
-lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
-#L #V1s #V2s * -V1s -V2s /2 width=1/
-#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/
-#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV
-lapply (csn_appl_theta … HV12 … H) -H -HV12 #H
-lapply (csn_fwd_pair_sn … H) #HV1
-@csn_appl_simple // #X #H1 #H2
-whd in ⊢ (? ? %);
-*)
-(*
-lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
-#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/
-*)
-
-axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* 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 "Basic_2/computation/acp_cr.ma".
+include "Basic_2/computation/cprs_tstc_vector.ma".
+include "Basic_2/computation/csn_lcpr.ma".
+include "Basic_2/computation/csn_vector.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
+
+(* Advanced properties ******************************************************)
+(*
+(* Basic_1: was only: sn3_appl_appls *)
+lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 →
+ (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+ 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
+#L *
+[ #V #T1 #HV
+ @csn_appl_simple_tstc //
+| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1
+ @csn_appl_simple_tstc // -HV
+ [ @H2T1
+]
+qed.
+*)
+lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s * -V1s -V2s /2 width=1/
+#V1s #V2s #V1 #V2 #HV12 #H
+generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
+elim H -V1s -V2s /2 width=3/
+#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV
+lapply (csn_appl_theta … HW12 … H) -H -HW12 #H
+lapply (csn_fwd_pair_sn … H) #HW1
+lapply (csn_fwd_flat_dx … H) #H1
+@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
+elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+[ -H #H elim (H2 ?) -H2 //
+| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
+]
+qed.
+(*
+theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).
+@mk_acr //
+[
+|
+|
+| #L #V1 #V2 #HV12 #V #T #H #HVT
+ @(csn_applv_theta … HV12) -HV12 //
+ @(csn_abbr) //
+|
+| @csn_lift
+]
+qed.
+*)
+axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).
(* Advanced properties ******************************************************)
-lemma csn_acp: acp cpr (eq …) (csn …).
-@mk_acp
-[ /2 width=1/
-| /2 width=3/
-| /2 width=5/
-| @cnf_lift
-]
-qed.
-
(* Basic_1: was: sn3_abbr *)
lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i.
#L #K #V #i #HLK #HV
@IHT1 -IHT1 // -HLT02 /2 width=1/
]
qed.
+
+(* Main properties **********************************************************)
+
+theorem csn_acp: acp cpr (eq …) (csn …).
+@mk_acp
+[ /2 width=1/
+| /2 width=3/
+| /2 width=5/
+| @cnf_lift
+]
+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 "Ground_2/tri.ma".
-include "Basic_2/substitution/lift.ma".
-
-(* RELOCATION ***************************************************************)
-
-let rec flift d e U on U ≝ match U with
-[ TAtom I ⇒ match I with
- [ Sort _ ⇒ U
- | LRef i ⇒ #(tri … i d i (i + e) (i + e))
- | GRef _ ⇒ U
- ]
-| TPair I V T ⇒ match I with
- [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T)
- | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T)
- ]
-].
-
-interpretation "functional relocation" 'Lift d e T = (flift d e T).
-
-(* Main properties **********************************************************)
-
-theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T.
-#T elim T -T
-[ * #i #d #e //
- elim (lt_or_eq_or_gt i d) #Hid normalize
- [ >(tri_lt ?????? Hid) /2 width=1/
- | /2 width=1/
- | >(tri_gt ?????? Hid) /3 width=2/
- ]
-| * /2/
-]
-qed.
-
-(* Main inversion properties ************************************************)
-
-theorem flift_inv_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2.
-#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
-[ #i #d #e #Hid >(tri_lt ?????? Hid) //
-| #i #d #e #Hid
- elim (le_to_or_lt_eq … Hid) -Hid #Hid
- [ >(tri_gt ?????? Hid) //
- | destruct //
- ]
-]
-qed-.
-
-(* Derived properties *******************************************************)
-
-lemma flift_join: ∀e1,e2,T. ⇧[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
-#e1 #e2 #T
-lapply (flift_lift T 0 (e1+e2)) #H
-elim (lift_split … H e1 e1 ? ? ?) -H // #U #H
->(flift_inv_lift … H) -H //
-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/grammar/term_vector.ma".
-include "Basic_2/grammar/genv.ma".
-
-(* REDUCTION AND TYPE MACHINE ***********************************************)
-
-(* machine local environment *)
-inductive xenv: Type[0] ≝
-| XAtom: xenv (* empty *)
-| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
-.
-
-interpretation "atom (ext. local environment)"
- 'Star = XAtom.
-
-interpretation "environment construction (quad)"
- 'DxItem4 L I u K V = (XQuad L I u K V).
-
-(* machine stack *)
-definition stack: Type[0] ≝ list2 xenv term.
-
-(* machine status *)
-record rtm: Type[0] ≝
-{ rg: genv; (* global environment *)
- ru: nat; (* current de Bruijn's level *)
- re: xenv; (* extended local environment *)
- rs: stack; (* application stack *)
- rt: term (* code *)
-}.
-
-(* initial state *)
-definition rtm_i: genv → term → rtm ≝
- λG,T. mk_rtm G 0 (⋆) (⟠) T.
-
-(* update code *)
-definition rtm_t: rtm → term → rtm ≝
- λM,T. match M with
- [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T
- ].
-
-(* update closure *)
-definition rtm_u: rtm → xenv → term → rtm ≝
- λM,E,T. match M with
- [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T
- ].
-
-(* get global environment *)
-definition rtm_g: rtm → genv ≝
- λM. match M with
- [ mk_rtm G _ _ _ _ ⇒ G
- ].
-
-(* get local reference level *)
-definition rtm_l: rtm → nat ≝
- λM. match M with
- [ mk_rtm _ u E _ _ ⇒ match E with
- [ XAtom ⇒ u
- | XQuad _ _ u _ _ ⇒ u
- ]
- ].
-
-(* get stack *)
-definition rtm_s: rtm → stack ≝
- λM. match M with
- [ mk_rtm _ _ _ S _ ⇒ S
- ].
-
-(* get code *)
-definition rtm_c: rtm → term ≝
- λM. match M with
- [ mk_rtm _ _ _ _ T ⇒ 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 "Basic_2/functional/rtm.ma".
-
-(* REDUCTION AND TYPE MACHINE ***********************************************)
-
-(* transitions *)
-inductive rtm_step: relation rtm ≝
-| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i.
- rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1)))
- (mk_rtm G u E S (#i))
-| rtm_ldelta: ∀G,u,E,t,F,V,S.
- rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0))
- (mk_rtm G u F S V)
-| rtm_ltype : ∀G,u,E,t,F,V,S.
- rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
- (mk_rtm G u F S V)
-| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
- rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
- (mk_rtm G u E S (§p))
-| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
- rtm_step (mk_rtm (G. ⓓV) u E S (§p))
- (mk_rtm G u E S V)
-| rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
- rtm_step (mk_rtm (G. ⓛV) u E S (§p))
- (mk_rtm G u E S V)
-| rtm_tau : ∀G,u,E,S,W,T.
- rtm_step (mk_rtm G u E S (ⓣW. T))
- (mk_rtm G u E S T)
-| rtm_appl : ∀G,u,E,S,V,T.
- rtm_step (mk_rtm G u E S (ⓐV. T))
- (mk_rtm G u E ({E, V} :: S) T)
-| rtm_beta : ∀G,u,E,F,V,S,W,T.
- rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
- (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
-| rtm_push : ∀G,u,E,W,T.
- rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
- (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
-| rtm_theta : ∀G,u,E,S,V,T.
- rtm_step (mk_rtm G u E S (ⓓV. T))
- (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
-.
-
-interpretation "sequential reduction (RTM)"
- 'SRed O1 O2 = (rtm_step O1 O2).
+++ /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/delift_lift.ma".
-include "Basic_2/functional/lift.ma".
-
-(* CORE SUBSTITUTION ********************************************************)
-
-let rec fsubst W d U on U ≝ match U with
-[ TAtom I ⇒ match I with
- [ Sort _ ⇒ U
- | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
- | GRef _ ⇒ U
- ]
-| TPair I V T ⇒ match I with
- [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
- | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
- ]
-].
-
-interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
-
-(* Main properties **********************************************************)
-
-theorem fsubst_delift: ∀K,V,T,L,d.
- ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
-#K #V #T elim T -T
-[ * #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_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)
- | -HLK >(tri_gt ?????? Hid) /3 width=3/
- ]
-| * /3 width=1/ /4 width=1/
-]
-qed.
-
-(* Main inversion properties ************************************************)
-
-theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
- L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
-#K #V #T1 elim T1 -T1
-[ * #i #L #T2 #d #HLK #H
- [ -HLK >(delift_fwd_sort1 … H) -H //
- | elim (lt_or_eq_or_gt i d) #Hid normalize
- [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/
- | destruct
- elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
- lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
- >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
- | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/
- ]
- | -HLK >(delift_fwd_gref1 … H) -H //
- ]
-| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
- [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
- | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
- ]
-]
-qed-.
lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False.
/2 width=6/ qed-.
+
+lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J.
+* /2 width=2/ #I #V #T #H
+elim (simple_inv_bind … H)
+qed-.
]
qed.
-axiom simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J.
-
lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2].
#T1 #T2 * -T1 -T2 //
#I #V1 #V2 #T1 #T2 #H
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
-(* Functional ***************************************************************)
+(* Conversion ***************************************************************)
-notation "hvbox( ↑ [ d , break e ] break T )"
- non associative with precedence 55
- for @{ 'Lift $d $e $T }.
+notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )"
+ non associative with precedence 45
+ for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( [ d ← break V ] break T )"
- non associative with precedence 55
- for @{ 'Subst $V $d $T }.
+(* Congruence ***************************************************************)
-notation "hvbox( T1 ⇨ break T2 )"
+notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )"
non associative with precedence 45
- for @{ 'SRed $T1 $T2 }.
+ for @{ 'PConvStar $L $T1 $T2 }.
CONF = Ground_2/xoa.conf.xml
TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma
-PACKAGES = Ground_2 Basic_2
+PACKAGES = Ground_2 Basic_2 Apps_2
all:
%.stats: CHARS = $(shell cat $(MAS) | wc -c)
-%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l)
-%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l)
+%.stats: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l)
+%.stats: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l)
+%.stats: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l)
%.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l)
%.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l)
+%.stats: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l)
%.stats: TBL = ld_$*_sum
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
@printf ' %-10s' ''
@printf '\x1B[0m\n'
- @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl
- @printf 'table {\n' >> $*/$(TBL).tbl
- @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl
- @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl
- @printf ' ]\n' >> $*/$(TBL).tbl
- @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl
- @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl
- @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl
- @printf ' ]\n' >> $*/$(TBL).tbl
- @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl
- @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl
- @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl
- @printf ' ]\n' >> $*/$(TBL).tbl
- @printf '}\n\n' >> $*/$(TBL).tbl
- @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl
- @printf 'class "plane" { 1 } { 3 } \n\n' >> $*/$(TBL).tbl
- @printf 'class "number" { 2 } { 4 } \n\n' >> $*/$(TBL).tbl
+ @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl
+ @printf 'table {\n' >> $*/$(TBL).tbl
+ @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl
+ @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl
+ @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "total" "$(P3)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl
+ @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' [ "total" "$(C3)" * ]\n' >> $*/$(TBL).tbl
+ @printf ' ]\n' >> $*/$(TBL).tbl
+ @printf '}\n\n' >> $*/$(TBL).tbl
+ @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl
+ @printf 'class "plane" { 1 } { 3 } { 5 } \n\n' >> $*/$(TBL).tbl
+ @printf 'class "number" { 2 } { 4 } { 6 } \n\n' >> $*/$(TBL).tbl
projects / helm.git / commitdiff