]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/Coq/IntMap/Adist.mma
update in ground_2, static_2, basic_2
[helm.git] / 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