Changeset 1087 for Deliverables/D3.3/idlookupbranch/utilities/lists.ma
 Timestamp:
 Jul 25, 2011, 2:58:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/utilities/lists.ma
r816 r1087 9 9 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ 10 10 match l with 11 [ nil ⇒ False11 [ nil ⇒ True 12 12  cons h t ⇒ P h ∧ All A P t 13 13 ]. 14 15 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l. 16 #A #P #Q #H #l elim l normalize // 17 #h #t #IH * /3/ 18 qed. 14 19 15 20 let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ … … 18 23  cons h t ⇒ orb (p h) (exists A p t) 19 24 ]. 25 26 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ 27 match l with 28 [ nil ⇒ False 29  cons h t ⇒ (P h) ∨ (Exists A P t) 30 ]. 31 32 lemma Exists_append : ∀A,P,l1,l2. 33 Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2. 34 #A #P #l1 elim l1 35 [ normalize /2/ 36  #h #t #IH #l2 * 37 [ #H /3/ 38  #H cases (IH l2 H) /3/ 39 ] 40 ] qed. 41 42 lemma map_append : ∀A,B,f,l1,l2. 43 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). 44 #A #B #f #l1 elim l1 45 [ #l2 @refl 46  #h #t #IH #l2 normalize // 47 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.