]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
definition of equivalence for local environments,
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "arithmetics/nat.ma".
16 include "ground_2/lib/star.ma".
17
18 (* ARITHMETICAL PROPERTIES **************************************************)
19
20 (* Equations ****************************************************************)
21
22 lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
23 // qed.
24
25 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
26 /2 by plus_minus/ qed.
27
28 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
29 /2 by plus_minus/ qed.
30
31 lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
32 // qed.
33
34 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
35 #a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
36 qed.
37
38 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
39 #a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
40 qed.
41
42 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
43 /3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
44
45 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
46                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
47 #a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
48 qed.
49
50 lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
51 /2 width=1 by plus_minus/ qed-.
52
53 (* Properties ***************************************************************)
54
55 lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
56 /3 width=1 by monotonic_le_minus_l/ qed.
57
58 lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
59 /3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
60
61 lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
62 #z #x #y #n #Hzx #Hxny
63 >plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
64 >plus_minus [2: /2 width=1 by lt_to_le/ ]
65 /2 width=1 by monotonic_le_minus_l2/
66 qed.
67
68 lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
69 #z #x #y #n #Hzx #Hyxn
70 >plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
71 >plus_minus [2: /2 width=1 by lt_to_le/ ]
72 /2 width=1 by monotonic_le_minus_l2/
73 qed.
74
75 (* Inversion & forward lemmas ***********************************************)
76
77 axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
78
79 axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
80
81 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
82 #m #n elim (lt_or_ge m n) /2 width=1/
83 #H elim H -m /2 width=1/
84 #m #Hm * #H /2 width=1/ /3 width=1/
85 qed-.
86
87 lemma lt_refl_false: ∀n. n < n → ⊥.
88 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
89 qed-.
90
91 lemma lt_zero_false: ∀n. n < 0 → ⊥.
92 #n #H elim (lt_to_not_le … H) -H /2 width=1/
93 qed-.
94
95 lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
96 #x #y #H elim (decidable_lt x y) /2 width=1/
97 #Hxy elim (H Hxy)
98 qed-.
99
100 lemma pred_inv_refl: ∀m. pred m = m → m = 0.
101 * // normalize #m #H elim (lt_refl_false m) //
102 qed-.
103
104 lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
105 #y #z #x elim x -x
106 [ #H lapply (le_n_O_to_eq … H) -H
107   <plus_n_Sm #H destruct
108 | /3 width=1 by le_S_S_to_le/
109 ]
110 qed-.
111
112 lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
113 /2 width=4 by le_plus_xySz_x_false/ qed-.
114
115 lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
116 /2 width=4 by plus_xySz_x_false/ qed-.
117
118 (* Iterators ****************************************************************)
119
120 (* Note: see also: lib/arithemetcs/bigops.ma *)
121 let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
122   match n with
123    [ O   ⇒ nil
124    | S k ⇒ op (iter k B op nil)
125    ].
126
127 interpretation "iterated function" 'exp op n = (iter n ? op).
128
129 lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
130 #B #f #b #l >commutative_plus //
131 qed.
132
133 lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
134 #B #f #b #l elim l -l normalize //
135 qed.
136
137 (* Trichotomy operator ******************************************************)
138
139 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
140 let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
141   match n1 with
142   [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
143   | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
144   ].
145
146 lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1.
147 #A #a1 #a2 #a3 #n2 elim n2 -n2
148 [ #n1 #H elim (lt_zero_false … H)
149 | #n2 #IH #n1 elim n1 -n1 // /3 width=1/
150 ]
151 qed.
152
153 lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
154 #A #a1 #a2 #a3 #n elim n -n normalize //
155 qed.
156
157 lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
158 #A #a1 #a2 #a3 #n1 elim n1 -n1
159 [ #n2 #H elim (lt_zero_false … H)
160 | #n1 #IH #n2 elim n2 -n2 // /3 width=1/
161 ]
162 qed.