Decidable membership and hashing for UInt8Array

Decidable membership, slice hashing and the lawful BEq and Hashable instances on slices. Left out of the float types, which have no DecidableEq.

theorem ScalarArray.UInt8Array.contains_iff_mem {a : UInt8Array} {x : UInt8} : a.contains x = true ↔ x ∈ a

@[implemented_by _private.ScalarArray.UInt8.Decidable.0.ScalarArray.UInt8Array.decMemImpl]

def ScalarArray.UInt8Array.decMem (x : UInt8) (a : UInt8Array) : Decidable (x ∈ a)

Decides membership with contains. Logically it decides membership in a.toList, so that decide can evaluate it.

Equations

• ScalarArray.UInt8Array.decMem x a = decidable_of_iff (x ∈ a.toList) ⋯

@[instance_reducible]

instance ScalarArray.UInt8Array.instDecidableMemUInt8 (x : UInt8) (a : UInt8Array) : Decidable (x ∈ a)

Equations

• ScalarArray.UInt8Array.instDecidableMemUInt8 x a = ScalarArray.UInt8Array.decMem x a

@[simp]

theorem ScalarArray.UInt8Array.contains_eq_mem {a : UInt8Array} {x : UInt8} : a.contains x = decide (x ∈ a)

theorem ScalarArray.UInt8Array.Slice.contains_iff_mem {s : UInt8Array.Slice} {x : UInt8} : s.contains x = true ↔ x ∈ s

@[implemented_by _private.ScalarArray.UInt8.Decidable.0.ScalarArray.UInt8Array.Slice.decMemImpl]

def ScalarArray.UInt8Array.Slice.decMem (x : UInt8) (s : UInt8Array.Slice) : Decidable (x ∈ s)

Decides membership with contains. Logically it decides membership in s.copy.toList, so that decide can evaluate it.

Equations

• ScalarArray.UInt8Array.Slice.decMem x s = decidable_of_iff (x ∈ s.copy.toList) ⋯

@[instance_reducible]

instance ScalarArray.UInt8Array.instDecidableMemUInt8Slice (x : UInt8) (s : UInt8Array.Slice) : Decidable (x ∈ s)

Equations

• ScalarArray.UInt8Array.instDecidableMemUInt8Slice x s = ScalarArray.UInt8Array.Slice.decMem x s

@[implemented_by _private.ScalarArray.UInt8.Decidable.0.ScalarArray.UInt8Array.Slice.hashImpl]

def ScalarArray.UInt8Array.Slice.hash (s : UInt8Array.Slice) : UInt64

The same hash as s.copy, so slices with the same elements have the same hash.

Equations

• s.hash = hash s.copy

@[instance_reducible]

instance ScalarArray.UInt8Array.instHashableSlice : Hashable UInt8Array.Slice

Equations

• ScalarArray.UInt8Array.instHashableSlice = { hash := ScalarArray.UInt8Array.Slice.hash }

theorem ScalarArray.UInt8Array.Slice.hash_eq_hash_copy (s : UInt8Array.Slice) : Hashable.hash s = Hashable.hash s.copy

theorem ScalarArray.UInt8Array.Slice.beq_iff_copy_eq {s t : UInt8Array.Slice} : (s == t) = true ↔ s.copy = t.copy

instance ScalarArray.UInt8Array.instEquivBEqSlice : EquivBEq UInt8Array.Slice

instance ScalarArray.UInt8Array.instLawfulHashableSlice : LawfulHashable UInt8Array.Slice