Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (9 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/utilities/lists.ma

    r1195 r1316  
    1717#h #t #IH * /3/
    1818qed.
     19
     20lemma All_nth : ∀A,P,n,l.
     21  All A P l →
     22  ∀a.
     23  nth_opt A n l = Some A a →
     24  P a.
     25#A #P #n elim n
     26[ * [ #_ #a #E whd in E:(??%?); destruct
     27    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
     28    ]
     29| #m #IH *
     30  [ #_ #a #E whd in E:(??%?); destruct
     31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
     32  ]
     33] qed.
    1934
    2035let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     
    4055] qed.
    4156
     57lemma Exists_append_l : ∀A,P,l1,l2.
     58  Exists A P l1 → Exists A P (l1@l2).
     59#A #P #l1 #l2 elim l1
     60[ *
     61| #h #t #IH *
     62  [ #H %1 @H
     63  | #H %2 @IH @H
     64  ]
     65] qed.
     66
     67lemma Exists_append_r : ∀A,P,l1,l2.
     68  Exists A P l2 → Exists A P (l1@l2).
     69#A #P #l1 #l2 elim l1
     70[ #H @H
     71| #h #t #IH #H %2 @IH @H
     72] qed.
     73
     74lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
     75#A #P #l1 #x #l2 elim l1
     76[ normalize #H %2 @H
     77| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
     78qed.
     79
     80lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
     81#A #P #l1 #x #l2 #H elim l1
     82[ %1 @H
     83| #h #t #IH %2 @IH
     84] qed.
     85
     86lemma Exists_map : ∀A,B,P,Q,f,l.
     87Exists A P l →
     88(∀a.P a → Q (f a)) →
     89Exists B Q (map A B f l).
     90#A #B #P #Q #f #l elim l //
     91#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
     92
    4293lemma map_append : ∀A,B,f,l1,l2.
    4394  (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.