--- /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/grammar/lenv.ma".
+
+(* ABSTRACT CANDIDATES OF REDUCIBILITY **************************************)
+
+(* the abstract candidate of reducibility associated to an atomic arity *)
+let rec acr (R:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
+λT. match A with
+[ AAtom ⇒ R L T
+| APair B A ⇒ ∀V. acr R B L V → acr R A L (𝕔{Appl} V. T)
+].
+
+interpretation
+ "candidate of reducibility (abstract)"
+ 'InEInt R L T A = (acr R A L T).
lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
#L elim L //
#K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2 width=1/ | skip ]
+@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
qed.
(* Basic_1: removed theorems 6:
+++ /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".
-
-(* SORT HIERARCHY ***********************************************************)
-
-(* sort hierarchy specifications *)
-record sh: Type[0] ≝ {
- next: nat → nat; (* next sort in the hierarchy *)
- next_lt: ∀k. k < next k (* strict monotonicity condition *)
-}.
[ #J #H destruct
| #J #W #U #IHW #_ #H destruct
-H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
- /2 width=1/
+ /2 width=1/
]
qed-.
non associative with precedence 90
for @{ 'GRef $p }.
+notation "hvbox( 𝕒 )"
+ non associative with precedence 90
+ for @{ 'SItem }.
+
notation "hvbox( 𝕒 { I } )"
non associative with precedence 90
for @{ 'SItem $I }.
+notation "hvbox( 𝕔 term 90 T1 . break term 90 T )"
+ non associative with precedence 90
+ for @{ 'SItem $T1 $T }.
+
notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
for @{ 'SItem $I $T1 $T }.
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
+(* Static Typing ************************************************************)
+
+notation "hvbox( L ⊢ break term 90 T ÷ break A )"
+ non associative with precedence 45
+ for @{ 'AtomicArity $L $T $A }.
+
(* Reducibility *************************************************************)
notation "hvbox( ℝ [ T ] )"
notation "hvbox( L ⊢ ⇓ T )"
non associative with precedence 45
for @{ 'SN $L $T }.
+
+notation "hvbox( { L, break T } ϵ break 〚 A 〛 )"
+ non associative with precedence 45
+ for @{ 'InEInt $L $T $A }.
+
+notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )"
+ non associative with precedence 45
+ for @{ 'InEInt $R $L $T $A }.
+
+notation "hvbox( T1 ⊑ break T2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEq $T1 $T2 }.
+
+notation "hvbox( T1 break [ R ] ⊑ break T2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEq $T1 $R $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/grammar/term_simple.ma".
-
-(* CANDIDATES OF REDUCIBILITY ***********************************************)
-
-(* abstract conditions for candidates *)
-
-definition CR1: predicate term → predicate term → Prop ≝
- λRD,RC. ∀T. RC T → RD T.
-
-definition CR2: relation term → predicate term → Prop ≝
- λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2.
-
-definition CR3: relation term → predicate term → Prop ≝
- λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1.
-
-(* a candidate *)
-record cr (RR:relation term) (RD:predicate term): Type[0] ≝ {
- in_cr: predicate term;
- cr1: CR1 RD in_cr;
- cr2: CR2 RR in_cr;
- cr3: CR3 RR in_cr
-}.
-
-interpretation
- "context-free parallel reduction (term)"
- 'InSubset T R = (in_cr ? ? R T).
-
-definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝
- λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C.
elim (lift_total T d e) #U #HTU
lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
elim (lt_or_ge (|K|) d) #HKd
-[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ]
+[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=2/ | /3 width=4/ ]
| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/
]
qed.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ]
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ]
| elim (lt_or_ge (|L|) (d + e)) #HLde
- [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ]
+ [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=2/ ]
| elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/
]
]
∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
-elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
-elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/
qed.
(* basic-1: was:
W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 →
∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
-elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2
elim (lift_total VV 0 1) #VVV #HVV
lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
elim (tpr_inv_abbr1 … H) -H *
(* case 1: delta *)
[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
- elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2
- elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2
+ elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2
+ elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2
elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
@ex2_1_intro
[2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
lapply (tw_lift … HUU10) -HUU10 #HUU10
- elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2
+ elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH /2 width=1/ -HUU10 #U #HU2 #HUUU2
@ex2_1_intro
[2: @tpr_flat
|1: skip
V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 -HV02 //
-elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/
qed.
(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
-elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
-elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2
-elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
+elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ #T #HT1 #HT2
elim (lift_total V 0 1) #VV #HVV
lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1
lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2
--- /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".
+
+(* SORT HIERARCHY ***********************************************************)
+
+(* sort hierarchy specifications *)
+record sh: Type[0] ≝ {
+ next: nat → nat; (* next sort in the hierarchy *)
+ next_lt: ∀k. k < next k (* strict monotonicity condition *)
+}.
[ -IHL12 -Hie destruct
<minus_n_O <minus_plus_m_m // /2 width=3/
| -HL12
- elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+ elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/
]
| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
[ -IHL12 -Hie -Hi destruct
- | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+ | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/
]
| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
- lapply (plus_S_le_to_pos … Hdi) #Hi
+ elim (le_inv_plus_l … Hdi) #Hdim #Hi
lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
- elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/
+ elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/
]
qed.
| //
| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2
- <minus_plus_comm /3 width=1/
+ <minus_plus >minus_minus_comm /3 width=1/
| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
lapply (transitive_le 1 … Hdee2) // #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2
[ #d #e #e2 #L2 #H
>(ldrop_inv_atom1 … H) -L2 /2 width=3/
| #K #I #V #e2 #L2 #HL2 #H
- lapply (le_O_to_eq_O … H) -H #H destruct /2 width=3/
+ lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
- lapply (le_O_to_eq_O … H) -H #H destruct
+ lapply (le_n_O_to_eq … H) -H #H destruct
elim (IHL12 … HL2 ?) -IHL12 -HL2 // #L0 #H #HL0
lapply (ldrop_inv_refl … H) -H #H destruct /3 width=5/
| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
- lapply (transitive_le …(i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
- <(arith_d1 i e2 e1) // /3 width=3/
+ lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
+ >(plus_minus_m_m e2 e1 ?) // /3 width=3/
| /3 width=3/
| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
| #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 lapply (arith1 … Hid2) -Hid2 #Hid2
- @(ex2_1_intro … #(i - e2))
- [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2 width=1/ | -Hd12 /2 width=2/ ]
- | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=1/
- ]
+ | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_inv_plus_plus_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
+ /4 width=3/
]
| #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/
lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e -Hded #Hid2
lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3/
| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
- elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct
- [ /4 width=3/ | >plus_plus_comm_23 /4 width=3/ ]
+ elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3/
| #p #d1 #e1 #d2 #e2 #X #HX #_
>(lift_inv_gref1 … HX) -HX /2 width=3/
| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
- lapply (plus_le_weak … He12) #He2
+ elim (le_inv_plus_l … He12) #_ #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
- lapply (plus_le_weak … Hd1e2) #He2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
]
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
- lapply (plus_le_weak … He12) #He2
+ elim (le_inv_plus_l … He12) #_ #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
- lapply (plus_le_weak … Hd1e2) #He2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
]
elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
]
| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
- lapply (plus_le_weak … Hd1e2) #He2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
<minus_le_minus_minus_comm //
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
]
| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
- lapply (plus_le_weak … Hd1e2) #He2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
<minus_le_minus_minus_comm //
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
- @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *)
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
| /3 width=4/
]
qed.
[ /2 width=3/
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
elim (lt_or_ge i2 d1) #Hi2d1
- [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=1/ #X #H #HLK1
+ [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
elim (ltps_inv_tps11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK1) #H
elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >arith_a2 // /3 width=4/
+ lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
| elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
- [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 /2 width=1/ #X #H #HLK1
+ [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
elim (ltps_inv_tps21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK1) #H
elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // normalize #HW01
- lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >arith_i2 //
+ lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
| lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
]
]
lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
- @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *)
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
| /3 width=4/
]
qed.
[ /2 width=3/
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
elim (lt_or_ge i2 d1) #Hi2d1
- [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=1/ #X #H #HLK1
+ [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
elim (ltps_inv_tps12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >arith_a2 // /3 width=4/
+ lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
| elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
- [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=1/ #X #H #HLK1
+ [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // normalize #HW01
- lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >arith_i2 //
+ lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
| lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
]
]
elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
destruct
elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i ? ? ?) // <minus_plus_m_m_comm /3 width=4/
+ elim (lift_split … HVW i i ? ? ?) // /3 width=4/
| * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
[ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
[ //
| #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
- lapply (le_to_lt_to_lt … Hdi Hi) #Hd
- lapply (plus_minus_m_m_comm (|L|) d ?) /2 width=1/ /2 width=4/
+ lapply (le_to_lt_to_lt … Hdi Hi) /3 width=4/
| normalize /2 width=1/
| /2 width=1/
]
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
elim (lt_or_ge i j)
[ -Hide -Hjde
- >(plus_minus_m_m_comm j d) in ⊢ (% → ?); // -Hdj /3 width=4/
+ >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=4/
| -Hdi -Hdj #Hid
generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *)
- >(plus_minus_m_m_comm … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
+ >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
]
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
- -Hdi -Hide >arith_c1 >arith_c1x #T #HT1 #HT2
+ -Hdi -Hide >arith_c1x #T #HT1 #HT2
lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid
lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct
elim (lift_trans_ge … HVW … HWU2 ?) -W // <minus_plus #W #HVW #HWU2
- elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=1/ #X #HLK #H
+ elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H
elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY
>(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=4/
| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
[ -Hdtd
lapply (lt_to_le_to_lt … (dt+et+e) Hidet ?) // -Hidet #Hidete
elim (lift_trans_ge … HVW … HWU2 ?) -W // <minus_plus #W #HVW #HWU2
- elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=1/ #X #HLK #H
+ elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H
elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY
>(lift_mono … HVY … HVW) -V #H destruct /2 width=4/
| -Hdti
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
@tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ]
- ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash, simplification like tps_lift_le is too slow *)
+ ] (**) (* /3 width=6/ is too slow, simplification like tps_lift_le is too slow *)
| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid
lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct
elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV
- elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/
+ elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=4/
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2
[ -Hdtd -Hidet
lapply (lt_to_le_to_lt … (dt + (et - e)) Hid ?) [ <le_plus_minus /2 width=1/ ] -Hdedet #Hidete
elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV
- elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/
+ elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=4/
| -Hdti -Hdedet
lapply (transitive_le … (i - e) Hdtd ?) /2 width=1/ -Hdtd #Hdtie
- lapply (plus_le_weak … Hid) #Hei
+ elim (le_inv_plus_l … Hid) #_ #Hei
lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
- elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: /2 width=1/ ] -Hid >arith_e2 // /4 width=4/
+ elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid
+ #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ /4 width=4/
]
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1 ? ?) -V1 // #W2 #HW12 #HWV2
- elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ]
+ elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] (**) (* 29s without the rewrites *)
/3 width=5/
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
]
| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
lapply (transitive_le … Hdedt … Hdti) #Hdei
- lapply (plus_le_weak … Hdedt) -Hdedt #Hedt
- lapply (plus_le_weak … Hdei) #Hei
+ elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt
+ elim (le_inv_plus_l … Hdei) #_ #Hei
lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct
lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
- elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: normalize /2 width=1/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
+ elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei
+ #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ #HV02
@ex2_1_intro /3 width=4/ (**) (* explicitc constructors *)
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- lapply (plus_le_weak … Hdetd) #Hedt
+ elim (le_inv_plus_l … Hdetd) #_ #Hedt
elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2
elim (IHU12 … HTU1 ?) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1/ ]
<plus_minus // /3 width=5/
∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫ T2 & ↑[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
-lapply (tps_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // <minus_plus_m_m /2 width=3/
qed.
lapply (IHU … HU0) -IHU #H
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
- lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2 width=1/ | /2 width=3/ ]
+ lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ]
]
qed.
[ //
| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
lapply (ldrop_fwd_lw … HLK1) normalize #H1
- elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 /2 width=1/ #X #H #HLK0
+ elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tps_fwd_tw … HV01) #H2
lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
[1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ]
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
]
qed.
[ /2 width=3/
| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
- elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: <plus_minus_m_m_comm // ]
+ elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: >commutative_plus /2 width=1/ ]
/3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
]
qed.
∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
-lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3/
qed.
(* ARITHMETICAL PROPERTIES **************************************************)
-lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
-#x #y #H elim (decidable_lt x y) /2 width=1/
-#Hxy elim (H Hxy)
-qed-.
+(* equations ****************************************************************)
-axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
+// qed.
-axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
+lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
+/2 by plus_minus/ qed.
-lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
-#n #m <plus_n_Sm #H destruct
-qed-.
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
+/2 by plus_minus/ qed.
-lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
-#n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b elim b -b
+[ #c #a #H >(le_n_O_to_eq … H) -H //
+| #b #IHb #c elim c -c //
+ #c #_ #a #Hcb
+ lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
+ <plus_n_Sm normalize /2 width=1/
+]
qed.
-lemma minus_le: ∀m,n. m - n ≤ m.
-/2 width=1/ 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 le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2 width=1/ qed.
+lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
+#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
+qed.
-lemma lt_to_le: ∀a,b. a < b → a ≤ b.
-/2 width=2/ qed.
+lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
+qed.
-lemma lt_refl_false: ∀n. n < n → False.
-#n #H elim (lt_to_not_eq … H) -H /2 width=1/
-qed-.
+lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
-lemma lt_zero_false: ∀n. n < 0 → False.
-#n #H elim (lt_to_not_le … H) -H /2 width=1/
-qed-.
+lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
+ a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
+#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
+qed.
+
+(* inversion & forward lemmas ***********************************************)
+
+axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+
+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.
+qed-.
lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
#m elim m -m
| #m #IHm * /2 width=1/
#n elim (IHm n) -IHm #H
[ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
-qed.
+qed-.
-lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
-/2 width=1/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
+lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
+/2 by le_plus_to_le/ qed-.
-lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
-/2 width=2/ qed.
+lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
+/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-.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2 width=1/
+qed-.
+
+lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
+#n #m <plus_n_Sm #H destruct
+qed-.
lemma plus_lt_false: ∀m,n. m + n < m → False.
#m #n #H1 lapply (le_plus_n_r n m) #H2
elim (lt_refl_false … H)
qed-.
+lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
+#x #y #H elim (decidable_lt x y) /2 width=1/
+#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 elim H -m1
[ /2 width=2/
-| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=1/
+| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/
]
-qed.
+qed-.
+
+(* backward lemmas **********************************************************)
lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
#p #q #n #H1 #H2
@lt_plus_to_minus_r <plus_minus_m_m //.
qed.
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2 width=1/ qed.
-
-lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
-/2 width=1/ qed.
+(* unstable *****************************************************************)
-lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
-// qed.
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+#j #i #e #d #H lapply (le_plus_to_minus_r … H) -H /2 width=3/
+qed.
-lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
-#n #m #p #lepm @plus_to_minus <associative_plus
->(commutative_plus p) <plus_minus_m_m //
+lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
+#a #b1 #b2 #c1 #H1 #H2 #H3
+>plus_minus // @monotonic_lt_minus_l //
qed.
-lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
-#b elim b -b
-[ #c #a #H >(le_O_to_eq_O … H) -H //
-| #b #IHb #c elim c -c //
- #c #_ #a #Hcb
- lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
- <plus_n_Sm normalize /2 width=1/
-]
+lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
+#a #b #c #d #e #H
+>minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
qed.
+(* remove *******************************************************************)
+(*
lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
// qed.
-lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3 width=1/ qed.
+lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
+/2 by ltn_to_ltO/ qed.
-lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
-/2 width=1/ qed.
+lemma minus_le: ∀m,n. m - n ≤ m.
+/2 by monotonic_le_minus_l/ qed.
-lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
-/2 width=1/ qed.
+lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
+/2 by le_n_O_to_eq/ qed.
-lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
-/2 width=1/ qed.
+lemma lt_to_le: ∀a,b. a < b → a ≤ b.
+/2 by le_plus_b/ qed.
-lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
-/2 width=1/ qed.
+lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
+/2 by le_to_or_lt_eq/ qed.
-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
-qed.
+lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
+/2 by le_plus_b/ qed.
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
-qed.
+lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
+/2 by le_plus_to_minus_r/ qed.
+
+lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
+/2 by monotonic_lt_minus_l/ qed.
+
+lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
+/2 by plus_minus/ qed.
lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
// qed.
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-#x #a #b #c1 >plus_plus_comm_23 //
-qed.
-
lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
-/2 width=1/ qed.
+/2 by plus_minus/ qed.
lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
-/3 width=1/ qed.
+/2 by minus_le_minus_minus_comm/ qed.
lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
-#a #b #c1 #H >minus_plus <minus_minus //
+/2 by minus_le_minus_minus_comm/
qed.
lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
-/2 width=1/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
- a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2 width=1/
-qed.
+/2 by arith_b1/ qed.
lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
-/2 width=1/ qed.
+/2 by plus_minus_m_m/ qed.
lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
// qed.
-(* unstable *****************************************************************)
-
lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
-/2 width=2/ qed.
-
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-#j #i #e #d #H lapply (plus_le_minus … H) -H /2 width=3/
-qed.
+/2 by le_plus_to_le/ qed.
lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
-/2 width=1/ qed.
+/2 by le_minus_to_plus/ qed.
lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
-/2 width=1/ qed.
-
-lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
-#a #b1 #b2 #c1 #H1 #H2 #H3
-<le_plus_minus_comm // @monotonic_lt_minus_l //
-qed.
+/2 by arith3/ qed.
lemma arith8: ∀a,b. a < a + b + 1.
// qed.
lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
// qed.
-lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
-#a #b #c #d #e #H
->minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
-qed.
+(* backward form of le_inv_plus_l *)
+lemma P2: ∀x,y,z. x ≤ z - y → y ≤ z → x + y ≤ z.
+/2 by le_minus_to_plus_r/ qed.
+*)
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-(* Subsets ******************************************************************)
-
-notation "hvbox( T ϵ break R )"
- non associative with precedence 45
- for @{ 'InSubset $T $R }.
-
(* Lists ********************************************************************)
notation "hvbox( hd break :: tl )"
right associative with precedence 47
for @{'Cons $hd $tl}.
-notation "hvbox( l1 break @ l2)"
+notation "hvbox( l1 break @ l2 )"
right associative with precedence 47
for @{'Append $l1 $l2 }.
include "basics/star.ma".
include "Ground_2/xoa_props.ma".
-(* PROPERTIES of RELATIONS **************************************************)
+(* PROPERTIES OF RELATIONS **************************************************)
-definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
+definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False).
-definition Decidable: Prop → Prop ≝
- λR. R ∨ (R → False).
+definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+ ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & R1 a2 a.
-definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
- ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
- ∃∃a. R2 a1 a & R1 a2 a.
+definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+ ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & R1 a a2.
-definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
- ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
- ∃∃a. R2 a1 a & R1 a a2.
-
-lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
+lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
∃∃a. R2 a1 a & TC … R1 a2 a.
#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
]
qed.
-lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
+lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 →
∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
∃∃a. TC … R2 a1 a & R1 a2 a.
#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
]
qed.
-lemma TC_confluent: ∀A,R1,R2.
- confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
+lemma TC_confluent2: ∀A,R1,R2.
+ confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2).
#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
[ #a1 #Ha01 #a2 #Ha02
elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
]
qed.
-lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
- R a1 a → TC … R a a2 → TC … R a1 a2.
-/3 width=3/ qed.
-
-lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
+lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 →
∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
∃∃a. R2 a1 a & TC … R1 a a2.
#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
]
qed.
-lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
+lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 →
∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
∃∃a. TC … R2 a1 a & R1 a a2.
#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
]
qed.
-lemma TC_transitive: ∀A,R1,R2.
- transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
+lemma TC_transitive2: ∀A,R1,R2.
+ transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2).
#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
[ #a0 #Ha10 #a2 #Ha02
elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
]
qed.
-lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
-/2 width=1/ qed.
-
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
- P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
- ∀a2. TC … R a1 a2 → P a2.
-#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
-qed.
-
definition NF: ∀A. relation A → relation A → predicate A ≝
λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
projects / helm.git / commitdiff