Sets of Variables

This file implements set of variables with the aim to be both easy to work with and effient at runtime.

Sets of variables

structure STRIPS.VarSet (n : ℕ) : Type

A set of variables of type Fin n, where n is the number of variables

• toBitVec : BitVec n

  The bitvector internally representing the set of variables.

def STRIPS.instDecidableEqVarSet.decEq {n✝ : ℕ} (x✝ x✝¹ : VarSet n✝) : Decidable (x✝ = x✝¹)

Equations

• STRIPS.instDecidableEqVarSet.decEq { toBitVec := a } { toBitVec := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance STRIPS.instDecidableEqVarSet {n✝ : ℕ} : DecidableEq (VarSet n✝)

Equations

• STRIPS.instDecidableEqVarSet = STRIPS.instDecidableEqVarSet.decEq

@[implicit_reducible]

instance STRIPS.VarSet.instSetLikeFin {n : ℕ} : SetLike (VarSet n) (Fin n)

Equations

• STRIPS.VarSet.instSetLikeFin = { coe := fun (V : STRIPS.VarSet n) => {i : Fin n | V.toBitVec[i] = true}, coe_injective := ⋯ }

theorem STRIPS.VarSet.mem_iff {n : ℕ} {i : Fin n} {V : VarSet n} : i ∈ V ↔ V.toBitVec[i] = true

@[implicit_reducible]

instance STRIPS.VarSet.instDecidableMemFin {n : ℕ} {i : Fin n} {V : VarSet n} : Decidable (i ∈ V)

Equations

• STRIPS.VarSet.instDecidableMemFin = ⋯.mpr inferInstance

@[reducible]

instance STRIPS.VarSet.instHasSubset {n : ℕ} : HasSubset (VarSet n)

Equations

• STRIPS.VarSet.instHasSubset = { Subset := fun (V V' : STRIPS.VarSet n) => ∀ (i : Fin n), i ∈ V → i ∈ V' }

theorem STRIPS.VarSet.subset_def {n : ℕ} {V V' : VarSet n} : V ⊆ V' ↔ ∀ (i : Fin n), i ∈ V → i ∈ V'

@[implicit_reducible]

instance STRIPS.VarSet.instEmptyCollection {n : ℕ} : EmptyCollection (VarSet n)

Equations

• STRIPS.VarSet.instEmptyCollection = { emptyCollection := { toBitVec := BitVec.zero n } }

@[simp]

theorem STRIPS.VarSet.mem_empty {n : ℕ} {i : Fin n} : ¬i ∈ ∅

def STRIPS.VarSet.insert {n : ℕ} (i : Fin n) (V : VarSet n) : VarSet n

Return the VarSet containing all variables in V and the variable i.

Equations

• STRIPS.VarSet.insert i V = { toBitVec := V.toBitVec ||| BitVec.twoPow n ↑i }

@[simp]

theorem STRIPS.VarSet.mem_insert {n : ℕ} {V : VarSet n} {i j : Fin n} : j ∈ insert i V ↔ j ∈ V ∨ j = i

def STRIPS.VarSet.all {n : ℕ} : VarSet n

Return the VarSet containing all variables.

Equations

• STRIPS.VarSet.all = { toBitVec := BitVec.allOnes n }

@[simp]

theorem STRIPS.VarSet.mem_all {n : ℕ} {i : Fin n} : i ∈ all

def STRIPS.VarSet.ofFn {n : ℕ} (f : Fin n → Bool) : VarSet n

Return the VarSet containing all variables i for which f i is true.

Equations

• STRIPS.VarSet.ofFn f = { toBitVec := BitVec.ofFnLE f }

@[simp]

theorem STRIPS.VarSet.mem_ofFn {n : ℕ} {f : Fin n → Bool} {i : Fin n} : i ∈ ofFn f ↔ f i = true

def STRIPS.VarSet.ofList {n : ℕ} (l : List (Fin n)) : VarSet n

Return the VarSet containing all variables in the given list.

Equations

• STRIPS.VarSet.ofList l = List.foldr STRIPS.VarSet.insert ∅ l

@[simp]

theorem STRIPS.VarSet.mem_ofList {n : ℕ} {l : List (Fin n)} {i : Fin n} : i ∈ ofList l ↔ i ∈ l

@[implicit_reducible]

instance STRIPS.VarSet.instUnion {n : ℕ} : Union (VarSet n)

Equations

• STRIPS.VarSet.instUnion = { union := fun (V V' : STRIPS.VarSet n) => { toBitVec := V.toBitVec ||| V'.toBitVec } }

@[simp]

theorem STRIPS.VarSet.mem_union {n : ℕ} {V V' : VarSet n} {i : Fin n} : i ∈ V ∪ V' ↔ i ∈ V ∨ i ∈ V'

@[simp]

theorem STRIPS.VarSet.empty_union {n : ℕ} {V : VarSet n} : ∅ ∪ V = V

@[simp]

theorem STRIPS.VarSet.union_empty {n : ℕ} {V : VarSet n} : V ∪ ∅ = V

@[implicit_reducible]

instance STRIPS.VarSet.instInter {n : ℕ} : Inter (VarSet n)

Equations

• STRIPS.VarSet.instInter = { inter := fun (V V' : STRIPS.VarSet n) => { toBitVec := V.toBitVec &&& V'.toBitVec } }

@[simp]

theorem STRIPS.VarSet.mem_inter {n : ℕ} {V V' : VarSet n} {i : Fin n} : i ∈ V ∩ V' ↔ i ∈ V ∧ i ∈ V'

@[simp]

theorem STRIPS.VarSet.empty_inter {n : ℕ} {V : VarSet n} : ∅ ∩ V = ∅

@[simp]

theorem STRIPS.VarSet.inter_eq_empty_iff {n : ℕ} {V V' : VarSet n} : V ∩ V' = ∅ ↔ ∀ (i : Fin n), i ∈ V → ¬i ∈ V'

@[implicit_reducible]

instance STRIPS.VarSet.instCompl {n : ℕ} : Compl (VarSet n)

Equations

• STRIPS.VarSet.instCompl = { compl := fun (V : STRIPS.VarSet n) => { toBitVec := ~~~V.toBitVec } }

@[simp]

theorem STRIPS.VarSet.mem_compl {n : ℕ} {V : VarSet n} {i : Fin n} : i ∈ Vᶜ ↔ ¬i ∈ V

@[implicit_reducible]

instance STRIPS.VarSet.instSDiff {n : ℕ} : SDiff (VarSet n)

Equations

• STRIPS.VarSet.instSDiff = { sdiff := fun (V V' : STRIPS.VarSet n) => { toBitVec := V.toBitVec &&& ~~~V'.toBitVec } }

@[simp]

theorem STRIPS.VarSet.mem_diff {n : ℕ} {V V' : VarSet n} {i : Fin n} : i ∈ V \ V' ↔ i ∈ V ∧ ¬i ∈ V'

def STRIPS.VarSet.foldl {α : Sort u_1} {n : ℕ} (f : α → Fin n → α) (init : α) (V : VarSet n) : α

Folds a function over all variables in V with starting value init. The variables are combined in increasing order.

Equations

• STRIPS.VarSet.foldl f init V = Fin.foldl n (fun (a : α) (i : Fin n) => if i ∈ V then f a i else a) init

theorem STRIPS.VarSet.foldl_cons {α : Type u_1} {n : ℕ} {V : VarSet n} {f : Fin n → α} {a : α} {as : List α} : a ∈ foldl (fun (a : List α) (i : Fin n) => f i :: a) as V ↔ (∃ (i : Fin n), i ∈ V ∧ a = f i) ∨ a ∈ as

def STRIPS.VarSet.map {n m : ℕ} (V : VarSet n) (f : Fin n → Fin m) : VarSet m

Return the VarSet containing the variables f i for every variable i in V.

Equations

• V.map f = STRIPS.VarSet.foldl (fun (V' : STRIPS.VarSet m) (i : Fin n) => STRIPS.VarSet.insert (f i) V') ∅ V

theorem STRIPS.VarSet.mem_map {n m : ℕ} {V : VarSet n} {f : Fin n → Fin m} {i : Fin m} : i ∈ V.map f ↔ ∃ (j : Fin n), j ∈ V ∧ i = f j

@[implicit_reducible]

instance STRIPS.VarSet.instToFormat {n : ℕ} : Std.ToFormat (VarSet n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance STRIPS.VarSet.instToString {n : ℕ} : ToString (VarSet n)

Equations

• STRIPS.VarSet.instToString = { toString := fun (V : STRIPS.VarSet n) => (Std.format V).pretty }