Line | |
---|

1 | include "basics/list.ma". |
---|

2 | |
---|

3 | let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝ |
---|

4 | match l with |
---|

5 | [ nil ⇒ None ? |
---|

6 | | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ] |
---|

7 | ]. |
---|

8 | |
---|

9 | let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
---|

10 | match l with |
---|

11 | [ nil ⇒ True |
---|

12 | | cons h t ⇒ P h ∧ All A P t |
---|

13 | ]. |
---|

14 | |
---|

15 | lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l. |
---|

16 | #A #P #Q #H #l elim l normalize // |
---|

17 | #h #t #IH * /3/ |
---|

18 | qed. |
---|

19 | |
---|

20 | let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ |
---|

21 | match l with |
---|

22 | [ nil ⇒ false |
---|

23 | | cons h t ⇒ orb (p h) (exists A p t) |
---|

24 | ]. |
---|

25 | |
---|

26 | let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
---|

27 | match l with |
---|

28 | [ nil ⇒ False |
---|

29 | | cons h t ⇒ (P h) ∨ (Exists A P t) |
---|

30 | ]. |
---|

31 | |
---|

32 | lemma Exists_append : ∀A,P,l1,l2. |
---|

33 | Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2. |
---|

34 | #A #P #l1 elim l1 |
---|

35 | [ normalize /2/ |
---|

36 | | #h #t #IH #l2 * |
---|

37 | [ #H /3/ |
---|

38 | | #H cases (IH l2 H) /3/ |
---|

39 | ] |
---|

40 | ] qed. |
---|

41 | |
---|

42 | lemma map_append : ∀A,B,f,l1,l2. |
---|

43 | (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). |
---|

44 | #A #B #f #l1 elim l1 |
---|

45 | [ #l2 @refl |
---|

46 | | #h #t #IH #l2 normalize // |
---|

47 | ] qed. |
---|

48 | |
---|

49 | let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝ |
---|

50 | match l with |
---|

51 | [ nil ⇒ None B |
---|

52 | | cons h t ⇒ |
---|

53 | match f h with |
---|

54 | [ None ⇒ find A B f t |
---|

55 | | Some b ⇒ Some B b |
---|

56 | ] |
---|

57 | ]. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.