H=@
-TAGS = www up-html \
+TAGS = www up-html up-css up-images up-download \
lint-xml index lddl install-xml \
test-html html install-html \
install-jed install-bib install-2 install-1 install-coq \
$(H)scp $< $(DOWNDIR)
up-html:
- @echo " UPDATE $(RHOMEDIR)/html"
+ @echo " UPDATE $(RHOMEDIR)/html/"
$(H)scp -q -r html $(RHOMEDIR)
+up-css:
+ @echo " UPDATE $(RHOMEDIR)/css/"
+ $(H)scp -q -r css $(RHOMEDIR)
+
+up-images:
+ @echo " UPDATE $(RHOMEDIR)/images/"
+ $(H)scp -q -r images $(RHOMEDIR)
+
up-download:
- @echo " UPDATE $(RHOMEDIR)/download"
+ @echo " UPDATE $(RHOMEDIR)/download/"
$(H)scp -q -r download $(RHOMEDIR)
%.ld:
--- /dev/null
+@charset "UTF-8";
+
+/* menus ********************************************************************/
+
+.text {
+ display: inline-block;
+ list-style: none;
+ margin: 0;
+ padding: 0;
+ white-space: nowrap;
+}
+
+.menu {
+ display: none;
+ border-style: solid;
+ border-width: thin;
+ position: absolute;
+}
+
+.menu:target {
+ display: inline-block;
+}
+
+/* buttons ******************************************************************/
+
+.button {
+ color: inherit;
+ background-color: inherit;
+ border-style: none;
+ margin: initial;
+ padding: initial;
+}
+
+.button:hover {
+ text-decoration: underline;
+}
+
+/* anchors ******************************************************************/
+
+a:link {
+ text-decoration: initial;
+ color: inherit;
+}
+
+/* visited link */
+a:visited {
+ text-decoration: initial;
+ color: inherit;
+}
+
+/* mouse over link */
+a:hover {
+ text-decoration: underline;
+ color: inherit;
+}
+
+/* selected link */
+a:active {
+ text-decoration: underline;
+ color: inherit;
+}
+
+/* displays *****************************************************************/
+
+.block {
+ display: block;
+}
+
+.inline {
+ display: inline;
+}
+
+/* font families ************************************************************/
+
+.monospace {
+ font-family:monospace;
+}
+
+/* line heights *************************************************************/
+
+.l_150 {
+ line-height:150%;
+}
+
+/* font sizes ***************************************************************/
+
+.t_130 {
+ font-size: 130%;
+}
+
+/* foreground colors (equalized to gray 8F) *********************************/
+
+.f_gray {
+ color:#8F8F8F;
+}
+
+.f_wine {
+ color:#FF52A0;
+}
+
+.f_magenta {
+ color:#FF41FF;
+}
+
+.f_prune {
+ color:#C65DFF;
+}
+
+.f_blue {
+ color:#8181FF;
+}
+
+.f_sky {
+ color:#04C0FF;
+}
+
+.f_cyan {
+ color:#00CCCC;
+}
+
+.f_water {
+ color:#00D88C;
+}
+
+.f_green {
+ color:#00F200;
+}
+
+.f_grass {
+ color:#83AF00;
+}
+
+.f_yellow {
+ color:#A0A000;
+}
+
+.f_orange {
+ color:#C09000;
+}
+
+.f_red {
+ color:#FF5F5F;
+}
+
+.f_black {
+ color:#000000;
+}
+
+/* background colors (equalized to gray D3) *********************************/
+
+.b_white {
+ background-color:#FFFFFF;
+}
+
+.b_gray {
+ background-color:#D3D3D3;
+}
+
+.b_wine {
+ background-color:#FFBBD9;
+}
+
+.b_magenta {
+ background-color:#FFB4FF;
+}
+
+.b_prune {
+ background-color:#E8BFFF;
+}
+
+.b_blue {
+ background-color:#CDCDFF;
+}
+
+.b_sky {
+ background-color:#9CE6FF;
+}
+
+.b_cyan {
+ background-color:#6CFFFF;
+}
+
+.b_water {
+ background-color:#7DFFD1;
+}
+
+.b_green {
+ background-color:#93FF93;
+}
+
+.b_grass {
+ background-color:#C3FF11;
+}
+
+.b_yellow {
+ background-color:#EDED00;
+}
+
+.b_orange {
+ background-color:#FFD454;
+}
+
+.b_red {
+ background-color:#FFC0C0;
+}
+
+/* background colors (equalized to gray EB) *********************************/
+
+.b_gray_EB {
+ background-color:#EBEBEB;
+}
href="{$baseurl}css/xhtbl.css"
/>
<link rel="shortcut icon"
- href="{$baseurl}images/crux_16.ico"
+ href="{$baseurl}images/crux_32.ico"
/>
</head><body lang="en-US">
<div class="spacer"><xsl:call-template name="img"/></div>
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌η[ break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PConvEta $h $G $L $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 "ground_2/xoa/ex_2_4.ma".
+include "basic_2/notation/relations/pconveta_5.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
+
+(* avtivate genv *)
+inductive cpce (h): relation4 genv lenv term term ≝
+| cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
+| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
+| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
+ cpce h G (K.ⓛV) (#0) (#0)
+| cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T →
+ cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1)
+| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
+ ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
+| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
+ cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
+ cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+| cpce_flat: ∀I,G,L,V1,V2,T1,T2.
+ cpce h G L V1 V2 → cpce h G L T1 T2 →
+ cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+ "context-sensitive parallel eta-conversion (term)"
+ 'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpce_inv_sort_sn (h) (G) (L) (X2):
+ ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
+#h #G #Y #X2 #s0
+@(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
+[ #G #L #s #_ //
+| #G #K #V #_ //
+| #n #G #K #V #s #_ #_ //
+| #n #p #G #K #V #W #T #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H destruct
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
+]
+qed-.
+
+lemma cpce_inv_ldef_sn (h) (G) (K) (X2):
+ ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
+#h #G #Y #X2 #X
+@(insert_eq_0 … (Y.ⓓX)) #Y1
+@(insert_eq_0 … (#0)) #X1
+* -G -Y1 -X1 -X2
+[ #G #L #s #_ #_ //
+| #G #K #V #_ #_ //
+| #n #G #K #V #s #_ #_ #_ //
+| #n #p #G #K #V #W #T #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_ldec_sn (h) (G) (K) (X2):
+ ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 →
+ ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2
+ | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2.
+#h #G #Y #X2 #X
+@(insert_eq_0 … (Y.ⓛX)) #Y1
+@(insert_eq_0 … (#0)) #X1
+* -G -Y1 -X1 -X2
+[ #G #L #s #H #_ destruct
+| #G #K #V #_ #H destruct
+| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/
+| #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/
+| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_lref_sn (h) (G) (K) (X2):
+ ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
+ ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2.
+#h #G #Y #X2 #Z #j
+@(insert_eq_0 … (Y.ⓘ{Z})) #Y1
+@(insert_eq_0 … (#↑j)) #X1
+* -G -Y1 -X1 -X2
+[ #G #L #s #H #_ destruct
+| #G #K #V #H #_ destruct
+| #n #G #K #V #s #_ #H #_ destruct
+| #n #p #G #K #V #W #T #_ #H #_ destruct
+| #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_bind_sn (h) (G) (K) (X2):
+ ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
+ ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
+#h #G #Y #X2 #q #Z #U #X
+@(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2
+[ #G #L #s #H destruct
+| #G #K #V #H destruct
+| #n #G #K #V #s #_ #H destruct
+| #n #p #G #K #V #W #T #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H destruct
+| #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
+]
+qed-.
+
+lemma cpce_inv_flat_sn (h) (G) (L) (X2):
+ ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
+ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2.
+#h #G #Y #X2 #Z #U #X
+@(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
+[ #G #L #s #H destruct
+| #G #K #V #H destruct
+| #n #G #K #V #s #_ #H destruct
+| #n #p #G #K #V #W #T #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H destruct
+| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
+| #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
]
class "blue"
[ { "rt-conversion" * } {
+ [ { "context-sensitive parallel eta-conversion" * } {
+ [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
+ }
+ ]
[ { "context-sensitive parallel r-conversion" * } {
[ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
}
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (2, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) }.
+
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+include "ground_2/notation/xoa/ex_2_4.ma".
+
+(* multiple existental quantifier (2, 4) *)
+
+inductive ex2_4 (A0,A1,A2,A3:Type[0]) (P0,P1:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex2_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → ex2_4 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 4)" 'Ex4 P0 P1 = (ex2_4 ? ? ? ? P0 P1).
+
<key name="objects">ground_2/xoa</key>
<key name="notations">ground_2/notation/xoa</key>
<key name="include">basics/pts.ma</key>
+ <key name="ex">2 4</key>
<key name="ex">5 1</key>
<key name="ex">5 7</key>
<key name="ex">9 3</key>
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌η break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PConvEta $G $L $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 "static_2/notation/relations/pconveta_4.ma".
-include "static_2/relocation/lifts.ma".
-include "static_2/static/aaa.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
-
-(* avtivate genv *)
-inductive cpce: relation4 genv lenv term term ≝
-| cpce_sort: ∀G,L,s. cpce G L (⋆s) (⋆s)
-| cpce_abbr: ∀G,K,V. cpce G (K.ⓓV) (#0) (#0)
-| cpce_abst: ∀G,K,W,B,A. ⦃G,K⦄ ⊢ W ⁝ ②B.A →
- cpce G (K.ⓛW) (#0) (+ⓛW.ⓐ#0.#1)
-| cpce_lref: ∀I,G,K,T,U,i. cpce G K (#i) T →
- ⬆*[1] T ≘ U → cpce G (K.ⓘ{I}) (#↑i) U
-| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
- cpce G K V1 V2 → cpce G (K.ⓑ{I}V1) T1 T2 →
- cpce G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
-| cpce_flat: ∀I,G,L,V1,V2,T1,T2.
- cpce G L V1 V2 → cpce G L T1 T2 →
- cpce G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-.
-
-interpretation
- "context-sensitive parallel eta-conversion (term)"
- 'PConvEta G L T1 T2 = (cpce G L T1 T2).
]
class "green"
[ { "static typing" * } {
- [ { "context-sensitive parallel eta-conversion" * } {
- [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η ? )" * ]
- }
- ]
[ { "generic reducibility" * } {
[ [ "restricted refinement for lenvs" ] "lsubc" + "( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
[ [ "candidates" ] "gcp_cr" + "( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
projects / helm.git / commitdiff