Decidable quantifiers

theorem BitVec.forall_zero_iff {P : BitVec 0 → Prop} : (∀ (v : BitVec 0), P v) ↔ P 0#0

theorem BitVec.forall_cons_iff {n : Nat} {P : BitVec (n + 1) → Prop} : (∀ (v : BitVec (n + 1)), P v) ↔ ∀ (x : Bool) (v : BitVec n), P (cons x v)

@[implicit_reducible]

instance BitVec.instDecidableForallBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] : Decidable (∀ (v : BitVec 0), P v)

@[implicit_reducible]

instance BitVec.instDecidableForallBitVecSucc {n : Nat} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), P (cons x v))] : Decidable (∀ (v : BitVec (n + 1)), P v)

@[implicit_reducible]

instance BitVec.instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] : Decidable (∃ (v : BitVec 0), P v)

@[implicit_reducible]

instance BitVec.instDecidableExistsBitVecSucc {n : Nat} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), ¬P (cons x v))] : Decidable (∃ (v : BitVec (n + 1)), P v)

@[implicit_reducible]

instance BitVec.instDecidableForallBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] : Decidable (∀ (v : BitVec n), P v)

For small numerals this isn't necessary (as typeclass search can use the above two instances), but for large numerals this provides a shortcut. Note, however, that for large numerals the decision procedure may be very slow, and you should use bv_decide if possible.

@[implicit_reducible]

instance BitVec.instDecidableExistsBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] : Decidable (∃ (v : BitVec n), P v)

For small numerals this isn't necessary (as typeclass search can use the above two instances), but for large numerals this provides a shortcut. Note, however, that for large numerals the decision procedure may be very slow.