--- /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/syntax/bind.ma".
+include "basic_2/static/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES FOR BINDERS *****************************)
+
+inductive freesb (L): relation2 β¦ β
+| freesb_pair: βI,V,f. L β’ π
*β¦Vβ¦ β‘ f β freesb L (BPair I V) f
+| freesb_unit: βI,f. πβ¦fβ¦ β freesb L (BUnit I) f
+.
+
+interpretation
+ "context-sensitive free variables (binder)"
+ 'FreeStar L I f = (freesb L I f).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact frees_inv_pair_aux: βL,Z,f. L β’ π
*β¦Zβ¦ β‘ f β
+ βI,V. Z = BPair I V β L β’ π
*β¦Vβ¦ β‘ f.
+#L #Z #f * -Z -f
+[ #I #V #f #Hf #Z #X #H destruct //
+| #I #f #_ #Z #X #H destruct
+]
+qed-.
+
+lemma frees_inv_pair: βL,I,V,f. L β’ π
*β¦BPair I Vβ¦ β‘ f β L β’ π
*β¦Vβ¦ β‘ f.
+/2 width=4 by frees_inv_pair_aux/ qed-.
+
+fact frees_inv_unit_aux: βL,Z,f. L β’ π
*β¦Zβ¦ β‘ f β
+ βI. Z = BUnit I β πβ¦fβ¦.
+#L #Z #f * -Z -f
+[ #I #V #f #_ #Z #H destruct
+| #I #f #Hf #Z #H destruct //
+]
+qed-.
+
+lemma frees_inv_unit: βL,I,f. L β’ π
*β¦BUnit Iβ¦ β‘ f β πβ¦fβ¦.
+/2 width=5 by frees_inv_unit_aux/ qed-.
--- /dev/null
+(* Note: this does not hold since L = Y.β§, U = #0, f = β«―g requires T = #(-1) *)
+lemma frees_inv_drops: βf2,L,U. L β’ π
*β¦Uβ¦ β‘ f2 β
+ βf,K. β¬*[β, f] L β‘ K β βf1. f ~β f1 β‘ f2 β
+ ββT. K β’ π
*β¦Tβ¦ β‘ f1 & β¬*[f] T β‘ U.
+#f2 #L #U #H lapply (frees_fwd_isfin β¦ H) elim H -f2 -L -U
+[ #f2 #I #Hf2 #_ #f #K #H1 #f1 #H2
+ lapply (coafter_fwd_isid2 β¦ H2 ??) -H2 // -Hf2 #Hf1
+ elim (drops_inv_atom1 β¦ H1) -H1 #H #Hf destruct
+ /4 width=3 by frees_atom, lifts_refl, ex2_intro/
+| #f2 #I #L #s #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push β¦ Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp β¦ H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 β¦ H1) -H1 #Z #K #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 β¦ H1) -H1 #HLK
+ ]
+ elim (IH β¦ HLK β¦ Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inv_sort2 β¦ HX) -HX #H destruct
+ /3 width=3 by frees_sort, lifts_sort, ex2_intro/
+| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_inv_next β¦ Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxn β¦ H2) -H2 [ |*: // ] #g #g1 #Hf2 #H0 #H destruct
+ elim (drops_inv_skip1 β¦ H1) -H1 #J #K #HLK #HJI #H destruct
+ elim (liftsb_inv_pair_dx β¦ HJI) -HJI #V #HVW #H destruct
+ elim (IH β¦ HLK β¦ Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inj β¦ HX β¦ HVW) -W #H destruct
+ /3 width=3 by frees_zero, lifts_lref, ex2_intro/
+| #f2 #L #Hf2 #_ #f #Y #H1 #f1 #H2
+ lapply (coafter_fwd_isid2 β¦ H2 ??) -H2 // -Hf2 #Hf1
+ elim (pn_split f) * #g #H destruct
+ [ elim (drops_inv_skip1 β¦ H1) -H1 #J #K #HLK #HJI #H destruct
+ lapply (liftsb_inv_unit_dx β¦ HJI) -HJI #H destruct
+ /3 width=3 by frees_void, lifts_lref, ex2_intro/
+ | lapply (drops_inv_drop1 β¦ H1) -H1 #H1
+| #f2 #I #L #j #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push β¦ Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp β¦ H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 β¦ H1) -H1 #J #K #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 β¦ H1) -H1 #HLK (* cannot continue *)
+ ]
+ elim (IH β¦ HLK β¦ Hf2) -L // -f2 #X #Hg1 #HX
+ elim (lifts_inv_lref2 β¦ HX) -HX #i #Hij #H destruct
+ /4 width=7 by frees_lref, lifts_lref, at_S1, at_next, ex2_intro/
+| #f2 #I #L #l #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push β¦ Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp β¦ H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 β¦ H1) -H1 #J #K #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 β¦ H1) -H1 #HLK
+ ]
+ elim (IH β¦ HLK β¦ Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inv_gref2 β¦ HX) -HX #H destruct
+ /3 width=3 by frees_gref, lifts_gref, ex2_intro/
+| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #f1 #H2
+ elim (sor_inv_isfin3 β¦ H1f2) // #H1f2W #H
+ lapply (isfin_inv_tl β¦ H) -H #H1f2U
+ elim (coafter_inv_sor β¦ H2 β¦ H1f2) -H2 -H1f2 // #f1W #f1U #H2f2W #H #Hf1
+ elim (coafter_inv_tl0 β¦ H) -H #g1 #H2f2U #H destruct
+ elim (IHW β¦ H1 β¦ H2f2W) -IHW -H2f2W // -H1f2W #V #Hf1W #HVW
+ elim (IHU β¦ H2f2U) -IHU -H2f2U
+ /3 width=5 by frees_bind, drops_skip, lifts_bind, ext2_pair, ex2_intro/
+| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #f1 #H2
+ elim (sor_inv_isfin3 β¦ H1f2) // #H1f2W #H1f2U
+ elim (coafter_inv_sor β¦ H2 β¦ H1f2) -H2 -H1f2 // #f1W #f1U #H2f2W #H2f2U #Hf1
+ elim (IHW β¦ H1 β¦ H2f2W) -IHW -H2f2W // -H1f2W
+ elim (IHU β¦ H1 β¦ H2f2U) -L -H2f2U
+ /3 width=5 by frees_flat, lifts_flat, ex2_intro/
+]
+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/syntax/bind.ma".
+
+(* EXTENSION TO BINDERS OF A RELATION FOR TERMS *****************************)
+
+inductive ext2 (R:relation term): relation bind β
+| ext2_unit: βI. ext2 R (BUnit I) (BUnit I)
+| ext2_pair: βI,V1,V2. R V1 V2 β ext2 R (BPair I V1) (BPair I V2)
+.
+
+(* Basic_inversion lemmas **************************************************)
+
+fact ext2_inv_unit_sn_aux: βR,Z1,Z2. ext2 R Z1 Z2 β
+ βI. Z1 = BUnit I β Z2 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_sn: βR,I,Z2. ext2 R (BUnit I) Z2 β Z2 = BUnit I.
+/2 width=4 by ext2_inv_unit_sn_aux/ qed-.
+
+fact ext2_inv_pair_sn_aux: βR,Z1,Z2. ext2 R Z1 Z2 β
+ βI,V1. Z1 = BPair I V1 β
+ ββV2. R V1 V2 & Z2 = BPair I V2.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W1 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_sn: βR,Z2,I,V1. ext2 R (BPair I V1) Z2 β
+ ββV2. R V1 V2 & Z2 = BPair I V2.
+/2 width=3 by ext2_inv_pair_sn_aux/ qed-.
+
+fact ext2_inv_unit_dx_aux: βR,Z1,Z2. ext2 R Z1 Z2 β
+ βI. Z2 = BUnit I β Z1 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_dx: βR,I,Z1. ext2 R Z1 (BUnit I) β Z1 = BUnit I.
+/2 width=4 by ext2_inv_unit_dx_aux/ qed-.
+
+fact ext2_inv_pair_dx_aux: βR,Z1,Z2. ext2 R Z1 Z2 β
+ βI,V2. Z2 = BPair I V2 β
+ ββV1. R V1 V2 & Z1 = BPair I V1.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W2 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_dx: βR,Z1,I,V2. ext2 R Z1 (BPair I V2) β
+ ββV1. R V1 V2 & Z1 = BPair I V1.
+/2 width=3 by ext2_inv_pair_dx_aux/ qed-.
+
+(* Basic properties ********************************************************)
+
+lemma ext2_refl: βR. reflexive β¦ R β reflexive β¦ (ext2 R).
+#R #HR * /2 width=1 by ext2_pair/
+qed.
+
+lemma ext2_sym: βR. symmetric β¦ R β symmetric β¦ (ext2 R).
+#R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/
+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/syntax/bind_ext2.ma".
+include "basic_2/syntax/lenv.ma".
+
+(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********)
+
+definition cext2: (lenv β relation term) β lenv β relation bind β
+ Ξ»R,L. ext2 (R L).
+
+(* Basic properties *********************************************************)
+
+lemma cext2_sym: βR. (βL1,L2,T1,T2. R L1 T1 T2 β R L2 T2 T1) β
+ βL1,L2,I1,I2. cext2 R L1 I1 I2 β cext2 R L2 I2 I1.
+#R #HR #L1 #L2 #I1 #I2 * /3 width=2 by ext2_pair/
+qed-.
+
+lemma cext2_co: βR1,R2. (βL,T1,T2. R1 L T1 T2 β R2 L T1 T2) β
+ βL,I1,I2. cext2 R1 L I1 I2 β cext2 R2 L I1 I2.
+#R1 #R2 #HR #L #I1 #I2 * /3 width=2 by ext2_unit, ext2_pair/
+qed-.
}
]
[ { "local environments" * } {
+ [ "lenv_ext2" * ]
[ "lenv_length ( |?| )" * ]
[ "lenv_weight ( β―{?} )" * ]
[ "lenv" * ]
}
]
[ { "binders for local environments" * } {
+ [ "bind_ext2" * ]
[ "bind" "bind_weight" * ]
}
]
projects / helm.git / commitdiff