include "basics/lists/listb.ma". include "ASM/Util.ma". include "utilities/lists.ma". lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. Exists S (λy. y = x) l → x ∈ l. #S #x #l elim l [ // | #h #t #IH normalize lapply (eqb_true … x h) cases (x==h) * [ #E #_ >(E (refl ??)) // | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct | #H @IH @H ] ] ] qed. lemma nth_opt_Exists : ∀A,n,l,a. nth_opt A n l = Some A a → Exists A (λa'. a' = a) l. #A #n elim n [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ] | #m #IH * [ #a #E normalize in E; destruct | #a #l #a' #E %2 @IH @E ] ] qed. lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → decidable (In A l a). #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC) [ #H % %2 assumption | * #H cases (DEC hd) [ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]] qed. lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l. #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption] % #H1 @H % >H1 % qed. lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a. #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % * [ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption] qed. lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A. All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2. #A #P #l1 elim l1 [ #l2 change with l2 in ⊢ (???% → ?); #H % //] #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?); * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % // qed.