bv_ex.lean

universes u

def bitvector (sz : nat) : Type :=
{ n : nat // n < 2^sz }

/- We use `by apply bv_mod_lt` to discharge the property above in
   many bitvector definitions. -/
lemma bv_mod_lt (n : nat) (sz : nat) : n % (2^sz) < 2^sz :=
begin
  apply nat.mod_lt,
  apply nat.pos_pow_of_pos,
  tactic.comp_val
end

/- We use `♯` as a shorthand for `by apply bv_mod_lt` -/
local notation `♯` := by apply bv_mod_lt

def bv_add {sz : nat} : bitvector sz → bitvector sz → bitvector sz
| ⟨v₁, _⟩ ⟨v₂, _⟩ := ⟨(v₁ + v₂)%2^sz, ♯⟩

def bv_mul {sz : nat} : bitvector sz → bitvector sz → bitvector sz
| ⟨v₁, _⟩ ⟨v₂, _⟩ := ⟨(v₁ * v₂)%2^sz, ♯⟩

/- A generic basic bitvector interface -/
class is_bitvector (α : Type u) :=
(size : α → nat)
(add  : α → α → α)
(mul  : α → α → α)
-- ...

/- Any type that implements tha `is_bitvector` interface also implements `has_add` -/
instance is_bitvector_has_add (α : Type u) [is_bitvector α] : has_add α :=
⟨is_bitvector.add⟩

instance is_bitvector_has_mul (α : Type u) [is_bitvector α] : has_mul α :=
⟨is_bitvector.mul⟩

/- The type `bitvector sz` implements the bitvector interface -/
instance (sz : nat) : is_bitvector (bitvector sz) :=
{ size := λ _, sz,
  add  := bv_add,
  mul  := bv_mul }

def double {sz : nat} (a : bitvector sz) : bitvector sz :=
a + a

inductive op
| op_add | op_mul | op_sub

/-
We can automatically generate `decidable_eq` instance for inductive datatypes (which do not contain functions).
Remark: this tactic is implemented in Lean itself.
-/
instance : decidable_eq op :=
by tactic.mk_dec_eq_instance

/- Instance is also a definition, we can write the function while defining the instance. -/
instance : has_to_string op :=
⟨λ a, match a with
      | op.op_add := "add"
      | op.op_mul := "mul"
      | op.op_sub := "sub"
      end⟩