BoundedN.v 7.9 KB
Newer Older
1
2
(* This file formalizes a bounded natural number type which is
efficient to compute with. *)
3
4
5
6
7
8
9
10
11
12
13
14
15
From Coq Require Import NArith ZArith.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Finite.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From Coq Require Import Eqdep_dec.
From Coq Require Import List.
From Coq Require Import Psatz.
From stdpp Require countable.
Import ListNotations.

Local Open Scope N.

16
17
18
19
20
21
(* The shape of the proof is carefully chosen so that we have unicity
of identity proofs. This is similar to CompCert's formalization of
machine integers. Additionally, we choose to put bound first in the
comparison so that Coq does not partially reduce the comparison, which
results in a term with a match containing 'bound' cases. This was
suggested as a solution by Gaëtan Gilbert in Gitter. *)
22
Inductive BoundedN (bound : N) :=
23
  bounded (n : N) (_ : (bound ?= n) = Gt).
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

Arguments bounded {_}.

Module BoundedN.
  Definition to_N {bound : N} (n : BoundedN bound) : N :=
    let (val, _) := n in val.

  Definition eqb {bound : N} (a b : BoundedN bound) : bool :=
    N.eqb (to_N a) (to_N b).

  Definition of_N_compare {bound : N} (n : N) : option ((bound ?= n) = Gt) :=
    match bound ?= n as comp return (option (comp = Gt)) with
    | Gt => Some eq_refl
    | _ => None
    end.

  Definition of_N {bound : N} (n : N) : option (BoundedN bound) :=
    match of_N_compare n with
    | Some prf => Some (bounded n prf)
    | None => None
    end.

  Definition to_nat {bound : N} (n : BoundedN bound) : nat :=
    N.to_nat (to_N n).

  Definition of_nat {bound : N} (n : nat) : option (BoundedN bound) :=
    of_N (N.of_nat n).

  Definition to_Z {bound : N} (n : BoundedN bound) : Z :=
    Z.of_N (to_N n).

  Definition of_Z {bound : N} (z : Z) : option (BoundedN bound) :=
    if (z <? 0)%Z then None else of_N (Z.to_N z).

  Definition of_Z_const (bound : N) (z : Z) :=
    let ofz := @of_Z bound z in
    match ofz return (match ofz with
                      | Some _ => BoundedN bound
                      | None => unit
                      end) with
    | Some x => x
    | None => tt
    end.

  Lemma to_N_inj {bound : N} {a b : BoundedN bound} :
    to_N a = to_N b -> a = b.
  Proof.
    intros eq.
    destruct a, b.
    simpl in *.
    subst.
    f_equal.
    apply UIP_dec.
    decide equality.
  Qed.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
80
  Hint Resolve to_N_inj : core.
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197

  Lemma eqb_spec {bound : N} (a b : BoundedN bound) :
    Bool.reflect (a = b) (eqb a b).
  Proof.
    unfold eqb.
    destruct (N.eqb_spec (to_N a) (to_N b)) as [eq | neq].
    - constructor.
      auto.
    - constructor.
      intros H; rewrite H in neq; tauto.
  Qed.

  Lemma eqb_refl {bound : N} (n : BoundedN bound) :
    eqb n n = true.
  Proof. destruct (eqb_spec n n); tauto. Qed.

  Lemma to_nat_inj {bound : N} (a b : BoundedN bound) :
    to_nat a = to_nat b -> a = b.
  Proof.
    intros eq.
    apply to_N_inj.
    unfold to_nat in eq.
    now apply N2Nat.inj.
  Qed.

  Lemma to_Z_inj {bound : N} (a b : BoundedN bound) :
    to_Z a = to_Z b -> a = b.
  Proof.
    intros eq.
    apply to_N_inj.
    unfold to_Z in eq.
    now apply N2Z.inj.
  Qed.

  Lemma of_to_N {bound : N} (n : BoundedN bound) :
    of_N (to_N n) = Some n.
  Proof.
    destruct n as [n prf]; simpl.
    unfold of_N.
    replace (of_N_compare n) with (Some prf); auto.
    unfold of_N_compare.
    now rewrite prf.
  Qed.

  Lemma of_to_nat {bound : N} (n : BoundedN bound) :
    of_nat (to_nat n) = Some n.
  Proof.
    unfold to_nat, of_nat.
    rewrite N2Nat.id.
    apply of_to_N.
  Qed.

  Lemma of_n_not_lt_0 (n : N) :
    (Z.of_N n <? 0)%Z = false.
  Proof.
    destruct (Z.ltb_spec (Z.of_N n) 0).
    - apply Zlt_not_le in H.
      destruct (H (N2Z.is_nonneg n)).
    - reflexivity.
  Qed.

  Lemma of_to_Z {bound : N} (n : BoundedN bound) :
    of_Z (to_Z n) = Some n.
  Proof.
    unfold to_Z, of_Z.
    rewrite of_n_not_lt_0.
    rewrite N2Z.id.
    apply of_to_N.
  Qed.

  Lemma of_N_some {bound : N} {m : N} {n : BoundedN bound} :
    of_N m = Some n -> to_N n = m.
  Proof.
    intros H.
    unfold of_N in H.
    destruct (of_N_compare m); try congruence.
    now inversion H.
  Qed.

  Lemma of_N_none {bound : N} {m : N} :
    @of_N bound m = None -> bound <= m.
  Proof.
    intros H.
    unfold of_N in H.
    destruct (of_N_compare m) eqn:comp; try congruence.
    unfold of_N_compare in comp.
    destruct (bound ?= m) eqn:comp'; congruence.
  Qed.

  Lemma of_nat_some {bound : N} {m : nat} {n : BoundedN bound} :
    of_nat m = Some n -> to_nat n = m.
  Proof.
    intros H.
    unfold to_nat.
    rewrite (of_N_some H).
    apply Nat2N.id.
  Qed.

  Lemma of_nat_none {bound : N} {m : nat} :
    @of_nat bound m = None -> bound <= N.of_nat m.
  Proof. apply of_N_none. Qed.

  Lemma in_map_of_nat (bound : N) (n : BoundedN bound) (xs : list nat) :
    In n (map_option (@of_nat bound) xs) <-> In (to_nat n) xs.
  Proof.
    induction xs as [|x xs IH].
    - split; intros H; inversion H.
    - simpl.
      destruct (of_nat x) eqn:of_nat_x; split; intros H.
      + destruct H.
        * subst.
          left.
          symmetry.
          now apply of_nat_some.
        * tauto.
      + destruct H as [eq | Hin].
        * left.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
198
199
200
          rewrite eq, of_to_nat in of_nat_x.
          congruence.
        * cbn. tauto.
201
202
203
      + tauto.
      + destruct H as [eq | Hin].
        * rewrite eq, of_to_nat in of_nat_x; inversion of_nat_x.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
204
        * tauto.
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
  Qed.

  Module Stdpp.
    Import countable.
    Lemma eq_dec {bound : N} : EqDecision (BoundedN bound).
    Proof.
      intros x y.
      destruct (BoundedN.eqb_spec x y); [left|right]; assumption.
    Qed.

    Global Instance BoundedNEqDec {bound : N} : EqDecision (BoundedN bound) :=
      eq_dec.

    Definition encode_bounded {bound : N} (n : BoundedN bound) : positive :=
      encode (to_N n).

    Definition decode_bounded {bound : N} (n : positive) : option (BoundedN bound) :=
      decode n >>= of_N.

    Lemma decode_encode_bounded {bound : N} (n : BoundedN bound) :
      decode_bounded (encode_bounded n) = Some n.
    Proof.
      unfold decode_bounded, encode_bounded.
      rewrite decode_encode.
      simpl.
      apply of_to_N.
    Qed.

    Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound) :=
      {| encode := encode_bounded;
         decode := decode_bounded;
         decode_encode := decode_encode_bounded; |}.
  End Stdpp.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
239
240
241
242
243
  Definition bounded_elements (bound : N) : list (BoundedN bound) :=
    map_option of_nat (List.seq 0 (N.to_nat bound)).

  Lemma bounded_elements_set (bound : N) :
    NoDup (bounded_elements bound).
244
  Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
    unfold bounded_elements.
    pose proof (seq_NoDup (N.to_nat bound) 0) as nodup.
    pose proof (in_seq (N.to_nat bound) 0) as in_seq'.
    pose proof (fun n => proj1 (in_seq' n)) as in_seq; clear in_seq'.
    induction nodup; try constructor.
    simpl.
    pose proof (in_seq x) as x_bound.
    specialize (x_bound (or_introl eq_refl)).
    destruct x_bound as [useless x_bound]; clear useless.
    simpl in x_bound.
    destruct (of_nat x) eqn:ofnatx. all: cycle 1.
    apply of_nat_none in ofnatx.
    lia.
    constructor.
    + intros Hin.
      apply in_map_of_nat in Hin.
      apply of_nat_some in ofnatx.
      rewrite <- ofnatx in H.
      tauto.
    + apply IHnodup.
      intros n in_n_l.
      apply (in_seq n (or_intror in_n_l)).
  Qed.

  Lemma bounded_elements_all (bound : N) :
    forall a, In a (bounded_elements bound).
  Proof.
    unfold bounded_elements.
    intros t.
    apply in_map_of_nat.
    apply in_seq.
    unfold to_nat.
    destruct t as [t lt].
    simpl.
    change ((bound ?= t) = Gt) with (bound > t) in lt.
    lia.
281
  Qed.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
282
283
284
285
286

  Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
    {| elements := bounded_elements bound;
       elements_set := bounded_elements_set bound;
       elements_all := bounded_elements_all bound; |}.
287
288
289
290
End BoundedN.

Delimit Scope BoundedN_scope with BoundedN.
Bind Scope BoundedN_scope with BoundedN.