BoundedN.v 7.46 KB
 Jakob Botsch Nielsen committed Apr 19, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 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 ``````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 Coq Require Import JMeq. From stdpp Require countable. Import ListNotations. Local Open Scope N. Inductive BoundedN (bound : N) := | bounded (n : N) (_ : (bound ?= n) = Gt). 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 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 committed Apr 19, 2019 73 `````` Hint Resolve to_N_inj : core. `````` Jakob Botsch Nielsen committed Apr 19, 2019 74 75 76 77 78 79 80 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 198 199 200 201 202 203 204 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 `````` 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 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. rewrite eq in of_nat_x. rewrite of_to_nat in of_nat_x; prove. * prove. + tauto. + destruct H as [eq | Hin]. * rewrite eq, of_to_nat in of_nat_x; inversion of_nat_x. * prove. 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 committed Apr 19, 2019 232 233 234 235 236 `````` 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). `````` Jakob Botsch Nielsen committed Apr 19, 2019 237 `````` Proof. `````` Jakob Botsch Nielsen committed Apr 19, 2019 238 239 240 241 242 243 244 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 `````` 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. `````` Jakob Botsch Nielsen committed Apr 19, 2019 274 `````` Qed. `````` Jakob Botsch Nielsen committed Apr 19, 2019 275 276 277 278 279 `````` 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; |}. `````` Jakob Botsch Nielsen committed Apr 19, 2019 280 281 282 283 ``````End BoundedN. Delimit Scope BoundedN_scope with BoundedN. Bind Scope BoundedN_scope with BoundedN.``````