--- /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/cpr.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …).
+
+interpretation
+ "context-sensitive strong normalization (term)"
+ 'SN L T = (csn 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/static/aaa.ma".
+include "Basic_2/computation/csn_cr.ma".
+include "Basic_2/computation/lsubcs.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Main propertis ***********************************************************)
+
+axiom snc_aarity_csubcs: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L2 ⊑ L1 → {L2, T} ϵ 〚A〛.
+
+lemma snc_aarity: ∀L,T,A. L ⊢ T ÷ A → {L, T} ϵ 〚A〛.
+/2 width=3/ qed.
+
+axiom csn_arity: ∀L,T,A. L ⊢ T ÷ A → 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/csn.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* the candidate of reducibility associated to an atomic arity *)
+definition snc: aarity → lenv → predicate term ≝ acr csn.
+
+interpretation
+ "candidate of reducibility (contex-sensitive strong normalization)"
+ 'InEInt L T A = (snc A 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".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+inductive lsubc (R:lenv→predicate term) : relation lenv ≝
+| lsubc_atom: lsubc R (⋆) (⋆)
+| lsubc_pair: ∀I,L1,L2,V. lsubc R L1 L2 → lsubc R (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsubc_abbr: ∀L1,L2,V,W,A. R ⊢ {L1, V} ϵ 〚A〛 → R ⊢ {L2, W} ϵ 〚A〛 →
+ lsubc R L1 L2 → lsubc R (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+.
+
+interpretation
+ "local environment refinement (abstract candidates of reducibility)"
+ 'CrSubEq L1 R L2 = (lsubc R L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsubc_refl: ∀R,L. L [R] ⊑ L.
+#R #L elim L -L // /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
--- /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/lsubc.ma".
+include "Basic_2/computation/csn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRONG NORMALIZATION ********************)
+
+definition lsubcs: relation lenv ≝ lsubc csn.
+
+interpretation
+ "local environment refinement (strong normalization)"
+ 'CrSubEq L1 L2 = (lsubcs L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsubcs_refl: ∀L. L ⊑ L.
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
--- /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
+ [ Bind I ⇒ 𝕓{I} (flift d e V). (flift (d+1) e T)
+ | Flat 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/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
+ [ Bind I ⇒ 𝕓{I} (fsubst W d V). (fsubst W (d+1) T)
+ | Flat 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. 𝕓{Abbr} 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. 𝕓{Abbr} 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-.
+
\ No newline at end of file
--- /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/list.ma".
+include "Basic_2/notation.ma".
+
+(* ATOMIC ARITY *************************************************************)
+
+inductive aarity: Type[0] ≝
+ | AAtom: aarity (* atomic aarity construction *)
+ | APair: aarity → aarity → aarity (* binary aarity construction *)
+.
+
+interpretation "aarity construction (atomic)" 'SItem = AAtom.
+
+interpretation "aarity construction (binary)" 'SItem A1 A2 = (APair A1 A2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma discr_apair_xy_x: ∀A,B. 𝕔 B. A = B → False.
+#A #B elim B -B
+[ #H destruct
+| #Y #X #IHY #_ #H destruct
+ -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+ /2 width=1/
+]
+qed-.
+
+lemma discr_tpair_xy_y: ∀B,A. 𝕔 B. A = A → False.
+#B #A elim A -A
+[ #H destruct
+| #Y #X #_ #IHX #H destruct
+ -H (**) (* destruct: the destucted equality is not erased *)
+ /2 width=1/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma aarity_eq_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
+#A1 elim A1 -A1
+[ #A2 elim A2 -A2 /2 width=1/
+ #B2 #A2 #_ #_ @or_intror #H destruct
+| #B1 #A1 #IHB1 #IHA1 #A2 elim A2 -A2
+ [ -IHB1 -IHA1 @or_intror #H destruct
+ | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1
+ [ #H destruct elim (IHA1 A2) -IHA1
+ [ #H destruct /2 width=1/
+ | #HA12 @or_intror #H destruct /2 width=1/
+ ]
+ | -IHA1 #HB12 @or_intror #H destruct /2 width=1/
+ ]
+ ]
+]
+qed-.
notation "hvbox( T1 break [ R ] ⊑ break T2 )"
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
+
+(* Functional ***************************************************************)
+
+notation "hvbox( ↟ [ d , break e ] break T )"
+ non associative with precedence 80
+ for @{ 'Lift $d $e $T }.
+
+notation "hvbox( ↡ [ d ← break V ] break T )"
+ non associative with precedence 80
+ for @{ 'Subst $V $d $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/grammar/aarity.ma".
+include "Basic_2/substitution/ldrop.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+inductive aaa: lenv → term → predicate aarity ≝
+| aaa_sort: ∀L,k. aaa L (⋆k) 𝕒
+| aaa_lref: ∀I,L,K,V,B,i. ↓[0, i] L ≡ K. 𝕓{I} V → aaa K V B → aaa L (#i) B
+| aaa_abbr: ∀L,V,T,B,A.
+ aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A
+| aaa_abst: ∀L,V,T,B,A.
+ aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abbr} V. T) (𝕔 B. A)
+| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A
+| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A
+.
+
+interpretation
+ "atomic arity assignment (term)"
+ 'AtomicArity L T A = (aaa L T A).
(* Basic inversion lemmas ***************************************************)
-fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
+fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // /3 width=1/
qed.
-lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
+lemma lift_inv_refl_O2: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
/2 width=4/ qed-.
fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/
qed.
+lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ↑[d, e] #j ≡ #i.
+/2 width=1/ qed-.
+
(* Basic_1: was: lift_r *)
lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T.
#T elim T -T
| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct
[ -Hd12 lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3 width=3/
- | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_inv_plus_plus_r … H) -H #H
+ | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_plus_to_le_r … H) -H #H
elim (le_inv_plus_l … H) -H #Hide2 #He2i
lapply (transitive_le … Hd12 Hide2) -Hd12 #Hd12
>le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); // -He2i
]
qed.
+(* Note: apparently this was missing in Basic_1 *)
+theorem lift_div_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+ ∀e,e2,T2. ↑[d1 + e, e2] T2 ≡ T →
+ e ≤ e1 → e1 ≤ e + e2 →
+ ∃∃T0. ↑[d1, e] T0 ≡ T2 & ↑[d1, e + e2 - e1] T0 ≡ T1.
+#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
+[ #k #d1 #e1 #e #e2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3/
+| #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2
+ >(lift_inv_lref2_lt … H) -H [ /3 width=3/ | /2 width=3/ ]
+| #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2
+ elim (lt_or_ge (i+e1) (d1+e+e2)) #Hie1d1e2
+ [ elim (lift_inv_lref2_be … H ? ?) -H // /2 width=1/
+ | >(lift_inv_lref2_ge … H ?) -H //
+ lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
+ elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
+ @ex2_1_intro [2: /2 width=1/ | skip ] -Hd1e12
+ @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
+ ]
+| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
+| #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2
+ elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
+ elim (IHV1 … HV2 ? ?) -V // >plus_plus_comm_23 in HT2; #HT2
+ elim (IHT1 … HT2 ? ?) -T // -He1 -He1e2 /3 width=5/
+| #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2
+ elim (lift_inv_flat2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
+ elim (IHV1 … HV2 ? ?) -V //
+ elim (IHT1 … HT2 ? ?) -T // -He1 -He1e2 /3 width=5/
+]
+qed.
+
theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
#d #e #T #U1 #H elim H -d -e -T -U1
[ #k #d #e #X #HX
* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/
qed-.
+lemma tps_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ≫ T2 → T2 = §p.
+#L #T2 #p #d #e #H
+elim (tps_inv_atom1 … H) -H //
+* #K #V #i #_ #_ #_ #_ #H destruct
+qed-.
+
fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
interpretation "delift (term)"
'TSubst L T1 d e T2 = (delift d e L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
+ ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2.
+#L1 #T1 #T2 #d #e * /3 width=3/
+qed.
+
+lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
+ L ⊢ V1 [d, e] ≡ V2 → L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
+ L ⊢ 𝕓{I} V1. T1 [d, e] ≡ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
+lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+qed.
+
+lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
+ L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 →
+ L ⊢ 𝕗{I} V1. T1 [d, e] ≡ 𝕗{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma delift_fwd_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k.
+#L #U2 #d #e #k * #U #HU
+>(tpss_inv_sort1 … HU) -HU #HU2
+>(lift_inv_sort2 … HU2) -HU2 //
+qed-.
+
+lemma delift_fwd_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p.
+#L #U #d #e #p * #U #HU
+>(tpss_inv_gref1 … HU) -HU #HU2
+>(lift_inv_gref2 … HU2) -HU2 //
+qed-.
+
+lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕓{I} V1. T1 [d, e] ≡ U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
+ L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
+ U2 = 𝕓{I} V2. T2.
+#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
+elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
+elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
+lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+qed-.
+
+lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕗{I} V1. T1 [d, e] ≡ U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
+ L ⊢ T1 [d, e] ≡ T2 &
+ U2 = 𝕗{I} V2. T2.
+#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
+elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct
+elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
+qed-.
+
+(* Basic Inversion lemmas ***************************************************)
+
+lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2.
+#L #T1 #T2 #d * #T #HT1
+>(tpss_inv_refl_O2 … HT1) -HT1 #HT2
+>(lift_inv_refl_O2 … HT2) -HT2 //
+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/tpss_lift.ma".
+include "Basic_2/unfold/delift.ma".
+
+(* DELIFT ON TERMS **********************************************************)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
+#L #U2 #i #d #e * #U #HU #HU2 #Hid
+elim (tpss_inv_lref1 … HU) -HU
+[ #H destruct >(lift_inv_lref2_lt … HU2) //
+| * #K #V1 #V2 #Hdi
+ lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
+ elim (lt_refl_false … Hi)
+]
+qed-.
+
+lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
+ d ≤ i → i < d + e →
+ ∃∃K,V1,V2. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 &
+ K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
+ ↑[0, d] V2 ≡ U2.
+#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
+elim (tpss_inv_lref1 … HU) -HU
+[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
+| * #K #V1 #V #_ #_ #HLK #HV1 #HVU
+ elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/
+]
+qed-.
+
+lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+ d + e ≤ i → U2 = #(i - e).
+#L #U2 #i #d #e * #U #HU #HU2 #Hdei
+elim (tpss_inv_lref1 … HU) -HU
+[ #H destruct >(lift_inv_lref2_ge … HU2) //
+| * #K #V1 #V2 #_ #Hide
+ lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi
+ elim (lt_refl_false … Hi)
+]
+qed-.
]
qed-.
+(* Note: this can be derived from tpss_inv_atom1 *)
+lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ≫* T2 → T2 = §p.
+#L #T2 #p #d #e #H @(tpss_ind … H) -T2
+[ //
+| #T #T2 #_ #HT2 #IHT destruct
+ >(tps_inv_gref1 … HT2) -HT2 //
+]
+qed-.
+
lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 &
L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
(* equations ****************************************************************)
-lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
-// qed.
-
lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
/2 by plus_minus/ qed.
lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
/2 by plus_minus/ qed.
-lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
-
-lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
-#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
-qed.
-
lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
qed.
axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
-lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
-qed-.
-
lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
#m #n elim (lt_or_ge m n) /2 width=1/
#H elim H -m /2 width=1/
#m #Hm * #H /2 width=1/ /3 width=1/
qed-.
-lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
-/2 by le_plus_to_le/ qed-.
-
-lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
-/3 width=2/ qed-.
-
-lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
-/3 width=2/ qed-.
-
lemma lt_refl_false: ∀n. n < n → False.
#n #H elim (lt_to_not_eq … H) -H /2 width=1/
qed-.
#Hxy elim (H Hxy)
qed-.
-lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-#m1 #m2 #H #n1 #n2 >commutative_plus
-#H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
-#H #_ @(transitive_le … H) /2 width=1/
-qed-.
-
(*
lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
/3 width=2/
--- /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/arith.ma".
+
+(* TRICOTOMY FUNCTION *******************************************************)
+
+let rec tri (A:Type[0]) m n a b c on m : A ≝
+ match m with
+ [ O ⇒ match n with [ O ⇒ b | S n ⇒ a ]
+ | S m ⇒ match n with [ O ⇒ c | S n ⇒ tri A m n a b c ]
+ ].
+
+(* Basic properties *********************************************************)
+
+lemma tri_lt: ∀A,a,b,c,n,m. m < n → tri A m n a b c = a.
+#A #a #b #c #n elim n -n
+[ #m #H elim (lt_zero_false … H)
+| #n #IH #m elim m -m // /3 width=1/
+]
+qed.
+
+lemma tri_eq: ∀A,a,b,c,m. tri A m m a b c = b.
+#A #a #b #c #m elim m -m normalize //
+qed.
+
+lemma tri_gt: ∀A,a,b,c,m,n. n < m → tri A m n a b c = c.
+#A #a #b #c #m elim m -m
+[ #n #H elim (lt_zero_false … H)
+| #m #IH #n elim n -n // /3 width=1/
+]
+qed.
+
- (*
+(*
||M|| This file is part of HELM, an Hypertextual, Electronic
||A|| Library of Mathematics, developed at the Computer Science
||T|| Department of the University of Bologna, Italy.
theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
@nat_elim2 normalize // qed.
+lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
+// qed.
+
(* Negated equalities *******************************************************)
theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
#a #b #c #H @le_plus_to_minus_r //
qed.
+theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
+(* demo *)
+/2/ qed-.
+
(* not le, lt *)
theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
]
qed.
+lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
+/3 width=2/ qed-.
+
+lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
+/3 width=2/ qed-.
+
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
+qed-.
+
(* More general conclusion **************************************************)
theorem lt_O_n_elim: ∀n:nat. 0 < n →
#n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
qed.
+theorem plus_minus_commutative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
+/2 by plus_minus/ qed.
+
(* More atomic conclusion ***************************************************)
(* le *)
@(ex_intro ?? (S a)) /2/
qed.
+lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
+/3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+
(* lt *)
theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
<commutative_plus <plus_minus_m_m //
qed.
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
+
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
+qed.
+
+(* Stilll more atomic conclusion ********************************************)
+
+(* le *)
+
+lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
+#m1 #m2 #H #n1 #n2 >commutative_plus
+#H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
+#H #_ @(transitive_le … H) /2 width=1/
+qed-.
+
(*********************** boolean arithmetics ********************)
+
include "basics/bool.ma".
let rec eqb n m ≝
projects / helm.git / commitdiff