Changeset 3050 for src/utilities
 Timestamp:
 Apr 1, 2013, 5:18:05 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/listb_extra.ma
r2728 r3050 1 1 include "basics/lists/listb.ma". 2 2 include "ASM/Util.ma". 3 include "utilities/lists.ma". 3 4 4 5 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. … … 17 18 ] qed. 18 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.
Note: See TracChangeset
for help on using the changeset viewer.