← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/micromega/VarMap.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/micromega/VarMap.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(*                                                                      *)
 
9
(* Micromega: A reflexive tactic using the Positivstellensatz           *)
 
10
(*                                                                      *)
 
11
(*  Fr�d�ric Besson (Irisa/Inria) 2006-2008                             *)
 
12
(*                                                                      *)
 
13
(************************************************************************)
 
14
 
 
15
Require Import ZArith.
 
16
Require Import Coq.Arith.Max.
 
17
Require Import List.
 
18
Set Implicit Arguments.
 
19
 
 
20
(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v) 
 
21
   -- this is harmless and spares a lot of Empty.
 
22
   This means smaller proof-terms. 
 
23
   BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
 
24
*)
 
25
 
 
26
Section MakeVarMap.
 
27
  Variable A : Type.
 
28
  Variable default : A.
 
29
  
 
30
  Inductive t  : Type :=
 
31
  | Empty : t 
 
32
  | Leaf : A -> t 
 
33
  | Node : t  -> A -> t  -> t .
 
34
  
 
35
  Fixpoint find   (vm : t ) (p:positive) {struct vm} : A :=
 
36
    match vm with
 
37
      | Empty => default
 
38
      | Leaf i => i
 
39
      | Node l e r => match p with
 
40
                        | xH => e
 
41
                        | xO p => find l p
 
42
                        | xI p => find r p
 
43
                      end
 
44
    end.
 
45
 
 
46
 (* an off_map (a map with offset) offers the same functionalites  as /contrib/setoid_ring/BinList.v - it is used in EnvRing.v *)
 
47
(*
 
48
  Definition off_map  :=  (option positive *t )%type.
 
49
 
 
50
 
 
51
 
 
52
  Definition jump  (j:positive) (l:off_map ) := 
 
53
    let (o,m) := l in
 
54
      match o with
 
55
        | None => (Some j,m)
 
56
        | Some j0 => (Some (j+j0)%positive,m)
 
57
      end.
 
58
 
 
59
  Definition nth  (n:positive) (l: off_map ) :=
 
60
    let (o,m) := l in
 
61
      let idx  := match o with
 
62
                    | None => n
 
63
                    | Some i => i + n
 
64
                  end%positive in
 
65
      find  idx m.
 
66
 
 
67
 
 
68
  Definition hd  (l:off_map) := nth  xH l.
 
69
 
 
70
 
 
71
  Definition tail (l:off_map ) := jump xH l.
 
72
 
 
73
 
 
74
  Lemma psucc : forall p,  (match p with
 
75
                              | xI y' => xO (Psucc y')
 
76
                              | xO y' => xI y'
 
77
                              | 1%positive => 2%positive 
 
78
                            end) = (p+1)%positive.
 
79
  Proof.
 
80
    destruct p.
 
81
    auto with zarith.
 
82
    rewrite xI_succ_xO.
 
83
    auto with zarith.
 
84
    reflexivity.
 
85
  Qed.
 
86
 
 
87
  Lemma jump_Pplus : forall i j l, 
 
88
    (jump (i + j) l) = (jump i (jump j l)).
 
89
  Proof.
 
90
    unfold jump.
 
91
    destruct l.
 
92
    destruct o.
 
93
    rewrite Pplus_assoc.
 
94
    reflexivity.
 
95
    reflexivity.
 
96
  Qed.
 
97
 
 
98
  Lemma jump_simpl : forall p l,
 
99
    jump p l = 
 
100
    match p with
 
101
      | xH => tail l
 
102
      | xO p => jump p (jump p l)
 
103
      | xI p  => jump p (jump p (tail l))
 
104
    end.
 
105
  Proof.
 
106
    destruct p ; unfold tail ; intros ;  repeat rewrite <- jump_Pplus.
 
107
    (* xI p = p + p + 1 *)
 
108
    rewrite xI_succ_xO.
 
109
    rewrite Pplus_diag.
 
110
    rewrite <- Pplus_one_succ_r.
 
111
    reflexivity.
 
112
    (* xO p = p + p *)
 
113
    rewrite Pplus_diag.
 
114
    reflexivity.
 
115
    reflexivity.
 
116
  Qed.
 
117
 
 
118
  Ltac jump_s :=
 
119
    repeat 
 
120
      match goal with
 
121
        | |- context [jump xH ?e] => rewrite (jump_simpl xH)
 
122
        | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
 
123
        | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
 
124
      end.
 
125
    
 
126
  Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
 
127
  Proof. 
 
128
    unfold tail.
 
129
    intros.
 
130
    repeat rewrite <- jump_Pplus.
 
131
    rewrite Pplus_comm.
 
132
    reflexivity.
 
133
  Qed.
 
134
 
 
135
  Lemma jump_Psucc : forall j l, 
 
136
    (jump (Psucc j) l) = (jump 1 (jump j l)).
 
137
  Proof.
 
138
    intros.
 
139
    rewrite <- jump_Pplus.
 
140
    rewrite Pplus_one_succ_r.
 
141
    rewrite Pplus_comm.
 
142
    reflexivity.
 
143
  Qed.
 
144
 
 
145
  Lemma jump_Pdouble_minus_one : forall i l,
 
146
    (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)).
 
147
  Proof.
 
148
    unfold tail.
 
149
    intros.
 
150
    repeat rewrite <- jump_Pplus.
 
151
    rewrite <- Pplus_one_succ_r.
 
152
    rewrite Psucc_o_double_minus_one_eq_xO.
 
153
    rewrite Pplus_diag.
 
154
    reflexivity.
 
155
  Qed.
 
156
 
 
157
  Lemma jump_x0_tail : forall p l, jump (xO p) (tail l) = jump (xI p) l.
 
158
  Proof.
 
159
    intros.
 
160
    jump_s.
 
161
    repeat rewrite <- jump_Pplus.
 
162
    reflexivity.
 
163
  Qed.
 
164
 
 
165
  
 
166
  Lemma nth_spec : forall p l, 
 
167
    nth p l = 
 
168
    match p with
 
169
      | xH => hd  l
 
170
      | xO p => nth p (jump p l)
 
171
      | xI p => nth p (jump p (tail l))
 
172
    end. 
 
173
  Proof.
 
174
    unfold nth.
 
175
    destruct l.
 
176
    destruct o.
 
177
    simpl.
 
178
    rewrite psucc.
 
179
    destruct p.
 
180
    replace (p0 + xI p)%positive with ((p + (p0 + 1) + p))%positive.
 
181
    reflexivity.
 
182
    rewrite xI_succ_xO.
 
183
    rewrite Pplus_one_succ_r.
 
184
    rewrite <- Pplus_diag.
 
185
    rewrite Pplus_comm.
 
186
    symmetry.
 
187
    rewrite (Pplus_comm p0).
 
188
    rewrite <- Pplus_assoc.
 
189
    rewrite (Pplus_comm 1)%positive.
 
190
    rewrite <- Pplus_assoc.
 
191
    reflexivity.
 
192
  (**)
 
193
    replace ((p0 + xO p))%positive with (p + p0 + p)%positive.
 
194
    reflexivity.
 
195
    rewrite <- Pplus_diag.
 
196
    rewrite <- Pplus_assoc.
 
197
    rewrite Pplus_comm.
 
198
    rewrite Pplus_assoc.
 
199
    reflexivity.
 
200
    reflexivity.
 
201
    simpl.
 
202
    destruct p.
 
203
    rewrite xI_succ_xO.
 
204
    rewrite Pplus_one_succ_r.
 
205
    rewrite <- Pplus_diag.
 
206
    symmetry.
 
207
    rewrite Pplus_comm.
 
208
    rewrite Pplus_assoc.
 
209
    reflexivity.
 
210
    rewrite Pplus_diag.
 
211
    reflexivity.
 
212
    reflexivity.
 
213
  Qed.
 
214
 
 
215
 
 
216
  Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l).
 
217
  Proof.
 
218
    destruct l.
 
219
    unfold tail.
 
220
    unfold hd.
 
221
    unfold jump.
 
222
    unfold nth.
 
223
    destruct o.
 
224
    symmetry.
 
225
    rewrite Pplus_comm.
 
226
    rewrite <- Pplus_assoc.
 
227
    rewrite (Pplus_comm p0).
 
228
    reflexivity.
 
229
    rewrite Pplus_comm.
 
230
    reflexivity.
 
231
  Qed.
 
232
 
 
233
  Lemma nth_Pdouble_minus_one :
 
234
    forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
 
235
  Proof.
 
236
    destruct l.
 
237
    unfold tail.
 
238
    unfold nth, jump.
 
239
    destruct o.
 
240
    rewrite ((Pplus_comm p)).
 
241
    rewrite <- (Pplus_assoc p0).
 
242
    rewrite Pplus_diag.
 
243
    rewrite <- Psucc_o_double_minus_one_eq_xO.
 
244
    rewrite Pplus_one_succ_r.
 
245
    rewrite (Pplus_comm (Pdouble_minus_one p)).
 
246
    rewrite Pplus_assoc.
 
247
    rewrite (Pplus_comm p0).
 
248
    reflexivity.
 
249
    rewrite <- Pplus_one_succ_l.
 
250
    rewrite Psucc_o_double_minus_one_eq_xO.
 
251
    rewrite Pplus_diag.
 
252
    reflexivity.
 
253
  Qed.
 
254
 
 
255
*)
 
256
 
 
257
End MakeVarMap.
 
258