Forcing a Nat to be one of 4 values

Stream: general

[l1mey]

Is there a nice way to make n only be 8, 16, 32, 64, so that it looks nice in writing and constructing a proof? In general having a proof that is polymorphic on all possible bitvectors might be a bit much for my purposes.

theorem conSwap {n} (a b con1 con2 : BitVec n)
    : (a + con1) - (b + con2) = (a - b) + (con1 - con2) := by
  grind

I tried this but it didn't work, probably due to my misunderstanding of dependent types:

inductive Bits (n : Nat) where
  | i1 : Bits 1
  | i8 : Bits 8
  | i16 : Bits 16
  | i32 : Bits 32
  | i64 : Bits 64

theorem conSwap (Bits n) (a b con1 con2 : BitVec n)
    : (a + con1) - (b + con2) = (a - b) + (con1 - con2) := by
  grind

[Aaron Liu]

why not just make it work for all bitvectors

[Aaron Liu]

what does having this restriction do for you

[l1mey]

It makes automatic proving and bv_decide work. I'm going to be dealing with thousands of these little lemmas and would like to prove these with as little effort as possible.

[Robin Arnez]

You can use something like

inductive Bits : Nat → Prop where
  | i1 : Bits 1
  | i8 : Bits 8
  | i16 : Bits 16
  | i32 : Bits 32
  | i64 : Bits 64

theorem conSwap (h : Bits n) (a b con1 con2 : BitVec n)
    : (a + con1) - (b + con2) = (a - b) + (con1 - con2) := by
  cases h <;> grind

[l1mey]

This does work for me, I appreciate it.