matita/contribs/CoRN-Decl/reals/RealLists.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/reals/RealLists".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
  22
  23 include "reals/CReals1.ma".
  24
  25 (* UNEXPORTED
  26 Section Lists
  27 *)
  28
  29 (*#* * Lists of Real Numbers
  30
  31 In some contexts we will need to work with nested existential quantified formulas of the form $\exists_{n\in\NN}\exists_{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$#exists n exists x1,...,xn P(x1,..,xn)#.  One way of formalizing this kind of statement is through quantifying over lists.  In this file we provide some tools for manipulating lists.
  32
  33 Notice that some of the properties listed below only make sense in the context within which we are working.  Unlike in the other lemma files, no care has been taken here to state the lemmas in their most general form, as that would make them very unpractical to use.
  34
  35 %\bigskip%
  36
  37 We start by defining maximum and minimum of lists of reals and two membership predicates. The value of these functions for the empty list is arbitrarily set to 0, but it will be irrelevant, as we will never work with empty lists.
  38 *)
  39
  40 inline "cic:/CoRN/reals/RealLists/maxlist.con".
  41
  42 inline "cic:/CoRN/reals/RealLists/minlist.con".
  43
  44 inline "cic:/CoRN/reals/RealLists/member.con".
  45
  46 (*#*
  47 Sometimes the length of the list has to be restricted; the next definition provides an easy way to do that. *)
  48
  49 inline "cic:/CoRN/reals/RealLists/length_leEq.con".
  50
  51 (*#* Length is preserved by mapping. *)
  52
  53 (* UNEXPORTED
  54 Implicit Arguments map [A B].
  55 *)
  56
  57 inline "cic:/CoRN/reals/RealLists/map_pres_length.con".
  58
  59 (*#*
  60 Often we want to map partial functions through a list; this next operator provides a way to do that, and is proved to be correct. *)
  61
  62 (* UNEXPORTED
  63 Implicit Arguments cons [A].
  64 *)
  65
  66 inline "cic:/CoRN/reals/RealLists/map2.con".
  67
  68 inline "cic:/CoRN/reals/RealLists/map2_wd.con".
  69
  70 inline "cic:/CoRN/reals/RealLists/map2_pres_member.con".
  71
  72 (*#*
  73 As [maxlist] and [minlist] are generalizations of [Max] and [Min] to finite sets of real numbers, they have the expected properties: *)
  74
  75 inline "cic:/CoRN/reals/RealLists/maxlist_greater.con".
  76
  77 (* begin hide *)
  78
  79 inline "cic:/CoRN/reals/RealLists/Lists/maxlist_aux.con" "Lists__".
  80
  81 (* end hide *)
  82
  83 inline "cic:/CoRN/reals/RealLists/maxlist_leEq_eps.con".
  84
  85 inline "cic:/CoRN/reals/RealLists/maxlist_less.con".
  86
  87 inline "cic:/CoRN/reals/RealLists/maxlist_leEq.con".
  88
  89 inline "cic:/CoRN/reals/RealLists/minlist_smaller.con".
  90
  91 (* begin hide *)
  92
  93 inline "cic:/CoRN/reals/RealLists/Lists/minlist_aux.con" "Lists__".
  94
  95 (* end hide *)
  96
  97 inline "cic:/CoRN/reals/RealLists/minlist_leEq_eps.con".
  98
  99 inline "cic:/CoRN/reals/RealLists/less_minlist.con".
 100
 101 inline "cic:/CoRN/reals/RealLists/leEq_minlist.con".
 102
 103 (* UNEXPORTED
 104 End Lists
 105 *)
 106