source: src/ASM/Util.ma @ 2055

Last change on this file since 2055 was 2055, checked in by sacerdot, 8 years ago

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

File size: 33.6 KB
Line 
1include "basics/lists/list.ma".
2include "basics/types.ma".
3include "arithmetics/nat.ma".
4include "basics/russell.ma".
5
6(* let's implement a daemon not used by automation *)
7inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
8axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
9example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
10example not_implemented: False. cases daemon qed.
11
12notation "⊥" with precedence 90
13  for @{ match ? in False with [ ] }.
14notation "Ⓧ" with precedence 90
15  for @{ λabs.match abs in False with [ ] }.
16
17
18definition ltb ≝
19  λm, n: nat.
20    leb (S m) n.
21   
22definition geb ≝
23  λm, n: nat.
24    leb n m.
25
26definition gtb ≝
27  λm, n: nat.
28    ltb n m.
29
30(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
31let rec eq_nat (n: nat) (m: nat) on n: bool ≝
32  match n with
33  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
34  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
35  ].
36
37let rec forall
38  (A: Type[0]) (f: A → bool) (l: list A)
39    on l ≝
40  match l with
41  [ nil        ⇒ true
42  | cons hd tl ⇒ f hd ∧ forall A f tl
43  ].
44
45let rec prefix
46  (A: Type[0]) (k: nat) (l: list A)
47    on l ≝
48  match l with
49  [ nil ⇒ [ ]
50  | cons hd tl ⇒
51    match k with
52    [ O ⇒ [ ]
53    | S k' ⇒ hd :: prefix A k' tl
54    ]
55  ].
56 
57let rec fold_left2
58  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
59  (left: list B) (right: list C) (proof: |left| = |right|)
60    on left: A ≝
61  match left return λx. |x| = |right| → A with
62  [ nil ⇒ λnil_prf.
63    match right return λx. |[ ]| = |x| → A with
64    [ nil ⇒ λnil_nil_prf. accu
65    | cons hd tl ⇒ λcons_nil_absrd. ?
66    ] nil_prf
67  | cons hd tl ⇒ λcons_prf.
68    match right return λx. |hd::tl| = |x| → A with
69    [ nil ⇒ λcons_nil_absrd. ?
70    | cons hd' tl' ⇒ λcons_cons_prf.
71        fold_left2 …  f (f accu hd hd') tl tl' ?
72    ] cons_prf
73  ] proof.
74  [ 1: normalize in cons_nil_absrd;
75       destruct(cons_nil_absrd)
76  | 2: normalize in cons_nil_absrd;
77       destruct(cons_nil_absrd)
78  | 3: normalize in cons_cons_prf;
79       @injective_S
80       assumption
81  ]
82qed.
83
84let rec remove_n_first_internal
85  (i: nat) (A: Type[0]) (l: list A) (n: nat)
86    on l ≝
87  match l with
88  [ nil ⇒ [ ]
89  | cons hd tl ⇒
90    match eq_nat i n with
91    [ true ⇒ l
92    | _ ⇒ remove_n_first_internal (S i) A tl n
93    ]
94  ].
95
96definition remove_n_first ≝
97  λA: Type[0].
98  λn: nat.
99  λl: list A.
100    remove_n_first_internal 0 A l n.
101   
102let rec foldi_from_until_internal
103  (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
104    on rem ≝
105  match rem with
106  [ nil ⇒ res
107  | cons e tl ⇒
108    match geb i m with
109    [ true ⇒ res
110    | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
111    ]
112  ].
113
114definition foldi_from_until ≝
115  λA: Type[0].
116  λn: nat.
117  λm: nat.
118  λf: ?.
119  λa: ?.
120  λl: ?.
121    foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
122
123definition foldi_from ≝
124  λA: Type[0].
125  λn.
126  λf.
127  λa.
128  λl.
129    foldi_from_until A n (|l|) f a l.
130
131definition foldi_until ≝
132  λA: Type[0].
133  λm.
134  λf.
135  λa.
136  λl.
137    foldi_from_until A 0 m f a l.
138
139definition foldi ≝
140  λA: Type[0].
141  λf.
142  λa.
143  λl.
144    foldi_from_until A 0 (|l|) f a l.
145
146definition hd_safe ≝
147  λA: Type[0].
148  λl: list A.
149  λproof: 0 < |l|.
150  match l return λx. 0 < |x| → A with
151  [ nil ⇒ λnil_absrd. ?
152  | cons hd tl ⇒ λcons_prf. hd
153  ] proof.
154  normalize in nil_absrd;
155  cases(not_le_Sn_O 0)
156  #HYP
157  cases(HYP nil_absrd)
158qed.
159
160definition tail_safe ≝
161  λA: Type[0].
162  λl: list A.
163  λproof: 0 < |l|.
164  match l return λx. 0 < |x| → list A with
165  [ nil ⇒ λnil_absrd. ?
166  | cons hd tl ⇒ λcons_prf. tl
167  ] proof.
168  normalize in nil_absrd;
169  cases(not_le_Sn_O 0)
170  #HYP
171  cases(HYP nil_absrd)
172qed.
173
174let rec safe_split
175  (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
176    on index ≝
177  match index return λx. x ≤ |l| → (list A) × (list A) with
178  [ O ⇒ λzero_prf. 〈[], l〉
179  | S index' ⇒ λsucc_prf.
180    match l return λx. S index' ≤ |x| → (list A) × (list A) with
181    [ nil ⇒ λnil_absrd. ?
182    | cons hd tl ⇒ λcons_prf.
183      let 〈l1, l2〉 ≝ safe_split A tl index' ? in
184        〈hd :: l1, l2〉
185    ] succ_prf
186  ] proof.
187  [1: normalize in nil_absrd;
188      cases(not_le_Sn_O index')
189      #HYP
190      cases(HYP nil_absrd)
191  |2: normalize in cons_prf;
192      @le_S_S_to_le
193      assumption
194  ]
195qed.
196
197let rec nth_safe
198  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
199  (proof: index < | the_list |)
200    on index ≝
201  match index return λs. s < | the_list | → elt_type with
202  [ O ⇒
203    match the_list return λt. 0 < | t | → elt_type with
204    [ nil        ⇒ λnil_absurd. ?
205    | cons hd tl ⇒ λcons_proof. hd
206    ]
207  | S index' ⇒
208    match the_list return λt. S index' < | t | → elt_type with
209    [ nil ⇒ λnil_absurd. ?
210    | cons hd tl ⇒
211      λcons_proof. nth_safe elt_type index' tl ?
212    ]
213  ] proof.
214  [ normalize in nil_absurd;
215    cases (not_le_Sn_O 0)
216    #ABSURD
217    elim (ABSURD nil_absurd)
218  | normalize in nil_absurd;
219    cases (not_le_Sn_O (S index'))
220    #ABSURD
221    elim (ABSURD nil_absurd)
222  | normalize in cons_proof;
223    @le_S_S_to_le
224    assumption
225  ]
226qed.
227
228lemma shift_nth_safe:
229 ∀T,i,l2,l1,K1,K2.
230  nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
231 #T #i #l2 elim l2 normalize
232  [ #l1 #K1 <plus_n_O #K2 %
233  | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
234    whd in ⊢ (???%); @IH ]
235qed.
236
237lemma shift_nth_prefix:
238 ∀T,l1,i,l2,K1,K2.
239  nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
240  #T #l1 elim l1 normalize
241  [
242    #i #l1 #K1 cases(lt_to_not_zero … K1)
243  |
244    #hd #tl #IH #i #l2
245    cases i
246    [
247      //
248    |
249      #i' #K1 #K2 whd in ⊢ (??%%);
250      @IH
251    ]
252  ]
253qed.
254
255
256definition last_safe ≝
257  λelt_type: Type[0].
258  λthe_list: list elt_type.
259  λproof   : 0 < | the_list |.
260    nth_safe elt_type (|the_list| - 1) the_list ?.
261  normalize /2 by lt_plus_to_minus/
262qed.
263
264let rec reduce
265  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
266  match left with
267  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
268  | cons hd tl ⇒
269    match right with
270    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
271    | cons hd' tl' ⇒
272      let 〈cleft, cright〉 ≝ reduce A B tl tl' in
273      let 〈commonl, restl〉 ≝ cleft in
274      let 〈commonr, restr〉 ≝ cright in
275        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
276    ]
277  ].
278
279(*
280axiom reduce_strong:
281  ∀A: Type[0].
282  ∀left: list A.
283  ∀right: list A.
284    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
285*)
286
287let rec reduce_strong
288  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
289    on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
290  match left with
291  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
292  | cons hd tl ⇒
293    match right with
294    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
295    | cons hd' tl' ⇒
296      let 〈cleft, cright〉 ≝ pi1 ?? (reduce_strong A B tl tl') in
297      let 〈commonl, restl〉 ≝ cleft in
298      let 〈commonr, restr〉 ≝ cright in
299        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
300    ]
301  ].
302  [ 1: normalize %
303  | 2: normalize %
304  | 3: normalize >p3 in p2; >p4 cases (reduce_strong … tl tl1) normalize
305       #X #H #EQ destruct // ]
306qed.
307   
308let rec map2_opt
309  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
310  (left: list A) (right: list B) on left ≝
311  match left with
312  [ nil ⇒
313    match right with
314    [ nil ⇒ Some ? (nil C)
315    | _ ⇒ None ?
316    ]
317  | cons hd tl ⇒
318    match right with
319    [ nil ⇒ None ?
320    | cons hd' tl' ⇒
321      match map2_opt A B C f tl tl' with
322      [ None ⇒ None ?
323      | Some tail ⇒ Some ? (f hd hd' :: tail)
324      ]
325    ]
326  ].
327
328let rec map2
329  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
330  (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
331  match left return λx. | x | = | right | → list C with
332  [ nil ⇒
333    match right return λy. | [] | = | y | → list C with
334    [ nil ⇒ λnil_prf. nil C
335    | _ ⇒ λcons_absrd. ?
336    ]
337  | cons hd tl ⇒
338    match right return λy. | hd::tl | = | y | → list C with
339    [ nil ⇒ λnil_absrd. ?
340    | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
341    ]
342  ] proof.
343  [1: normalize in cons_absrd;
344      destruct(cons_absrd)
345  |2: normalize in nil_absrd;
346      destruct(nil_absrd)
347  |3: normalize in cons_prf;
348      destruct(cons_prf)
349      assumption
350  ]
351qed.
352
353let rec map3
354  (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
355  (left: list A) (centre: list B) (right: list C)
356  (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
357  match left return λx. |x| = |centre| → list D with
358  [ nil ⇒ λnil_prf.
359    match centre return λx. |x| = |right| → list D with
360    [ nil ⇒ λnil_nil_prf.
361      match right return λx. |nil ?| = |x| → list D with
362      [ nil        ⇒ λnil_nil_nil_prf. nil D
363      | cons hd tl ⇒ λcons_nil_nil_absrd. ?
364      ] nil_nil_prf
365    | cons hd tl ⇒ λnil_cons_absrd. ?
366    ] prfcr
367  | cons hd tl ⇒ λcons_prf.
368    match centre return λx. |x| = |right| → list D with
369    [ nil ⇒ λcons_nil_absrd. ?
370    | cons hd' tl' ⇒ λcons_cons_prf.
371      match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
372      [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
373      | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
374        (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
375      ] (refl ? (|right|)) cons_cons_prf
376    ] prfcr
377  ] prflc.
378  [ 1: normalize in cons_nil_nil_absrd;
379       destruct(cons_nil_nil_absrd)
380  | 2: generalize in match nil_cons_absrd;
381       <prfcr <nil_prf #HYP
382       normalize in HYP;
383       destruct(HYP)
384  | 3: generalize in match cons_nil_absrd;
385       <prfcr <cons_prf #HYP
386       normalize in HYP;
387       destruct(HYP)
388  | 4: normalize in cons_cons_nil_absrd;
389       destruct(cons_cons_nil_absrd)
390  | 5: normalize in cons_cons_cons_prf;
391       destruct(cons_cons_cons_prf)
392       assumption
393  | 6: generalize in match cons_cons_cons_prf;
394       <refl_prf <prfcr <cons_prf #HYP
395       normalize in HYP;
396       destruct(HYP)
397       @sym_eq assumption
398  ]
399qed.
400 
401lemma eq_rect_Type0_r :
402  ∀A: Type[0].
403  ∀a:A.
404  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
405  #A #a #P #H #x #p lapply H lapply P cases p //
406qed.
407 
408let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
409  match n return λo. o < length A l → A with
410  [ O ⇒
411    match l return λm. 0 < length A m → A with
412    [ nil ⇒ λabsd1. ?
413    | cons hd tl ⇒ λprf1. hd
414    ]
415  | S n' ⇒
416    match l return λm. S n' < length A m → A with
417    [ nil ⇒ λabsd2. ?
418    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
419    ]
420  ] ?.
421  [ 1:
422    @ p
423  | 4:
424    normalize in prf2;
425    normalize
426    @ le_S_S_to_le
427    assumption
428  | 2:
429    normalize in absd1;
430    cases (not_le_Sn_O O)
431    # H
432    elim (H absd1)
433  | 3:
434    normalize in absd2;
435    cases (not_le_Sn_O (S n'))
436    # H
437    elim (H absd2)
438  ]
439qed.
440 
441let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
442  match n with
443  [ O ⇒
444    match l with
445    [ nil ⇒ [ ]
446    | cons hd tl ⇒ l
447    ]
448  | S n ⇒
449    match l with
450    [ nil ⇒ [ ]
451    | cons hd tl ⇒
452      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
453    ]
454  ].
455 
456definition nub_by ≝
457  λA: Type[0].
458  λf: A → A → bool.
459  λl: list A.
460    nub_by_internal A f l (length ? l).
461 
462let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
463  match l with
464  [ nil ⇒ false
465  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
466  ].
467 
468let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
469  match n with
470  [ O ⇒ [ ]
471  | S n ⇒
472    match l with
473    [ nil ⇒ [ ]
474    | cons hd tl ⇒ hd :: take A n tl
475    ]
476  ].
477 
478let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
479  match n with
480  [ O ⇒ l
481  | S n ⇒
482    match l with
483    [ nil ⇒ [ ]
484    | cons hd tl ⇒ drop A n tl
485    ]
486  ].
487 
488definition list_split ≝
489  λA: Type[0].
490  λn: nat.
491  λl: list A.
492    〈take A n l, drop A n l〉.
493 
494let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
495                      (l: list A) on l: list B ≝
496  match l with
497  [ nil ⇒ nil ?
498  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
499  ]. 
500
501definition mapi ≝
502  λA, B: Type[0].
503  λf: nat → A → B.
504  λl: list A.
505    mapi_internal A B 0 f l.
506
507let rec zip_pottier
508  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
509    on left ≝
510  match left with
511  [ nil ⇒ [ ]
512  | cons hd tl ⇒
513    match right with
514    [ nil ⇒ [ ]
515    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
516    ]
517  ].
518
519let rec zip_safe
520  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
521    on left ≝
522  match left return λx. |x| = |right| → list (A × B) with
523  [ nil ⇒ λnil_prf.
524    match right return λx. |[ ]| = |x| → list (A × B) with
525    [ nil ⇒ λnil_nil_prf. [ ]
526    | cons hd tl ⇒ λnil_cons_absrd. ?
527    ] nil_prf
528  | cons hd tl ⇒ λcons_prf.
529    match right return λx. |hd::tl| = |x| → list (A × B) with
530    [ nil ⇒ λcons_nil_absrd. ?
531    | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
532    ] cons_prf
533  ] prf.
534  [ 1: normalize in nil_cons_absrd;
535       destruct(nil_cons_absrd)
536  | 2: normalize in cons_nil_absrd;
537       destruct(cons_nil_absrd)
538  | 3: normalize in cons_cons_prf;
539       @injective_S
540       assumption
541  ]
542qed.
543
544let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
545  match l with
546  [ nil ⇒ Some ? (nil (A × B))
547  | cons hd tl ⇒
548    match r with
549    [ nil ⇒ None ?
550    | cons hd' tl' ⇒
551      match zip ? ? tl tl' with
552      [ None ⇒ None ?
553      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
554      ]
555    ]
556  ].
557
558let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
559  match l with
560  [ nil ⇒ a
561  | cons hd tl ⇒ foldl A B f (f a hd) tl
562  ].
563
564lemma foldl_step:
565 ∀A:Type[0].
566  ∀B: Type[0].
567   ∀H: A → B → A.
568    ∀acc: A.
569     ∀pre: list B.
570      ∀hd:B.
571       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
572 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
573  [ normalize; //
574  | #hd #tl #IH #acc #X normalize; @IH ]
575qed.
576
577lemma foldl_append:
578 ∀A:Type[0].
579  ∀B: Type[0].
580   ∀H: A → B → A.
581    ∀acc: A.
582     ∀suff,pre: list B.
583      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
584 #A #B #H #acc #suff elim suff
585  [ #pre >append_nil %
586  | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
587qed.
588
589(* redirecting to library reverse *)
590definition rev ≝ reverse.
591
592lemma append_length:
593  ∀A: Type[0].
594  ∀l, r: list A.
595    |(l @ r)| = |l| + |r|.
596  #A #L #R
597  elim L
598  [ %
599  | #HD #TL #IH
600    normalize >IH %
601  ]
602qed.
603
604lemma append_nil:
605  ∀A: Type[0].
606  ∀l: list A.
607    l @ [ ] = l.
608  #A #L
609  elim L //
610qed.
611
612lemma rev_append:
613  ∀A: Type[0].
614  ∀l, r: list A.
615    rev A (l @ r) = rev A r @ rev A l.
616  #A #L #R
617  elim L
618  [ normalize >append_nil %
619  | #HD #TL normalize #IH
620    >rev_append_def
621    >rev_append_def
622    >rev_append_def
623    >append_nil
624    normalize
625    >IH
626    @associative_append
627  ]
628qed.
629
630lemma rev_length:
631  ∀A: Type[0].
632  ∀l: list A.
633    |rev A l| = |l|.
634  #A #L
635  elim L
636  [ %
637  | #HD #TL normalize #IH
638    >rev_append_def
639    >(append_length A (rev A TL) [HD])
640    normalize /2 by /
641  ]
642qed.
643
644lemma nth_append_first:
645 ∀A:Type[0].
646 ∀n:nat.∀l1,l2:list A.∀d:A.
647   n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
648 #A #n #l1 #l2 #d
649 generalize in match n; -n; elim l1
650 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
651 | #h #t #Hind #k normalize
652   cases k -k
653   [ #Hk normalize @refl
654   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
655   ] 
656 ]
657qed.
658
659lemma nth_append_second:
660 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
661  nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
662 #A #n #l1 #l2 #d
663 generalize in match n; -n; elim l1
664 [ normalize #k #Hk <(minus_n_O) @refl
665 | #h #t #Hind #k normalize
666   cases k -k;
667   [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
668   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
669   ]
670 ]
671qed.
672
673   
674let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
675                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
676  match l with
677    [ nil ⇒ x
678    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
679    ].
680
681definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
682
683notation "hvbox(t⌈o ↦ h⌉)"
684  with precedence 45
685  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
686
687definition function_apply ≝
688  λA, B: Type[0].
689  λf: A → B.
690  λa: A.
691    f a.
692   
693notation "f break $ x"
694  left associative with precedence 99
695  for @{ 'function_apply $f $x }.
696 
697interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
698
699let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
700  match n with
701    [ O ⇒ a
702    | S o ⇒ f (iterate A f a o)
703    ].
704
705let rec division_aux (m: nat) (n : nat) (p: nat) ≝
706  match ltb n (S p) with
707    [ true ⇒ O
708    | false ⇒
709      match m with
710        [ O ⇒ O
711        | (S q) ⇒ S (division_aux q (n - (S p)) p)
712        ]
713    ].
714   
715definition division ≝
716  λm, n: nat.
717    match n with
718      [ O ⇒ S m
719      | S o ⇒ division_aux m m o
720      ].
721     
722notation "hvbox(n break ÷ m)"
723  right associative with precedence 47
724  for @{ 'division $n $m }.
725 
726interpretation "Nat division" 'division n m = (division n m).
727
728let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
729  match leb n p with
730    [ true ⇒ n
731    | false ⇒
732      match m with
733        [ O ⇒ n
734        | S o ⇒ modulus_aux o (n - (S p)) p
735        ]
736    ].
737   
738definition modulus ≝
739  λm, n: nat.
740    match n with
741      [ O ⇒ m
742      | S o ⇒ modulus_aux m m o
743      ].
744   
745notation "hvbox(n break 'mod' m)"
746  right associative with precedence 47
747  for @{ 'modulus $n $m }.
748 
749interpretation "Nat modulus" 'modulus m n = (modulus m n).
750
751definition divide_with_remainder ≝
752  λm, n: nat.
753    mk_Prod … (m ÷ n) (modulus m n).
754   
755let rec exponential (m: nat) (n: nat) on n ≝
756  match n with
757    [ O ⇒ S O
758    | S o ⇒ m * exponential m o
759    ].
760
761interpretation "Nat exponential" 'exp n m = (exponential n m).
762   
763notation "hvbox(a break ⊎ b)"
764 left associative with precedence 55
765for @{ 'disjoint_union $a $b }.
766interpretation "sum" 'disjoint_union A B = (Sum A B).
767
768theorem less_than_or_equal_monotone:
769  ∀m, n: nat.
770    m ≤ n → (S m) ≤ (S n).
771 #m #n #H
772 elim H
773 /2 by le_n, le_S/
774qed.
775
776theorem less_than_or_equal_b_complete:
777  ∀m, n: nat.
778    leb m n = false → ¬(m ≤ n).
779 #m;
780 elim m;
781 normalize
782 [ #n #H
783   destruct
784 | #y #H1 #z
785   cases z
786   normalize
787   [ #H
788     /2 by /
789   | /3 by not_le_to_not_le_S_S/
790   ]
791 ]
792qed.
793
794theorem less_than_or_equal_b_correct:
795  ∀m, n: nat.
796    leb m n = true → m ≤ n.
797 #m
798 elim m
799 //
800 #y #H1 #z
801 cases z
802 normalize
803 [ #H
804   destruct
805 | #n #H lapply (H1 … H) /2 by le_S_S/
806 ]
807qed.
808
809definition less_than_or_equal_b_elim:
810 ∀m, n: nat.
811 ∀P: bool → Type[0].
812   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
813 #m #n #P #H1 #H2;
814 lapply (less_than_or_equal_b_correct m n)
815 lapply (less_than_or_equal_b_complete m n)
816 cases (leb m n)
817 /3 by /
818qed.
819
820lemma lt_m_n_to_exists_o_plus_m_n:
821  ∀m, n: nat.
822    m < n → ∃o: nat. m + o = n.
823  #m #n
824  cases m
825  [1:
826    #irrelevant
827    %{n} %
828  |2:
829    #m' #lt_hyp
830    %{(n - S m')}
831    >commutative_plus in ⊢ (??%?);
832    <plus_minus_m_m
833    [1:
834      %
835    |2:
836      @lt_S_to_lt
837      assumption
838    ]
839  ]
840qed.
841
842lemma lt_O_n_to_S_pred_n_n:
843  ∀n: nat.
844    0 < n → S (pred n) = n.
845  #n
846  cases n
847  [1:
848    #absurd
849    cases(lt_to_not_zero 0 0 absurd)
850  |2:
851    #n' #lt_hyp %
852  ]
853qed.
854
855lemma exists_plus_m_n_to_exists_Sn:
856  ∀m, n: nat.
857    m < n → ∃p: nat. S p = n.
858  #m #n
859  cases m
860  [1:
861    #lt_hyp %{(pred n)}
862    @(lt_O_n_to_S_pred_n_n … lt_hyp)
863  |2:
864    #m' #lt_hyp %{(pred n)}
865    @(lt_O_n_to_S_pred_n_n)
866    @(transitive_le … (S m') …)
867    [1:
868      //
869    |2:
870      @lt_S_to_lt
871      assumption
872    ]
873  ]
874qed.
875
876lemma plus_right_monotone:
877  ∀m, n, o: nat.
878    m = n → m + o = n + o.
879  #m #n #o #refl >refl %
880qed.
881
882lemma plus_left_monotone:
883  ∀m, n, o: nat.
884    m = n → o + m = o + n.
885  #m #n #o #refl destruct %
886qed.
887
888lemma minus_plus_cancel:
889  ∀m, n : nat.
890  ∀proof: n ≤ m.
891    (m - n) + n = m.
892  #m #n #proof /2 by plus_minus/
893qed.
894
895lemma lt_to_le_to_le:
896  ∀n, m, p: nat.
897    n < m → m ≤ p → n ≤ p.
898  #n #m #p #H #H1
899  elim H
900  [1:
901    @(transitive_le n m p) /2/
902  |2:
903    /2/
904  ]
905qed.
906
907lemma eqb_decidable:
908  ∀l, r: nat.
909    (eqb l r = true) ∨ (eqb l r = false).
910  #l #r //
911qed.
912
913lemma r_Sr_and_l_r_to_Sl_r:
914  ∀r, l: nat.
915    (∃r': nat. r = S r' ∧ l = r') → S l = r.
916  #r #l #exists_hyp
917  cases exists_hyp #r'
918  #and_hyp cases and_hyp
919  #left_hyp #right_hyp
920  destruct %
921qed.
922
923lemma eqb_Sn_to_exists_n':
924  ∀m, n: nat.
925    eqb (S m) n = true → ∃n': nat. n = S n'.
926  #m #n
927  cases n
928  [1:
929    normalize #absurd
930    destruct(absurd)
931  |2:
932    #n' #_ %{n'} %
933  ]
934qed.
935
936lemma eqb_true_to_eqb_S_S_true:
937  ∀m, n: nat.
938    eqb m n = true → eqb (S m) (S n) = true.
939  #m #n normalize #assm assumption
940qed.
941
942lemma eqb_S_S_true_to_eqb_true:
943  ∀m, n: nat.
944    eqb (S m) (S n) = true → eqb m n = true.
945  #m #n normalize #assm assumption
946qed.
947
948lemma eqb_true_to_refl:
949  ∀l, r: nat.
950    eqb l r = true → l = r.
951  #l
952  elim l
953  [1:
954    #r cases r
955    [1:
956      #_ %
957    |2:
958      #l' normalize
959      #absurd destruct(absurd)
960    ]
961  |2:
962    #l' #inductive_hypothesis #r
963    #eqb_refl @r_Sr_and_l_r_to_Sl_r
964    %{(pred r)} @conj
965    [1:
966      cases (eqb_Sn_to_exists_n' … eqb_refl)
967      #r' #S_assm >S_assm %
968    |2:
969      cases (eqb_Sn_to_exists_n' … eqb_refl)
970      #r' #refl_assm destruct normalize
971      @inductive_hypothesis
972      normalize in eqb_refl; assumption
973    ]
974  ]
975qed.
976
977lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
978  ∀r, l: nat.
979    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
980  #r #l #disj_hyp
981  cases disj_hyp
982  [1:
983    #r_O_refl destruct @nmk
984    #absurd destruct(absurd)
985  |2:
986    #exists_hyp cases exists_hyp #r'
987    #conj_hyp cases conj_hyp #left_conj #right_conj
988    destruct @nmk #S_S_refl_hyp
989    elim right_conj #hyp @hyp //
990  ]
991qed.
992
993lemma neq_l_r_to_neq_Sl_Sr:
994  ∀l, r: nat.
995    l ≠ r → S l ≠ S r.
996  #l #r #l_neq_r_assm
997  @nmk #Sl_Sr_assm cases l_neq_r_assm
998  #assm @assm //
999qed.
1000
1001lemma eqb_false_to_not_refl:
1002  ∀l, r: nat.
1003    eqb l r = false → l ≠ r.
1004  #l
1005  elim l
1006  [1:
1007    #r cases r
1008    [1:
1009      normalize #absurd destruct(absurd)
1010    |2:
1011      #r' #_ @nmk
1012      #absurd destruct(absurd)
1013    ]
1014  |2:
1015    #l' #inductive_hypothesis #r
1016    cases r
1017    [1:
1018      #eqb_false_assm
1019      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1020      @or_introl %
1021    |2:
1022      #r' #eqb_false_assm
1023      @neq_l_r_to_neq_Sl_Sr
1024      @inductive_hypothesis
1025      assumption
1026    ]
1027  ]
1028qed.
1029
1030lemma le_to_lt_or_eq:
1031  ∀m, n: nat.
1032    m ≤ n → m = n ∨ m < n.
1033  #m #n #le_hyp
1034  cases le_hyp
1035  [1:
1036    @or_introl %
1037  |2:
1038    #m' #le_hyp'
1039    @or_intror
1040    normalize
1041    @le_S_S assumption
1042  ]
1043qed.
1044
1045lemma le_neq_to_lt:
1046  ∀m, n: nat.
1047    m ≤ n → m ≠ n → m < n.
1048  #m #n #le_hyp #neq_hyp
1049  cases neq_hyp
1050  #eq_absurd_hyp
1051  generalize in match (le_to_lt_or_eq m n le_hyp);
1052  #disj_assm cases disj_assm
1053  [1:
1054    #absurd cases (eq_absurd_hyp absurd)
1055  |2:
1056    #assm assumption
1057  ]
1058qed.
1059
1060inverter nat_jmdiscr for nat.
1061
1062lemma plus_lt_to_lt:
1063  ∀m, n, o: nat.
1064    m + n < o → m < o.
1065  #m #n #o
1066  elim n
1067  [1:
1068    <(plus_n_O m) in ⊢ (% → ?);
1069    #assumption assumption
1070  |2:
1071    #n' #inductive_hypothesis
1072    <(plus_n_Sm m n') in ⊢ (% → ?);
1073    #assm @inductive_hypothesis
1074    normalize in assm; normalize
1075    /2 by lt_S_to_lt/
1076  ]
1077qed.
1078
1079include "arithmetics/div_and_mod.ma".
1080
1081lemma n_plus_1_n_to_False:
1082  ∀n: nat.
1083    n + 1 = n → False.
1084  #n elim n
1085  [1:
1086    normalize #absurd destruct(absurd)
1087  |2:
1088    #n' #inductive_hypothesis normalize
1089    #absurd @inductive_hypothesis /2 by injective_S/
1090  ]
1091qed.
1092
1093lemma one_two_times_n_to_False:
1094  ∀n: nat.
1095    1=2*n→False.
1096  #n cases n
1097  [1:
1098    normalize #absurd destruct(absurd)
1099  |2:
1100    #n' normalize #absurd
1101    lapply (injective_S … absurd) -absurd #absurd
1102    /2/
1103  ]
1104qed.
1105
1106let rec odd_p
1107  (n: nat)
1108    on n ≝
1109  match n with
1110  [ O ⇒ False
1111  | S n' ⇒ even_p n'
1112  ]
1113and even_p
1114  (n: nat)
1115    on n ≝
1116  match n with
1117  [ O ⇒ True
1118  | S n' ⇒ odd_p n'
1119  ].
1120
1121let rec n_even_p_to_n_plus_2_even_p
1122  (n: nat)
1123    on n: even_p n → even_p (n + 2) ≝
1124  match n with
1125  [ O ⇒ ?
1126  | S n' ⇒ ?
1127  ]
1128and n_odd_p_to_n_plus_2_odd_p
1129  (n: nat)
1130    on n: odd_p n → odd_p (n + 2) ≝
1131  match n with
1132  [ O ⇒ ?
1133  | S n' ⇒ ?
1134  ].
1135  [1,3:
1136    normalize #assm assumption
1137  |2:
1138    normalize @n_odd_p_to_n_plus_2_odd_p
1139  |4:
1140    normalize @n_even_p_to_n_plus_2_even_p
1141  ]
1142qed.
1143
1144let rec two_times_n_even_p
1145  (n: nat)
1146    on n: even_p (2 * n) ≝
1147  match n with
1148  [ O ⇒ ?
1149  | S n' ⇒ ?
1150  ]
1151and two_times_n_plus_one_odd_p
1152  (n: nat)
1153    on n: odd_p ((2 * n) + 1) ≝
1154  match n with
1155  [ O ⇒ ?
1156  | S n' ⇒ ?
1157  ].
1158  [1,3:
1159    normalize @I
1160  |2:
1161    normalize
1162    >plus_n_Sm
1163    <(associative_plus n' n' 1)
1164    >(plus_n_O (n' + n'))
1165    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1166    [1:
1167      //
1168    |2:
1169      #refl_assm >refl_assm
1170      @two_times_n_plus_one_odd_p     
1171    ]
1172  |4:
1173    normalize
1174    >plus_n_Sm
1175    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1176    [1:
1177      normalize /2/
1178    |2:
1179      #refl_assm >refl_assm
1180      @n_even_p_to_n_plus_2_even_p
1181      @two_times_n_even_p
1182    ]
1183  ]
1184qed.
1185
1186include alias "basics/logic.ma".
1187
1188let rec even_p_to_not_odd_p
1189  (n: nat)
1190    on n: even_p n → ¬ odd_p n ≝
1191  match n with
1192  [ O ⇒ ?
1193  | S n' ⇒ ?
1194  ]
1195and odd_p_to_not_even_p
1196  (n: nat)
1197    on n: odd_p n → ¬ even_p n ≝
1198  match n with
1199  [ O ⇒ ?
1200  | S n' ⇒ ?
1201  ].
1202  [1:
1203    normalize #_
1204    @nmk #assm assumption
1205  |3:
1206    normalize #absurd
1207    cases absurd
1208  |2:
1209    normalize
1210    @odd_p_to_not_even_p
1211  |4:
1212    normalize
1213    @even_p_to_not_odd_p
1214  ]
1215qed.
1216
1217lemma even_p_odd_p_cases:
1218  ∀n: nat.
1219    even_p n ∨ odd_p n.
1220  #n elim n
1221  [1:
1222    normalize @or_introl @I
1223  |2:
1224    #n' #inductive_hypothesis
1225    normalize
1226    cases inductive_hypothesis
1227    #assm
1228    try (@or_introl assumption)
1229    try (@or_intror assumption)
1230  ]
1231qed.
1232
1233lemma two_times_n_plus_one_refl_two_times_n_to_False:
1234  ∀m, n: nat.
1235    2 * m + 1 = 2 * n → False.
1236  #m #n
1237  #assm
1238  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1239  [1:
1240    >assm
1241    @conj
1242    @two_times_n_even_p
1243  |2:
1244    * #_ #absurd
1245    cases (even_p_to_not_odd_p … absurd)
1246    #assm @assm
1247    @two_times_n_plus_one_odd_p
1248  ]
1249qed.
1250
1251lemma not_Some_neq_None_to_False:
1252  ∀a: Type[0].
1253  ∀e: a.
1254    ¬ (Some a e ≠ None a) → False.
1255  #a #e #absurd cases absurd -absurd
1256  #absurd @absurd @nmk -absurd
1257  #absurd destruct(absurd)
1258qed.
1259
1260lemma not_None_to_Some:
1261  ∀A: Type[0].
1262  ∀o: option A.
1263    o ≠ None A → ∃v: A. o = Some A v.
1264  #A #o cases o
1265  [1:
1266    #absurd cases absurd #absurd' cases (absurd' (refl …))
1267  |2:
1268    #v' #ignore /2/
1269  ]
1270qed.
1271
1272lemma inclusive_disjunction_true:
1273  ∀b, c: bool.
1274    (orb b c) = true → b = true ∨ c = true.
1275  # b
1276  # c
1277  elim b
1278  [ normalize
1279    # H
1280    @ or_introl
1281    %
1282  | normalize
1283    /3 by trans_eq, orb_true_l/
1284  ]
1285qed.
1286
1287lemma conjunction_true:
1288  ∀b, c: bool.
1289    andb b c = true → b = true ∧ c = true.
1290  # b
1291  # c
1292  elim b
1293  normalize
1294  [ /2 by conj/
1295  | # K
1296    destruct
1297  ]
1298qed.
1299
1300lemma eq_true_false: false=true → False.
1301 # K
1302 destruct
1303qed.
1304
1305lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
1306 # b
1307 cases b
1308 %
1309qed.
1310
1311(* XXX: to be moved into logic/basics.ma *)
1312lemma and_intro_right:
1313  ∀a, b: Prop.
1314    a → (a → b) → a ∧ b.
1315  #a #b /3/
1316qed.
1317
1318definition bool_to_Prop ≝
1319 λb. match b with [ true ⇒ True | false ⇒ False ].
1320
1321coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
1322
1323lemma bool_as_Prop_to_eq : ∀b : bool. b → b = true.
1324**%
1325qed.
1326
1327(* with this you can use prf : b with b : bool with rewriting
1328   >prf rewrites b as true *)
1329coercion bool_to_Prop_to_eq : ∀b : bool.∀prf : b.b = true
1330 ≝ bool_as_Prop_to_eq on _prf : bool_to_Prop ? to (? = true).
1331
1332lemma andb_Prop : ∀b,d : bool.b → d → b∧d.
1333#b #d #btrue #dtrue >btrue >dtrue %
1334qed.
1335
1336lemma andb_Prop_true : ∀b,d : bool. (b∧d) → And (bool_to_Prop b) (bool_to_Prop d).
1337#b #d #bdtrue elim (andb_true … bdtrue) #btrue #dtrue >btrue >dtrue % %
1338qed.
1339
1340lemma orb_Prop_l : ∀b,d : bool.b → b∨d.
1341#b #d #btrue >btrue %
1342qed.
1343
1344lemma orb_Prop_r : ∀b,d : bool.d → b∨d.
1345#b #d #dtrue >dtrue elim b %
1346qed.
1347
1348lemma orb_Prop_true : ∀b,d : bool. (b∨d) → Or (bool_to_Prop b) (bool_to_Prop d).
1349#b #d #bdtrue elim (orb_true_l … bdtrue) #xtrue >xtrue [%1 | %2] %
1350qed.
1351
1352lemma notb_Prop : ∀b : bool. Not (bool_to_Prop b) → notb b.
1353* * #H [@H % | %]
1354qed.
1355
1356lemma eq_false_to_notb: ∀b. b = false → ¬ b.
1357 *; /2 by eq_true_false, I/
1358qed.
1359
1360lemma not_b_to_eq_false : ∀b : bool. Not (bool_to_Prop b) → b = false.
1361** #H [elim (H ?) % | %]
1362qed.
1363
1364(* with this you can use prf : ¬b with b : bool with rewriting
1365   >prf rewrites b as false *)
1366coercion not_bool_to_Prop_to_eq : ∀b : bool.∀prf : Not (bool_to_Prop b).b = false
1367 ≝ not_b_to_eq_false on _prf : Not (bool_to_Prop ?) to (? = false).
1368
1369
1370lemma true_or_false_Prop : ∀b : bool.Or (bool_to_Prop b) (¬(bool_to_Prop b)).
1371* [%1 % | %2 % *]
1372qed.
1373
1374lemma eq_true_to_b : ∀b. b = true → b.
1375#b #btrue >btrue %
1376qed.
1377
1378definition if_then_else_safe : ∀A : Type[0].∀b : bool.(b → A) → (¬(bool_to_Prop b) → A) → A ≝
1379  λA,b,f,g.
1380  match b return λx.match x with [true ⇒ bool_to_Prop b | false ⇒ ¬bool_to_Prop b] → A with
1381  [ true ⇒ f
1382  | false ⇒ g
1383  ] ?. elim b % *
1384qed.
1385
1386notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
1387  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ${ident prf2}.$g)}.
1388notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
1389  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
1390notation > "'If' b 'then' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
1391  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}.$g)}.
1392notation > "'If' b 'then' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
1393  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}:$ty2.$g)}.
1394notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' g" with precedence 46 for
1395  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ_.$g)}.
1396notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' g" with precedence 46 for
1397  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_.$g)}.
1398
1399notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
1400  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
1401notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
1402  @{'if_then_else_safe $b (λ_:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
1403notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break g)" with precedence 46 for
1404  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_:$ty2.$g)}.
1405 
1406interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
1407
1408(* Also extracts an equality proof (useful when not using Russell). *)
1409notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
1410 with precedence 10
1411for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
1412        λ${ident E}.$s ] (refl ? $t) }.
1413
1414notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
1415 with precedence 10
1416for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
1417        λ${ident E}.$s ] (refl ? $t) }.
1418
1419notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
1420 with precedence 10
1421for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
1422       match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
1423        λ${ident E}.$s ] ] (refl ? $t) }.
1424
1425notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
1426 with precedence 10
1427for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
1428       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
1429        λ${ident E}.$s ] ] (refl ? $t) }.
1430
1431lemma length_append:
1432 ∀A.∀l1,l2:list A.
1433  |l1 @ l2| = |l1| + |l2|.
1434 #A #l1 elim l1
1435  [ //
1436  | #hd #tl #IH #l2 normalize <IH //]
1437qed.
1438
1439lemma nth_cons:
1440  ∀n,A,h,t,y.
1441  nth (S n) A (h::t) y = nth n A t y.
1442 #n #A #h #t #y /2 by refl/
1443qed.
1444
1445lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1446 #A #a #b #EQ destruct //
1447qed.
1448
1449lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
1450  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
1451 #A #P #s1 #s2 / by /
1452qed.
1453
1454lemma Some_eq:
1455 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
1456 #T #x #y #H @option_destruct_Some @H
1457qed.
1458
1459lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?.
1460#A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS')
1461qed.
1462
1463coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
1464  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
Note: See TracBrowser for help on using the repository browser.