Changeset 1102 for Deliverables/D3.3/idlookupbranch/utilities/lists.ma
 Timestamp:
 Aug 4, 2011, 1:55:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/utilities/lists.ma
r1087 r1102 40 40 ] qed. 41 41 42 lemma Exists_append_l : ∀A,P,l1,l2. 43 Exists A P l1 → Exists A P (l1@l2). 44 #A #P #l1 #l2 elim l1 45 [ * 46  #h #t #IH * 47 [ #H %1 @H 48  #H %2 @IH @H 49 ] 50 ] qed. 51 52 lemma Exists_append_r : ∀A,P,l1,l2. 53 Exists A P l2 → Exists A P (l1@l2). 54 #A #P #l1 #l2 elim l1 55 [ #H @H 56  #h #t #IH #H %2 @IH @H 57 ] qed. 58 59 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2). 60 #A #P #l1 #x #l2 elim l1 61 [ normalize #H %2 @H 62  #h #t #IH normalize * [ #H %1 @H  #H %2 @IH @H ] 63 qed. 64 65 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2). 66 #A #P #l1 #x #l2 #H elim l1 67 [ %1 @H 68  #h #t #IH %2 @IH 69 ] qed. 70 71 lemma Exists_map : ∀A,B,P,Q,f,l. 72 Exists A P l → 73 (∀a.P a → Q (f a)) → 74 Exists B Q (map A B f l). 75 #A #B #P #Q #f #l elim l // 76 #h #t #IH * [ #H #F %1 @F @H  #H #F %2 @IH [ @H  @F ] ] qed. 77 42 78 lemma map_append : ∀A,B,f,l1,l2. 43 79 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
Note: See TracChangeset
for help on using the changeset viewer.