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

2 | include "ASM/Util.ma". |
---|

3 | include "utilities/lists.ma". |
---|

4 | |
---|

5 | lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. |
---|

6 | Exists S (λy. y = x) l → |
---|

7 | x ∈ l. |
---|

8 | #S #x #l elim l |
---|

9 | [ // |
---|

10 | | #h #t #IH |
---|

11 | normalize lapply (eqb_true … x h) |
---|

12 | cases (x==h) * |
---|

13 | [ #E #_ >(E (refl ??)) // |
---|

14 | | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct |
---|

15 | | #H @IH @H |
---|

16 | ] |
---|

17 | ] |
---|

18 | ] qed. |
---|

19 | |
---|

20 | |
---|

21 | lemma nth_opt_Exists : ∀A,n,l,a. |
---|

22 | nth_opt A n l = Some A a → |
---|

23 | Exists A (λa'. a' = a) l. |
---|

24 | #A #n elim n |
---|

25 | [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ] |
---|

26 | | #m #IH * |
---|

27 | [ #a #E normalize in E; destruct |
---|

28 | | #a #l #a' #E %2 @IH @E |
---|

29 | ] |
---|

30 | ] qed. |
---|

31 | |
---|

32 | |
---|

33 | lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → |
---|

34 | decidable (In A l a). |
---|

35 | #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC) |
---|

36 | [ #H % %2 assumption | * #H cases (DEC hd) |
---|

37 | [ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]] |
---|

38 | qed. |
---|

39 | |
---|

40 | lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l. |
---|

41 | #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption] |
---|

42 | % #H1 @H % >H1 % |
---|

43 | qed. |
---|

44 | |
---|

45 | lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a. |
---|

46 | #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % * |
---|

47 | [ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption] |
---|

48 | qed. |
---|

49 | |
---|

50 | lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A. |
---|

51 | All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2. |
---|

52 | #A #P #l1 elim l1 |
---|

53 | [ #l2 change with l2 in ⊢ (???% → ?); #H % //] |
---|

54 | #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?); |
---|

55 | * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % // |
---|

56 | qed. |
---|