source: src/utilities/listb_extra.ma @ 3155

Last change on this file since 3155 was 3050, checked in by piccolo, 7 years ago

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File size: 1.7 KB
Line 
1include "basics/lists/listb.ma".
2include "ASM/Util.ma".
3include "utilities/lists.ma".
4
5lemma 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
21lemma 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
33lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
34decidable (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]]
38qed.
39
40lemma 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 %
43qed.
44
45lemma 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]
48qed.
49
50lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
51All ? 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 % //
56qed.
Note: See TracBrowser for help on using the repository browser.