Changeset 1092 for src/utilities


Ignore:
Timestamp:
Jul 28, 2011, 12:14:37 PM (9 years ago)
Author:
campbell
Message:

Some minor definitions for identifiers and lists.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r816 r1092  
    99let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
    1010match l with
    11 [ nil ⇒ False
     11[ nil ⇒ True
    1212| cons h t ⇒ P h ∧ All A P t
    1313].
     14
     15lemma 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/
     18qed.
    1419
    1520let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     
    1823| cons h t ⇒ orb (p h) (exists A p t)
    1924].
     25
     26let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
     27match l with
     28[ nil ⇒ False
     29| cons h t ⇒ (P h) ∨ (Exists A P t)
     30].
     31
     32lemma 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
     42lemma 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.