source:Deliverables/D4.1/Matita/Util.ma@557

Last change on this file since 557 was 465, checked in by mulligan, 9 years ago

Moved over to standard library.

File size: 4.1 KB
Line
1include "arithmetics/nat.ma".
2include "datatypes/pairs.ma".
3include "datatypes/sums.ma".
4include "datatypes/list.ma".
5
6nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0])
7                         (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
8  match l with
9    [ nil ⇒ x
10    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
11    ].
12
13ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
14
15
16ndefinition function_apply ≝
17  λA, B: Type[0].
18  λf: A → B.
19  λa: A.
20    f a.
21
22notation "f break \$ x"
23  left associative with precedence 99
24  for @{ 'function_apply \$f \$x }.
25
26interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
27
28nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
29  match n with
30    [ O ⇒ a
31    | S o ⇒ f (iterate A f a o)
32    ].
33
34notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
35 with precedence 10
36for @{ match \$t with [ mk_pair \${ident x} \${ident y} ⇒ \$s ] }.
37
38
39notation "⊥" with precedence 90
40  for @{ match ? in False with [ ] }.
41
42nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝
43  match b with
44    [ true ⇒ t
45    | false ⇒ f
46    ].
47
48notation "hvbox('if' b 'then' t 'else' f)"
49  non associative with precedence 83
50  for @{ 'if_then_else \$b \$t \$f }.
51
52interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
53
54nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝
55  match b with
56    [ true ⇒
57      match c with
58        [ false ⇒ true
59        | true ⇒ false
60        ]
61    | false ⇒
62      match c with
63        [ false ⇒ false
64        | true ⇒ true
65        ]
66    ].
67
68ndefinition ltb ≝
69  λm, n: nat.
70    leb (S m) n.
71
72ndefinition geb ≝
73  λm, n: nat.
74    ltb n m.
75
76ndefinition gtb ≝
77  λm, n: nat.
78    leb n m.
79
80interpretation "Nat less than" 'lt m n = (ltb m n).
81interpretation "Nat greater than" 'gt m n = (gtb m n).
82interpretation "Nat greater than eq" 'geq m n = (geb m n).
83
84nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝
85  match ltb n p with
86    [ true ⇒ O
87    | false ⇒
88      match m with
89        [ O ⇒ O
90        | (S q) ⇒ S (division_aux q (n - (S p)) p)
91        ]
92    ].
93
94ndefinition division ≝
95  λm, n: nat.
96    match n with
97      [ O ⇒ S m
98      | S o ⇒ division_aux m m o
99      ].
100
101notation "hvbox(n break ÷ m)"
102  right associative with precedence 47
103  for @{ 'division \$n \$m }.
104
105interpretation "Nat division" 'division n m = (division n m).
106
107nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
108  match leb n p with
109    [ true ⇒ n
110    | false ⇒
111      match m with
112        [ O ⇒ n
113        | S o ⇒ modulus_aux o (n - (S p)) p
114        ]
115    ].
116
117ndefinition modulus ≝
118  λm, n: nat.
119    match n with
120      [ O ⇒ m
121      | S o ⇒ modulus_aux m m o
122      ].
123
124notation "hvbox(n break 'mod' m)"
125  right associative with precedence 47
126  for @{ 'modulus \$n \$m }.
127
128interpretation "Nat modulus" 'modulus m n = (modulus m n).
129
130ndefinition divide_with_remainder ≝
131  λm, n: nat.
132    mk_pair ? ? (m ÷ n) (modulus m n).
133
134nlet rec exponential (m: nat) (n: nat) on n ≝
135  match n with
136    [ O ⇒ S O
137    | S o ⇒ m * exponential m o
138    ].
139
140interpretation "Nat exponential" 'exp n m = (exponential n m).
141
142notation "hvbox(a break ⊎ b)"
143 left associative with precedence 50
144for @{ 'disjoint_union \$a \$b }.
145interpretation "sum" 'disjoint_union A B = (Sum A B).
146
147ntheorem less_than_or_equal_monotone:
148  ∀m, n: nat.
149    m ≤ n → (S m) ≤ (S n).
150 #m n H; nelim H; /2/.
151nqed.
152
153ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n).
154 #m; nelim m; nnormalize
155  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
156    [ #H; /2/ | /3/ ]
157nqed.
158
159ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n.
160 #m; nelim m; //; #y H1 z; ncases z; nnormalize
161  [ #H; ndestruct | /3/ ]
162nqed.
163
164ndefinition less_than_or_equal_b_elim:
165 ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
166  P (leb m n).
167 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
168 nlapply (less_than_or_equal_b_complete m n);
169 ncases (leb m n); /3/.
170nqed.
Note: See TracBrowser for help on using the repository browser.