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

2 | |
---|

3 | lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). |
---|

4 | #A #P #l elim l |
---|

5 | [ // |
---|

6 | | #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // |
---|

7 | ] qed. |
---|

8 | |
---|

9 | (* An alternative form of All that can be easier to use sometimes. *) |
---|

10 | lemma All_alt : ∀A,P,l. |
---|

11 | (∀a,pre,post. l = pre@a::post → P a) → |
---|

12 | All A P l. |
---|

13 | #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); |
---|

14 | generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); |
---|

15 | [ #pre #E % |
---|

16 | | #a #tl #IH #pre #E % |
---|

17 | [ @(H a pre tl E) |
---|

18 | | @(IH (pre@[a])) >associative_append @E |
---|

19 | ] |
---|

20 | ] qed. |
---|

21 | |
---|

22 | let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ |
---|

23 | match la with |
---|

24 | [ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ] |
---|

25 | | cons ha ta ⇒ |
---|

26 | match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ] |
---|

27 | ]. |
---|

28 | |
---|

29 | lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|. |
---|

30 | #A #B #P #la elim la |
---|

31 | [ * [ // | #x #y * ] |
---|

32 | | #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl |
---|

33 | ] qed. |
---|

34 | |
---|

35 | lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb. |
---|

36 | #A #B #P #Q #la elim la |
---|

37 | [ * [ // | #h #t #_ * ] |
---|

38 | | #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ] |
---|

39 | ] qed. |
---|

40 | |
---|

41 | let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝ |
---|

42 | match l return λl. All A P l → ? with |
---|

43 | [ nil ⇒ λ_. nil B |
---|

44 | | cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) |
---|

45 | ] H. |
---|

46 | |
---|