--- /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/lstas.ma".
+
+(* EXAMPLES *****************************************************************)
+
+(* Static type assignment (iterated vs primitive): the declared variable ****)
+
+(* basic_1: we have "L.ⓛⓝ⋆k1.⋆k2⦄ ⊢ #0 • ⓝ⋆k1.⋆k2". *)
+theorem sta_ldec: ∀h,G,L,s1,s2. ⦃G, L.ⓛⓝ⋆s1.⋆s2⦄ ⊢ #0 •*[h, 1] ⋆s2.
+/3 width=6 by lstas_sort, lstas_succ, lstas_cast, drop_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/rt_computation/cpms_drops.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* EXAMPLES *****************************************************************)
+
+(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
+
+(* Note: extended validity of a closure, height of cnv_appl > 1 *)
+lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![Ⓕ,h].
+#h #p #G #L #s
+@(cnv_appl … 2 p … (⋆s) … (⋆s))
+[ #H destruct
+| /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
+| /4 width=1 by cnv_bind, cnv_zero/
+| /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
+| /5 width=5 by cpm_cpms, cpm_bind, cpm_ell, lifts_uni, lifts_sort, lifts_bind/
+]
+qed.
+
+(* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
+lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![Ⓣ,h].
+#h #p #G #L #s
+@(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
+[ /2 width=1 by/
+| /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
+| @cnv_zero
+ @cnv_bind //
+ @(cnv_appl … 1 p … (⋆s) … (⋆s))
+ [ /2 width=1 by/
+ | /2 width=1 by cnv_sort, cnv_zero/
+ | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
+ | /2 width=3 by cpms_ell, lifts_sort/
+ | /4 width=5 by cpms_lref, cpms_ell, lifts_uni, lifts_sort, lifts_bind/
+ ]
+| /4 width=3 by cpms_lref, cpms_ell, lifts_sort/
+| /5 width=7 by cpms_ell, lifts_bind, lifts_flat, lifts_push_lref, lifts_push_zero, lifts_sort/
+]
+qed.
(* *)
(**************************************************************************)
-include "basic_2/computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbs_cpxs.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
(* EXAMPLES *****************************************************************)
-(* Reflexivity of proper qrst-computation: the term ApplOmega ***************)
+(* Reflexivity of proper rst-computation: the term ApplOmega ****************)
definition ApplDelta: term → nat → term ≝ λW,s. +ⓛW.ⓐ⋆s.ⓐ#0.#0.
(* Basic properties *********************************************************)
-lemma ApplDelta_lift: ∀W1,W2,s,l,k. ⬆[l, k] W1 ≡ W2 →
- ⬆[l, k] (ApplDelta W1 s) ≡ (ApplDelta W2 s).
-/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
+lemma ApplDelta_lifts (f:rtmap):
+ ∀W1,W2,s. ⬆*[f] W1 ≘ W2 →
+ ⬆*[f] (ApplDelta W1 s) ≘ (ApplDelta W2 s).
+/5 width=1 by lifts_sort, lifts_lref, lifts_bind, lifts_flat/ qed.
-lemma cpr_ApplOmega_12: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡ ApplOmega2 W s.
-/2 width=1 by cpr_beta/ qed.
+lemma cpr_ApplOmega_12 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡[h] ApplOmega2 W s.
+/2 width=1 by cpm_beta/ qed.
-lemma cpr_ApplOmega_23: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡ ApplOmega3 W s.
-#G #L #W1 #s elim (lift_total W1 0 1) #W2 #HW12
-@(cpr_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lift, lift_flat/
-@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 s) ? 0)
-[3,5,8,10: /2 width=2 by ApplDelta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ]
+lemma cpr_ApplOmega_23 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡[h] ApplOmega3 W s.
+#h #G #L #W1 #s elim (lifts_total W1 (𝐔❴1❵)) #W2 #HW12
+@(cpm_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lifts, lifts_flat/
+@cpm_appl // @cpm_appl @(cpm_delta … (ApplDelta W1 s))
+/2 width=1 by ApplDelta_lifts, cpm_eps/
qed.
-lemma cpxs_ApplOmega_13: ∀h,o,G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡*[h,o] ApplOmega3 W s.
-/4 width=3 by cpxs_strap1, cpr_cpx/ qed.
+lemma cpxs_ApplOmega_13 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ⬈*[h] ApplOmega3 W s.
+/4 width=4 by cpxs_strap1, cpm_fwd_cpx/ qed.
lemma fqup_ApplOmega_13: ∀G,L,W,s. ⦃G, L, ApplOmega3 W s⦄ ⊐+ ⦃G, L, ApplOmega1 W s⦄.
/2 width=1 by/ qed.
(* Main properties **********************************************************)
-theorem fpbg_refl: ∀h,o,G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >≡[h,o] ⦃G, L, ApplOmega1 W s⦄.
+theorem fpbg_refl (h) (o): ∀G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >[h,o] ⦃G, L, ApplOmega1 W s⦄.
/3 width=5 by fpbs_fpbg_trans, fqup_fpbg, cpxs_fpbs/ 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/dynamic/snv.ma".
-
-(* EXAMPLES *****************************************************************)
-
-(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
-
-(* extended validity of a closure, last arg of snv_appl > 1 *)
-lemma snv_extended: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, o].
-#h #o #a #G #L #s elim (deg_total h o s)
-#d #Hd @(snv_appl … a … (⋆s) … (⋆s) (0+1+1))
-[ /4 width=5 by snv_lref, drop_drop_lt/
-| /4 width=13 by snv_bind, snv_lref/
-| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (d+1+1))
- /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/
-]
-qed.
-
-(* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **)
-lemma snv_restricted: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛⓛ{a}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, o].
-#h #o #a #G #L #s elim (deg_total h o s)
-#d #Hd @(snv_appl … a … (⋆s) … (ⓐ#0.#2) (0+1))
-[ /4 width=5 by snv_lref, drop_drop_lt/
-| @snv_lref [4: // |1,2,3: skip ]
- @snv_bind //
- @(snv_appl … a … (⋆s) … (⋆s) (0+1))
- [ @snv_lref [4: // |1,2,3: skip ] //
- | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //
- | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/
- | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/
- @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/
- ]
-| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (d+1+1)) //
- [ @da_ldec [3: // |1,2: skip ]
- @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ]
- /3 width=1 by da_sort, da_bind/
- | @lstas_succ [4: // |1,2: skip ]
- [2: @lstas_bind | skip ]
- [2: @lstas_appl | skip ]
- [2: @lstas_zero
- [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ]
- |1: skip ]
- /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/
- ]
-]
-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/unfold/lstas.ma".
-
-(* EXAMPLES *****************************************************************)
-
-(* Static type assignment (iterated vs primitive): the declared variable ****)
-
-(* basic_1: we have "L.ⓛⓝ⋆k1.⋆k2⦄ ⊢ #0 • ⓝ⋆k1.⋆k2". *)
-theorem sta_ldec: ∀h,G,L,s1,s2. ⦃G, L.ⓛⓝ⋆s1.⋆s2⦄ ⊢ #0 •*[h, 1] ⋆s2.
-/3 width=6 by lstas_sort, lstas_succ, lstas_cast, drop_pair/ qed-.
class "red"
[ { "examples" * } {
[ { "terms with special features" * } {
- [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
+ [ "ex_cpr_omega" + "ex_fpbg_refl" + "ex_cnv_eta" * ]
}
]
}
(* *)
(**************************************************************************)
+include "ground_2/lib/arith_2b.ma".
include "basic_2/rt_transition/lpr_lpr.ma".
include "basic_2/rt_computation/cpms_lsubr.ma".
include "basic_2/rt_computation/cpms_fpbg.ma".
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
-lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
/3 width=3 by cpms_eps, ex2_intro/
qed-.
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
-lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
/2 width=3 by ex2_intro/
qed-.
(* *)
(**************************************************************************)
+include "ground_2/lib/arith_2b.ma".
include "basic_2/rt_computation/cpms_fpbg.ma".
include "basic_2/rt_computation/cprs_cprs.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
>eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
lapply (cprs_trans … HXW21 … H1) -XW1 #H1
- lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l_eq #H2
+ lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l1 #H2
/2 width=3 by cnv_cast/
| #HX -IH2 -HW1 -U1
lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
--- /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/dynamic/cnv_cpm_trans.ma".
+include "basic_2/dynamic/cnv_cpm_conf.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Far confluence propery with t-bound rt-computation for terms *************)
+
+fact cnv_cpsms_conf_lpr_aux (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpsms_conf_lpr a h o G1 L1 T1.
+#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0
+#n1 #T1 * #m11 #m12 #X1 #HnX01 #HX01 #HXT1 #H1
+#n2 #T2 * #m21 #m22 #X2 #HnX02 #HX02 #HXT2 #H2
+#L1 #HL01 #L2 #HL02 destruct
+lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
+lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
+elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
+cut (⦃G0,L0,T0⦄ >[h,o] ⦃G0,L0,X1⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
+lapply (fpbg_fpbs_trans ??? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg
+lapply (cnv_cpms_trans_lpr_far … IH2 … HXZ10 … L0 ?) // #HZ0
+elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
+elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
+elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
+lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
+lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
+/2 width=3 by ex2_intro/
+qed-.
(* *)
(**************************************************************************)
+include "basic_2/notation/relations/predstar_7.ma".
include "basic_2/rt_computation/fpbg.ma".
include "basic_2/rt_computation/cpms_fpbs.ma".
include "basic_2/dynamic/cnv.ma".
(* Inductive premises for the preservation results **************************)
+definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2.
+ ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n.
+
+interpretation
+ "context-sensitive parallel stratified t-bound rt-computarion (term)"
+ 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2).
+
definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
(* Properties for preservation **********************************************)
lemma cnv_cpms_trans_lpr_far (a) (h) (o):
--- /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 n, break term 46 h, break term 46 o ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $n $h $o $G $L $T1 $T2 }.
#h #o #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
/3 width=1 by/
qed-.
+
+(* Inversion lemmas with proper parallel rst-computation for closures *******)
+
+lemma fsb_fpbg_refl_false (h) (o) (G) (L) (T):
+ ≥[h,o] 𝐒⦃G, L, T⦄ → ⦃G, L, T⦄ >[h,o] ⦃G, L, T⦄ → ⊥.
+#h #o #G #L #T #H
+@(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
+/2 width=5 by/
+qed-.
*)
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpms_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
}
]
}
lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
// qed.
-lemma arith_l (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
-* // qed.
-
-lemma arith_l_eq: ∀x. 1 = 1-x+(x-(x-1)).
-// qed.
-
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
/2 width=3 by transitive_le/ qed.
+lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a.
+/2 width=1 by le_plus_to_minus_r/
+qed-.
+
+lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
+/2 width=1 by le_plus_to_minus/ qed-.
+
(* Note: this might interfere with nat.ma *)
lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
#m #n #Hmn #Hm whd >(S_pred … Hm)
--- /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/lib/arith.ma".
+
+(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
+
+lemma arith_l4 (m11) (m12) (m21) (m22):
+ m21+m22-(m11+m12) = m21-m11-m12+(m22-(m11-m21)-(m12-(m21-m11))).
+#m11 #m12 #m21 #m22 >minus_plus
+elim (le_or_ge (m11+m12) m21) #Hm1121
+[ lapply (transitive_le m11 ??? Hm1121) // #Hm121
+ lapply (le_plus_to_minus_l … Hm1121) #Hm12211
+ <plus_minus // @eq_f2 // >(eq_minus_O m11 ?) // >(eq_minus_O m12 ?) //
+| >(eq_minus_O m21 ?) // <plus_O_n <minus_plus <commutative_plus
+ elim (le_or_ge m11 m21) #Hm121
+ [ lapply (le_plus_to_minus_comm … Hm1121) #Hm2112
+ >(eq_minus_O m11 ?) // <plus_minus_associative // <minus_le_minus_minus_comm //
+ | >(eq_minus_O m21 ?) // <minus_le_minus_minus_comm //
+ ]
+]
+qed.
+
+lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
+* // qed.
+
+lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
+// qed.
[ { "" * } {
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
[ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
- [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
+ [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2b" * ]
[ "ltc" "ltc_ctc" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ]
}
ground_2
static_2
-basic_2/rt_transition
-basic_2/rt_computation
-basic_2/rt_conversion
-basic_2/rt_equivalence
-basic_2/dynamic/
-apps_2/examples/ex_cpr_omega.ma
-apps_2/functional/
-apps_2/models/
+basic_2
+apps_2
]
qed-.
+lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0.
+/2 width=1 by lifts_lref/ qed.
+
+lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2).
+#f1 #i1 #i2 #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+/3 width=7 by lifts_lref, at_push/
+qed.
+
lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i).
#l elim l -l /2 width=1 by lifts_lref/
qed.
projects / helm.git / commitdiff