]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / arith_etc.txt
1 (* Equalities ***************************************************************)
2
3 (*** plus_minus_plus_plus_l *) (**)
4 lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
5 #H1 #H2 #H3 #H4
6 <nplus_assoc <nminus_plus_dx_bi // qed-.
7
8 fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
9 /2 width=1 by plus_minus_minus_be/ qed-.
10
11 (* Properties ***************************************************************)
12
13 (*** lt_plus_Sn_r *) (**)
14 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
15 /2 width=1/ qed-.
16
17 (* Inversion & forward lemmas ***********************************************)
18
19 lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
20 #y #z #x elim x -x /3 width=1 by le_S_S_to_le/
21 #H elim (le_plus_xSy_O_false … H)
22 qed-.
23
24 lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
25 /2 width=4 by le_plus_xySz_x_false/ qed-.
26
27 lemma nat_elim_le_sn (Q:relation …):
28       (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
29       ∀n1,n2. n1 ≤ n2 → Q n1 n2.
30 #Q #IH #n1 #n2 #Hn
31 <(minus_minus_m_m … Hn) -Hn
32 lapply (minus_le n2 n1)
33 let d ≝ (n2-n1)
34 @(nat_elim1 … d) -d -n1 #d
35 @pull_2 #Hd
36 <(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
37 let n1 ≝ (n2-d) #IHd
38 @IH -IH [| // ] #m #Hn
39 /4 width=3 by lt_to_le, lt_to_le_to_lt/
40 qed-.
41
42 (* Decidability of predicates ***********************************************)
43
44 lemma dec_min (R:predicate nat):
45       (∀n. Decidable … (R n)) → ∀n. R n →
46       ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
47 #R #HR #n
48 @(nat_elim1 n) -n #n #IH #Hn
49 elim (dec_lt … HR n) -HR [ -Hn | -IH ]
50 [ * #p #Hpn #Hp
51   elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
52   @(ex3_intro … Hm HNm) -HNm
53   /3 width=3 by lt_to_le, le_to_lt_to_lt/
54 | /4 width=4 by ex3_intro, ex2_intro/
55 ]
56 qed-.