Documentation

Init.Data.BitVec.Decidable

Decidable quantifiers #

source
theorem BitVec.forall_zero_iff {P : BitVec 0 → Prop} :
(∀ (v : BitVec 0), P v) ↔ P 0#0
source
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)
source
instance BitVec.instDecidableForallBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
Decidable (∀ (v : BitVec 0), P v)
Equations
source
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)
Equations
source
instance BitVec.instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
Decidable (∃ (v : BitVec 0), P v)
Equations
source
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)
Equations
source
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.

Equations
source
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.

Equations