matita/matita/contribs/procedural/Coq/IntMap/Adist.mma

   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 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i          $Id: Adist.v,v 1.9.2.1 2004/07/16 19:31:04 herbelin Exp $        i*)
  34
  35 include "Bool/Bool.ma".
  36
  37 include "ZArith/ZArith.ma".
  38
  39 include "Arith/Arith.ma".
  40
  41 include "Arith/Min.ma".
  42
  43 include "IntMap/Addr.ma".
  44
  45 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_1.con" as definition.
  46
  47 inline procedural "cic:/Coq/IntMap/Adist/natinf.ind".
  48
  49 inline procedural "cic:/Coq/IntMap/Adist/ad_plength.con" as definition.
  50
  51 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_infty.con" as lemma.
  52
  53 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_zeros.con" as lemma.
  54
  55 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_one.con" as lemma.
  56
  57 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_first_one.con" as lemma.
  58
  59 inline procedural "cic:/Coq/IntMap/Adist/ni_min.con" as definition.
  60
  61 inline procedural "cic:/Coq/IntMap/Adist/ni_min_idemp.con" as lemma.
  62
  63 inline procedural "cic:/Coq/IntMap/Adist/ni_min_comm.con" as lemma.
  64
  65 inline procedural "cic:/Coq/IntMap/Adist/ni_min_assoc.con" as lemma.
  66
  67 inline procedural "cic:/Coq/IntMap/Adist/ni_min_O_l.con" as lemma.
  68
  69 inline procedural "cic:/Coq/IntMap/Adist/ni_min_O_r.con" as lemma.
  70
  71 inline procedural "cic:/Coq/IntMap/Adist/ni_min_inf_l.con" as lemma.
  72
  73 inline procedural "cic:/Coq/IntMap/Adist/ni_min_inf_r.con" as lemma.
  74
  75 inline procedural "cic:/Coq/IntMap/Adist/ni_le.con" as definition.
  76
  77 inline procedural "cic:/Coq/IntMap/Adist/ni_le_refl.con" as lemma.
  78
  79 inline procedural "cic:/Coq/IntMap/Adist/ni_le_antisym.con" as lemma.
  80
  81 inline procedural "cic:/Coq/IntMap/Adist/ni_le_trans.con" as lemma.
  82
  83 inline procedural "cic:/Coq/IntMap/Adist/ni_le_min_1.con" as lemma.
  84
  85 inline procedural "cic:/Coq/IntMap/Adist/ni_le_min_2.con" as lemma.
  86
  87 inline procedural "cic:/Coq/IntMap/Adist/ni_min_case.con" as lemma.
  88
  89 inline procedural "cic:/Coq/IntMap/Adist/ni_le_total.con" as lemma.
  90
  91 inline procedural "cic:/Coq/IntMap/Adist/ni_le_min_induc.con" as lemma.
  92
  93 inline procedural "cic:/Coq/IntMap/Adist/le_ni_le.con" as lemma.
  94
  95 inline procedural "cic:/Coq/IntMap/Adist/ni_le_le.con" as lemma.
  96
  97 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_lb.con" as lemma.
  98
  99 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_ub.con" as lemma.
 100
 101 (*#* We define an ultrametric distance between addresses:
 102     $d(a,a')=1/2^pd(a,a')$,
 103     where $pd(a,a')$ is the number of identical bits at the beginning
 104     of $a$ and $a'$ (infinity if $a=a'$).
 105     Instead of working with $d$, we work with $pd$, namely
 106     [ad_pdist]: *)
 107
 108 inline procedural "cic:/Coq/IntMap/Adist/ad_pdist.con" as definition.
 109
 110 (*#* d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that
 111     $pd(a,a')=infty$ iff $a=a'$: *)
 112
 113 inline procedural "cic:/Coq/IntMap/Adist/ad_pdist_eq_1.con" as lemma.
 114
 115 inline procedural "cic:/Coq/IntMap/Adist/ad_pdist_eq_2.con" as lemma.
 116
 117 (*#* $d$ is a distance, so $d(a,a')=d(a',a)$: *)
 118
 119 inline procedural "cic:/Coq/IntMap/Adist/ad_pdist_comm.con" as lemma.
 120
 121 (*#* $d$ is an ultrametric distance, that is, not only $d(a,a')\leq
 122     d(a,a'')+d(a'',a')$,
 123   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
 124   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
 125   This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{ad\_plength}}(a))$
 126   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
 127   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
 128   min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq
 129   \texttt{ad\_plength} (a~\texttt{xor}~ b)$
 130   (lemma [ad_plength_ultra]).
 131 *)
 132
 133 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_ultra_1.con" as lemma.
 134
 135 inline procedural "cic:/Coq/IntMap/Adist/ad_plength_ultra.con" as lemma.
 136
 137 inline procedural "cic:/Coq/IntMap/Adist/ad_pdist_ultra.con" as lemma.
 138