source: src/ASM/new-matita-development/Util.ma @ 688

Last change on this file since 688 was 475, checked in by mulligan, 10 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

File size: 4.4 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/list.ma".
3include "basics/sums.ma".
4
5definition if_then_else ≝
6  λA: Type[0].
7  λb: bool.
8  λt: A.
9  λf: A.
10  match b with
11  [ true ⇒ t
12  | false ⇒ f
13  ].
14   
15notation "hvbox('if' b 'then' t 'else' f)"
16  non associative with precedence 83
17  for @{ 'if_then_else $b $t $f }.
18
19interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
20
21let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
22                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
23  match l with
24    [ nil ⇒ x
25    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
26    ].
27
28definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
29
30lemma eq_rect_Type0_r :
31  ∀A: Type[0].
32  ∀a:A.
33  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
34  #A #a #P #H #x #p
35  generalize in match H
36  generalize in match P
37  cases p
38  //
39qed.
40
41
42notation "hvbox(t⌈o ↦ h⌉)"
43  with precedence 45
44  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
45
46definition function_apply ≝
47  λA, B: Type[0].
48  λf: A → B.
49  λa: A.
50    f a.
51   
52notation "f break $ x"
53  left associative with precedence 99
54  for @{ 'function_apply $f $x }.
55 
56interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
57
58let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
59  match n with
60    [ O ⇒ a
61    | S o ⇒ f (iterate A f a o)
62    ].
63   
64notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
65 with precedence 10
66for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
67
68notation "⊥" with precedence 90
69  for @{ match ? in False with [ ] }.
70
71let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
72  match b with
73    [ true ⇒
74      match c with
75        [ false ⇒ true
76        | true ⇒ false
77        ]
78    | false ⇒
79      match c with
80        [ false ⇒ false
81        | true ⇒ true
82        ]
83    ].
84
85definition ltb ≝
86  λm, n: nat.
87    leb (S m) n.
88   
89definition geb ≝
90  λm, n: nat.
91    ltb n m.
92
93definition gtb ≝
94  λm, n: nat.
95    leb n m.
96
97interpretation "Nat less than" 'lt m n = (ltb m n).
98interpretation "Nat greater than" 'gt m n = (gtb m n).
99interpretation "Nat greater than eq" 'geq m n = (geb m n).
100
101let rec division_aux (m: nat) (n : nat) (p: nat) ≝
102  match ltb n p with
103    [ true ⇒ O
104    | false ⇒
105      match m with
106        [ O ⇒ O
107        | (S q) ⇒ S (division_aux q (n - (S p)) p)
108        ]
109    ].
110   
111definition division ≝
112  λm, n: nat.
113    match n with
114      [ O ⇒ S m
115      | S o ⇒ division_aux m m o
116      ].
117     
118notation "hvbox(n break ÷ m)"
119  right associative with precedence 47
120  for @{ 'division $n $m }.
121 
122interpretation "Nat division" 'division n m = (division n m).
123
124let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
125  match leb n p with
126    [ true ⇒ n
127    | false ⇒
128      match m with
129        [ O ⇒ n
130        | S o ⇒ modulus_aux o (n - (S p)) p
131        ]
132    ].
133   
134definition modulus ≝
135  λm, n: nat.
136    match n with
137      [ O ⇒ m
138      | S o ⇒ modulus_aux m m o
139      ].
140   
141notation "hvbox(n break 'mod' m)"
142  right associative with precedence 47
143  for @{ 'modulus $n $m }.
144 
145interpretation "Nat modulus" 'modulus m n = (modulus m n).
146
147definition divide_with_remainder ≝
148  λm, n: nat.
149    mk_pair ? ? (m ÷ n) (modulus m n).
150   
151let rec exponential (m: nat) (n: nat) on n ≝
152  match n with
153    [ O ⇒ S O
154    | S o ⇒ m * exponential m o
155    ].
156
157interpretation "Nat exponential" 'exp n m = (exponential n m).
158   
159notation "hvbox(a break ⊎ b)"
160 left associative with precedence 50
161for @{ 'disjoint_union $a $b }.
162interpretation "sum" 'disjoint_union A B = (Sum A B).
163
164theorem less_than_or_equal_monotone:
165  ∀m, n: nat.
166    m ≤ n → (S m) ≤ (S n).
167 #m #n #H
168 elim H
169 /2/
170qed.
171
172theorem less_than_or_equal_b_complete:
173  ∀m, n: nat.
174    leb m n = false → ¬(m ≤ n).
175 #m;
176 elim m;
177 normalize
178 [ #n #H
179   destruct
180 | #y #H1 #z
181   cases z
182   normalize
183   [ #H
184     /2/
185   | /3/
186   ]
187 ]
188qed.
189
190theorem less_than_or_equal_b_correct:
191  ∀m, n: nat.
192    leb m n = true → m ≤ n.
193 #m
194 elim m
195 //
196 #y #H1 #z
197 cases z
198 normalize
199 [ #H
200   destruct
201 | /3/
202 ]
203qed.
204
205definition less_than_or_equal_b_elim:
206 ∀m, n: nat.
207 ∀P: bool → Type[0].
208   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
209 #m #n #P #H1 #H2;
210 lapply (less_than_or_equal_b_correct m n)
211 lapply (less_than_or_equal_b_complete m n)
212 cases (leb m n)
213 /3/
214qed.
Note: See TracBrowser for help on using the repository browser.