Ignore:
Timestamp:
Aug 4, 2011, 1:55:53 PM (9 years ago)
Author:
campbell
Message:

Tidy up branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1087 r1102  
    4040] qed.
    4141
     42lemma 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
     52lemma 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
     59lemma 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 ]
     63qed.
     64
     65lemma 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
     71lemma Exists_map : ∀A,B,P,Q,f,l.
     72Exists A P l →
     73(∀a.P a → Q (f a)) →
     74Exists 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
    4278lemma map_append : ∀A,B,f,l1,l2.
    4379  (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.