Last change
on this file since 1087 was
1087,
checked in by campbell, 9 years ago

Experimental branch where lookups of local variables in Cminor code always
succeed.

File size:
1.1 KB

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. 

Note: See
TracBrowser
for help on using the repository browser.