-
Notifications
You must be signed in to change notification settings - Fork 298
/
basic.lean
96 lines (79 loc) · 3.55 KB
/
basic.lean
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
/-
Copyright (c) 2020 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import data.bitvec.core
import data.fin.basic
import tactic.monotonicity
import tactic.norm_num
namespace bitvec
instance (n : ℕ) : preorder (bitvec n) :=
preorder.lift bitvec.to_nat
/-- convert `fin` to `bitvec` -/
def of_fin {n : ℕ} (i : fin $ 2^n) : bitvec n :=
bitvec.of_nat _ i.val
lemma of_fin_val {n : ℕ} (i : fin $ 2^n) : (of_fin i).to_nat = i.val :=
by rw [of_fin,to_nat_of_nat,nat.mod_eq_of_lt]; apply i.is_lt
/-- convert `bitvec` to `fin` -/
def to_fin {n : ℕ} (i : bitvec n) : fin $ 2^n :=
i.to_nat
lemma add_lsb_eq_twice_add_one {x b} :
add_lsb x b = 2 * x + cond b 1 0 :=
by simp [add_lsb,two_mul]
lemma to_nat_eq_foldr_reverse {n : ℕ} (v : bitvec n) :
v.to_nat = v.to_list.reverse.foldr (flip add_lsb) 0 :=
by rw [list.foldr_reverse, flip]; refl
lemma to_nat_lt {n : ℕ} (v : bitvec n) : v.to_nat < 2^n :=
begin
suffices : v.to_nat + 1 ≤ 2 ^ n, { simpa },
rw to_nat_eq_foldr_reverse,
cases v with xs h,
dsimp [bitvec.to_nat,bits_to_nat],
rw ← list.length_reverse at h,
generalize_hyp : xs.reverse = ys at ⊢ h, clear xs,
induction ys generalizing n,
{ simp [← h] },
{ simp only [←h, pow_add, flip, list.length, list.foldr, pow_one],
rw [add_lsb_eq_twice_add_one],
transitivity 2 * list.foldr (λ (x : bool) (y : ℕ), add_lsb y x) 0 ys_tl + 2 * 1,
{ ac_mono, rw two_mul, mono, cases ys_hd; simp },
{ rw ← left_distrib, ac_mono,
exact ys_ih rfl, norm_num } }
end
lemma add_lsb_div_two {x b} : add_lsb x b / 2 = x :=
by cases b; simp only [nat.add_mul_div_left, add_lsb, ←two_mul, add_comm, nat.succ_pos',
nat.mul_div_right, gt_iff_lt, zero_add, cond]; norm_num
lemma to_bool_add_lsb_mod_two {x b} : to_bool (add_lsb x b % 2 = 1) = b :=
by cases b; simp only [to_bool_iff, nat.add_mul_mod_self_left, add_lsb, ←two_mul, add_comm,
bool.to_bool_false, nat.mul_mod_right, zero_add, cond, zero_ne_one]; norm_num
lemma of_nat_to_nat {n : ℕ} (v : bitvec n) : bitvec.of_nat _ v.to_nat = v :=
begin
cases v with xs h,
ext1,
change vector.to_list _ = xs,
dsimp [bitvec.to_nat,bits_to_nat],
rw ← list.length_reverse at h,
rw [← list.reverse_reverse xs,list.foldl_reverse],
generalize_hyp : xs.reverse = ys at ⊢ h, clear xs,
induction ys generalizing n,
{ cases h, simp [bitvec.of_nat] },
{ simp only [←nat.succ_eq_add_one, list.length] at h, subst n,
simp only [bitvec.of_nat, vector.to_list_cons, vector.to_list_nil, list.reverse_cons,
vector.to_list_append, list.foldr],
erw [add_lsb_div_two, to_bool_add_lsb_mod_two],
congr, apply ys_ih, refl }
end
lemma to_fin_val {n : ℕ} (v : bitvec n) : (to_fin v : ℕ) = v.to_nat :=
by rw [to_fin, fin.coe_of_nat_eq_mod, nat.mod_eq_of_lt]; apply to_nat_lt
lemma to_fin_le_to_fin_of_le {n} {v₀ v₁ : bitvec n} (h : v₀ ≤ v₁) : v₀.to_fin ≤ v₁.to_fin :=
show (v₀.to_fin : ℕ) ≤ v₁.to_fin,
by rw [to_fin_val,to_fin_val]; exact h
lemma of_fin_le_of_fin_of_le {n : ℕ} {i j : fin (2^n)} (h : i ≤ j) : of_fin i ≤ of_fin j :=
show (bitvec.of_nat n i).to_nat ≤ (bitvec.of_nat n j).to_nat,
by { simp only [to_nat_of_nat, nat.mod_eq_of_lt, fin.is_lt], exact h }
lemma to_fin_of_fin {n} (i : fin $ 2^n) : (of_fin i).to_fin = i :=
fin.eq_of_veq (by simp [to_fin_val, of_fin, to_nat_of_nat, nat.mod_eq_of_lt, i.is_lt])
lemma of_fin_to_fin {n} (v : bitvec n) : of_fin (to_fin v) = v :=
by dsimp [of_fin]; rw [to_fin_val, of_nat_to_nat]
end bitvec