Changeset 1351 for src/utilities


Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (9 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/deppair.ma

    r1316 r1351  
     1(* TODO: merge with utilities/sigma.ma *)
     2
    13include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *)
    24
     
    79#A #P * #a #p @p
    810qed.
     11
     12lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x.
     13#A #P #P' #H1 * #x #H2 @H1 @H2
     14qed.
  • src/utilities/lists.ma

    r1316 r1351  
    9191#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
    9292
     93lemma Exists_exists : ∀A,P,l.
     94  Exists A P l →
     95  ∃x. P x.
     96#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
     97qed.
     98
     99lemma Exists_All : ∀A,P,Q,l.
     100  Exists A P l →
     101  All A Q l →
     102  ∃x. P x ∧ Q x.
     103#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
     104qed.
     105
    93106lemma map_append : ∀A,B,f,l1,l2.
    94107  (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.