--- /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 "hvbox( T1 π break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RTop $T1 $T2 }.
+
+include "basic_2/grammar/lenv_px.ma".
+
+(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
+
+definition ttop: relation term β Ξ»T1,T2. True.
+
+definition ltop: relation lenv β lpx ttop.
+
+interpretation
+ "top reduction (environment)"
+ 'RTop L1 L2 = (ltop L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltop_refl: reflexive β¦ ltop.
+/2 width=1/ qed.
+
+lemma ltop_sym: symmetric β¦ ltop.
+/2 width=1/ qed.
+
+lemma ltop_trans: transitive β¦ ltop.
+/2 width=3/ qed.
+
+lemma ltop_append: βK1,K2. K1 π K2 β βL1,L2. L1 π L2 β L1 @@ K1 π L2 @@ K2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltop_inv_atom1: βL2. β π L2 β L2 = β.
+/2 width=2 by lpx_inv_atom1/ qed-.
+
+lemma ltop_inv_pair1: βK1,I,V1,L2. K1. β{I} V1 π L2 β
+ ββK2,V2. K1 π K2 & L2 = K2. β{I} V2.
+#K1 #I #V1 #L2 #H
+elim (lpx_inv_pair1 β¦ H) -H /2 width=4/
+qed-.
+
+lemma ltop_inv_atom2: βL1. L1 π β β L1 = β.
+/2 width=2 by lpx_inv_atom2/ qed-.
+
+lemma ltop_inv_pair2: βL1,K2,I,V2. L1 π K2. β{I} V2 β
+ ββK1,V1. K1 π K2 & L1 = K1. β{I} V1.
+#L1 #K2 #I #V2 #H
+elim (lpx_inv_pair2 β¦ H) -H /2 width=4/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltop_fwd_length: βL1,L2. L1 π L2 β |L1| = |L2|.
+/2 width=2 by lpx_fwd_length/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/grammar/lenv.ma".
+include "basic_2/grammar/lenv_append.ma".
(* SHIFT OF A CLOSURE *******************************************************)
].
interpretation "shift (closure)" 'Append L T = (shift L T).
+
+(* Basic properties *********************************************************)
+
+lemma shift_append_assoc: βL,K. βT:term. (L @@ K) @@ T = L @@ K @@ T.
+#L #K elim K -K normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma shift_inj: βL1,L2. βT1,T2:term. L1 @@ T1 = L2 @@ T2 β |L1| = |L2| β
+ L1 = L2 β§ T1 = T2.
+#L1 elim L1 -L1
+[ * normalize /2 width=1/
+ #L2 #I2 #V2 #T1 #T2 #_ <plus_n_Sm #H destruct
+| #L1 #H1 #V1 #IH * normalize
+ [ #T1 #T2 #_ <plus_n_Sm #H destruct
+ | #L2 #I2 #V2 #T1 #T2 #H1 #H2
+ elim (IH β¦ H1 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ ]
+]
+qed-.
+
\ No newline at end of file
(* Basic inversion lemmas ***************************************************)
-axiom discr_lpair_append_xy_x: βI,L,K,V. (L @@ K).β{I}V = L β β₯.
-(*
-#I #L #K #V #H
-lapply (refl β¦ (|L|)) <H in β’ (? ? % ? β ?); -H
-normalize >append_length -I -V #H
-*)
-lemma append_inv_sn: βL1,L2,L. L1 @@ L = L2 @@ L β L1 = L2.
-#L1 #L2 #L elim L -L normalize //
-#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
-qed.
+lemma append_inj_sn: βK1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 β |K1| = |K2| β
+ L1 = L2 β§ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+ #K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
+| #K1 #I1 #V1 #IH * normalize
+ [ #L1 #L2 #_ <plus_n_Sm #H destruct
+ | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+ elim (IH β¦ e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ ]
+]
+qed-.
(* Note: lemma 750 *)
-lemma append_inv_dx: βL1,L2,L. L @@ L1 = L @@ L2 β L1 = L2.
-#L1 elim L1 -L1
-[ * normalize //
- #L2 #I2 #V2 #L #H
- elim (discr_lpair_append_xy_x I2 L L2 V2 ?) //
-| #L1 #I1 #V1 #IHL1 * normalize
- [ #L #H -IHL1 elim (discr_lpair_append_xy_x β¦ H)
- | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *)
- -H >e0 /3 width=2/
+lemma append_inj_dx: βK1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 β |L1| = |L2| β
+ L1 = L2 β§ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+ #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
+ normalize in H2; >append_length in H2; #H
+ elim (plus_xySz_x_false β¦ H)
+| #K1 #I1 #V1 #IH * normalize
+ [ #L1 #L2 #H1 #H2 destruct
+ normalize in H2; >append_length in H2; #H
+ elim (plus_xySz_x_false β¦ (sym_eq β¦ H))
+ | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+ elim (IH β¦ e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
]
]
-qed.
+qed-.
+
+lemma length_inv_pos_dx_append: βd,L. |L| = d + 1 β
+ ββI,K,V. |K| = d & L = β.β{I}V @@ K.
+#d @(nat_ind_plus β¦ d) -d
+[ #L #H
+ elim (length_inv_pos_dx β¦ H) -H #I #K #V #H
+ >(length_inv_zero_dx β¦ H) -H #H destruct
+ @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (* /3/ does not work *)
+| #d #IHd #L #H
+ elim (length_inv_pos_dx β¦ H) -H #I #K #V #H
+ elim (IHd β¦ H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
+ @(ex2_3_intro β¦ (K0.β{I}V)) //
+]
+qed-.
+
+(* Basic_eliminators ********************************************************)
+
+fact lenv_ind_dx_aux: βR:predicate lenv. R β β
+ (βI,L,V. R L β R (β.β{I}V @@ L)) β
+ βd,L. |L| = d β R L.
+#R #Hatom #Hpair #d @(nat_ind_plus β¦ d) -d
+[ #L #H >(length_inv_zero_dx β¦ H) -H //
+| #d #IH #L #H
+ elim (length_inv_pos_dx_append β¦ H) -H #I #K #V #H1 #H2 destruct /3 width=1/
+]
+qed-.
+
+lemma lenv_ind_dx: βR:predicate lenv. R β β
+ (βI,L,V. R L β R (β.β{I}V @@ L)) β
+ βL. R L.
+/3 width=2 by lenv_ind_dx_aux/ qed-.
].
interpretation "length (local environment)" 'card L = (length L).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma length_inv_zero_dx: βL. |L| = 0 β L = β.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_zero_sn: βL. 0 = |L| β L = β.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_pos_dx: βd,L. |L| = d + 1 β
+ ββI,K,V. |K| = d & L = K. β{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+ lapply (injective_plus_l β¦ H) -H /2 width=5/
+]
+qed-.
+
+lemma length_inv_pos_sn: βd,L. d + 1 = |L| β
+ ββI,K,V. d = |K| & L = K. β{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+ lapply (injective_plus_l β¦ H) -H /2 width=5/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_append.ma".
(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
#R #HR #L elim L -L // /2 width=1/
qed.
+lemma lpx_sym: βR. symmetric ? R β symmetric β¦ (lpx R).
+#R #HR #L1 #L2 #H elim H -H // /3 width=1/
+qed.
+
lemma lpx_trans: βR. Transitive ? R β Transitive β¦ (lpx R).
#R #HR #L1 #L #H elim H -L //
#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
βL1,L2. lpx (TC β¦ R) L1 L2 β TC β¦ (lpx R) L1 L2.
#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
qed.
+
+lemma lpx_append: βR,K1,K2. lpx R K1 K2 β βL1,L2. lpx R L1 L2 β
+ lpx R (L1 @@ K1) (L2 @@ K2).
+#R #K1 #K2 #H elim H -K1 -K2 // /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/grammar/lenv_length.ma".
+
+(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************)
+
+inductive lpx_bi (R:bi_relation lenv term): relation lenv β
+| lpx_bi_stom: lpx_bi R (β) (β)
+| lpx_bi_pair: βI,K1,K2,V1,V2.
+ lpx_bi R K1 K2 β R K1 V1 K2 V2 β
+ lpx_bi R (K1. β{I} V1) (K2. β{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_bi_inv_atom1_aux: βR,L1,L2. lpx_bi R L1 L2 β L1 = β β L2 = β.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom1: βR,L2. lpx_bi R (β) L2 β L2 = β.
+/2 width=4 by lpx_bi_inv_atom1_aux/ qed-.
+
+fact lpx_bi_inv_pair1_aux: βR,L1,L2. lpx_bi R L1 L2 β
+ βI,K1,V1. L1 = K1. β{I} V1 β
+ ββK2,V2. lpx_bi R K1 K2 &
+ R K1 V1 K2 V2 & L2 = K2. β{I} V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair1: βR,I,K1,V1,L2. lpx_bi R (K1. β{I} V1) L2 β
+ ββK2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+ L2 = K2. β{I} V2.
+/2 width=3 by lpx_bi_inv_pair1_aux/ qed-.
+
+fact lpx_bi_inv_atom2_aux: βR,L1,L2. lpx_bi R L1 L2 β L2 = β β L1 = β.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom2: βR,L1. lpx_bi R L1 (β) β L1 = β.
+/2 width=4 by lpx_bi_inv_atom2_aux/ qed-.
+
+fact lpx_bi_inv_pair2_aux: βR,L1,L2. lpx_bi R L1 L2 β
+ βI,K2,V2. L2 = K2. β{I} V2 β
+ ββK1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+ L1 = K1. β{I} V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair2: βR,I,L1,K2,V2. lpx_bi R L1 (K2. β{I} V2) β
+ ββK1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+ L1 = K1. β{I} V1.
+/2 width=3 by lpx_bi_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_bi_fwd_length: βR,L1,L2. lpx_bi R L1 L2 β |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_bi_refl: βR. bi_reflexive ? ? R β reflexive β¦ (lpx_bi R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
non associative with precedence 45
for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
+notation "hvbox( β¦ L1 β¦ β‘ β‘ break β¦ L2 β¦ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedAlt $L1 $L2 }.
+
notation "hvbox( β¦ h , break L β¦ β’ break term 46 T1 βΈ break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XPRed $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 "basic_2/reducibility/tpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+
+definition fpr: bi_relation lenv term β
+ Ξ»L1,T1,L2,T2. |L1| = |L2| β§ L1 @@ T1 β‘ L2 @@ T2.
+
+interpretation
+ "focalized parallel reduction (closure)"
+ 'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fpr_refl: bi_reflexive β¦ fpr.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpr_inv_atom1: βL2,T1,T2. β¦β, T1β¦ β‘ β¦L2, T2β¦ β T1 β‘ T2 β§ L2 = β.
+#L2 #T1 #T2 * #H
+lapply (length_inv_zero_sn β¦ H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair1: βI,K1,L2,V1,T1,T2. β¦K1.β{I}V1, T1β¦ β‘ β¦L2, T2β¦ β
+ ββK2,V2. β¦K1, -β{I}V1.T1β¦ β‘ β¦K2, -β{I}V2.T2β¦ &
+ L2 = K2.β{I}V2.
+#I1 #K1 #L2 #V1 #T1 #T2 * #H
+elim (length_inv_pos_sn β¦ H) -H #I2 #K2 #V2 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus β¦ H) // #_ #H0 destruct /3 width=4/
+qed-.
+
+lemma fpr_inv_atom3: βL1,T1,T2. β¦L1,T1β¦ β‘ β¦β,T2β¦ β T1 β‘ T2 β§ L1 = β.
+#L1 #T1 #T2 * #H
+lapply (length_inv_zero_dx β¦ H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair3: βI,L1,K2,V2,T1,T2. β¦L1, T1β¦ β‘ β¦K2.β{I}V2, T2β¦ β
+ ββK1,V1. β¦K1, -β{I}V1.T1β¦ β‘ β¦K2, -β{I}V2.T2β¦ &
+ L1 = K1.β{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 * #H
+elim (length_inv_pos_dx β¦ H) -H #I1 #K1 #V1 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus β¦ H) // #_ #H0 destruct /3 width=4/
+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/lenv_px_bi.ma".
+include "basic_2/reducibility/fpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
+
+(* alternative definition *)
+definition lfpra: relation lenv β lpx_bi fpr.
+
+interpretation
+ "focalized parallel reduction (environment) alternative"
+ 'FocalizedPRedAlt L1 L2 = (lfpra L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lfpra_refl: reflexive β¦ lfpra.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfpra_inv_atom1: βL2. β¦ββ¦ β‘β‘ β¦L2β¦ β L2 = β.
+/2 width=2 by lpx_bi_inv_atom1/ qed-.
+
+lemma lfpra_inv_pair1: βK1,I,V1,L2. β¦K1. β{I} V1β¦ β‘β‘ β¦L2β¦ β
+ ββK2,V2. β¦K1β¦ β‘β‘ β¦K2β¦ & β¦K1, V1β¦ β‘ β¦K2, V2β¦ &
+ L2 = K2. β{I} V2.
+/2 width=1 by lpx_bi_inv_pair1/ qed-.
+
+lemma lfpra_inv_atom2: βL1. β¦L1β¦ β‘β‘ β¦ββ¦ β L1 = β.
+/2 width=2 by lpx_bi_inv_atom2/ qed-.
+
+lemma lfpra_inv_pair2: βL1,K2,I,V2. β¦L1β¦ β‘β‘ β¦K2. β{I} V2β¦ β
+ ββK1,V1. β¦K1β¦ β‘β‘ β¦K2β¦ & β¦K1, V1β¦ β‘ β¦K2, V2β¦ &
+ L1 = K1. β{I} V1.
+/2 width=1 by lpx_bi_inv_pair2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfpra_fwd_length: βL1,L2. β¦L1β¦ β‘β‘ β¦L2β¦ β |L1| = |L2|.
+/2 width=2 by lpx_bi_fwd_length/ qed-.
+
+(****************************************************************************)
+
+lemma fpr_lfpra: βL1,T1,L2,T2. β¦L1, T1β¦ β‘ β¦L2, T2β¦ β β¦L1β¦ β‘β‘ β¦L2β¦.
+#L1 #T1 @(cw_wf_ind β¦ L1 T1) -L1 -T1 *
+[ #T1 #_ #L2 #T2 #H
+ elim (fpr_inv_atom1 β¦ H) -H #_ #H destruct //
+| #L1 #I #V1 #T1 #IH #Y #X #H
+ elim (fpr_inv_pair1 β¦ H) -H #L2 #V2 #HL12 #H destruct
+ @lpx_bi_pair
+ [ @(IH β¦ HL12)
+ | @IH
+
+ /3 width=4/
+
+lemma fpr_lfpra: βL1,L2,T1,T2. β¦L1, T1β¦ β‘ β¦L2, T2β¦ β β¦L1β¦ β‘β‘ β¦L2β¦.
+#L1 elim L1 -L1
+[ #L2 #T1 #T2 #H
+ elim (fpr_inv_atom1 β¦ H) -H #_ #H destruct //
+| #L1 #I #V1 #IH #L2 #T1 #T2 #H
+ elim (fpr_inv_pair1 β¦ H) -H #L #V #HL1 #H destruct
+ @lpx_bi_pair /2 width=3/
+
+ /4 width=3/
+
+(*
+include "basic_2/reducibility/lcpr.ma".
+
+lemma lcpr_pair2: βL1,L2. L1 β’ β‘ L2 β βV1,V2. β¦L1, V1β¦ β‘ β¦L2, V2β¦ β
+ βI. L1. β{I} V1 β’ β‘ L2. β{I} V2.
+#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
+#H1 #H2 #I
+@(ex2_1_intro β¦ (L.β{I}V1)) /2 width=1/
+@tpss_
+
+(*
+<(ltpss_fwd_length β¦ HL2) /4 width=5/
+qed.
+*)
+*)
\ No newline at end of file
| ββV,T. T β‘ #i & T1 = βV. T.
/2 width=3/ qed-.
+(* Basic forward lemmas *****************************************************)
+
+lemma tpr_fwd_shift1: βL1,T1,T. L1 @@ T1 β‘ T β
+ ββL2,T2. L1 π L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx β¦ L1) -L1
+[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H
+ elim (tpr_inv_bind1 β¦ H) -H *
+ [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct
+ elim (IH β¦ HT10) -IH -T1 #L2 #V2 #HL12 #H destruct
+ elim (tps_fwd_shift1 β¦ HTX0) -V2 #L3 #X3 #HL23 #H destruct
+ lapply (ltop_trans β¦ HL12 HL23) -L2 #HL13
+ @(ex2_2_intro β¦ (β.β{I}V0@@L3)) /2 width=4/ /3 width=1/
+ | #T0 #_ #_ #H destruct
+ ]
+]
+qed-.
+
+lemma tpr_fwd_shift_bind_minus: βL1,L2. |L1| = |L2| β βI1,I2,V1,V2,T1,T2.
+ L1 @@ -β{I1}V1.T1 β‘ L2 @@ -β{I2}V2.T2 β
+ L1 π L2 β§ I1 = I2.
+#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
+elim (tpr_fwd_shift1 (L1.β{I1}V1) β¦ H) -H #Y #X #HY #HX
+elim (ltop_inv_pair1 β¦ HY) -HY #L #V #HL1 #H destruct
+elim (shift_inj (L2.β{I2}V2) β¦ HX ?) -HX
+[ #H1 #_ destruct /2 width=1/
+| lapply (ltop_fwd_length β¦ HL1) -HL1 normalize //
+]
+qed-.
+
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
Basic_1: removed local theorems: 1: pr0_delta_tau
(* *)
(**************************************************************************)
+include "basic_2/grammar/lenv_top.ma".
include "basic_2/substitution/ldrop.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.
+lemma tps_fwd_shift1: βL1,L,T1,T,d,e. L β’ L1 @@ T1 βΆ [d, e] T β
+ ββL2,T2. L1 π L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx β¦ L1) -L1
+[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
+ elim (tps_inv_bind1 β¦ H) -H #V2 #T2 #_ #HT12 #H destruct
+ elim (IH β¦ HT12) -IH -L -T1 -d -e #L2 #T #HL12 #H destruct
+ @(ex2_2_intro β¦ (β.β{I}V2@@L2)) /2 width=4/ /3 width=2/
+]
+qed-.
+
(* Basic_1: removed theorems 25:
subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
#Hxy elim (H Hxy)
qed-.
+lemma plus_xySz_x_false: βz,x,y. x + y + S z = x β β₯.
+#z #x elim x -x normalize
+[ #y <plus_n_Sm #H destruct
+| /3 width=2/
+]
+qed-.
+
(* iterators ****************************************************************)
(* Note: see also: lib/arithemetcs/bigops.ma *)
interpretation "functional extentional equality"
'eqF A B f g = (exteqF A B f g).
+(********** relations on unboxed pairs **********)
+
+definition bi_relation: Type[0] β Type[0] β Type[0]
+β Ξ»A,B.AβBβAβBβProp.
+
+definition bi_reflexive: βA,B. βR :bi_relation A B. Prop
+β Ξ»A,B,R. βx,y. R x y x y.
["z"; "ΞΆ"; "π«"; "π³"; "π"; "β©"; ] ;
["Z"; "β¨"; "β€"; "π"; "β"; ] ;
["0"; "π"; "βͺ"; ] ;
- ["1"; "π"; "β "; ] ;
- ["2"; "π"; "β‘"; ] ;
- ["3"; "π"; "β’"; ] ;
- ["4"; "π"; "β£"; ] ;
- ["5"; "π"; "β€"; ] ;
- ["6"; "π"; "β₯"; ] ;
- ["7"; "π"; "β¦"; ] ;
- ["8"; "π "; "β§"; ] ;
- ["9"; "π‘"; "β¨"; ] ;
+ ["1"; "π"; "β "; "β΅"; ] ;
+ ["2"; "π"; "β‘"; "βΆ"; ] ;
+ ["3"; "π"; "β’"; "β·"; ] ;
+ ["4"; "π"; "β£"; "βΈ"; ] ;
+ ["5"; "π"; "β€"; "βΉ"; ] ;
+ ["6"; "π"; "β₯"; "βΊ"; ] ;
+ ["7"; "π"; "β¦"; "β»"; ] ;
+ ["8"; "π "; "β§"; "βΌ"; ] ;
+ ["9"; "π‘"; "β¨"; "β½"; ] ;
]
;;
projects / helm.git / commitdiff