data.semiquot

# Semiquotients #

A data type for semiquotients, which are classically equivalent to nonempty sets, but are useful for programming; the idea is that a semiquotient set S represents some (particular but unknown) element of S. This can be used to model nondeterministic functions, which return something in a range of values (represented by the predicate S) but are not completely determined.

structure semiquot (α : Type u_1) :
Type u_1

A member of semiquot α is classically a nonempty set α, and in the VM is represented by an element of α; the relation between these is that the VM element is required to be a member of the set s. The specific element of s that the VM computes is hidden by a quotient construction, allowing for the representation of nondeterministic functions.

Instances for semiquot
@[protected, instance]
def semiquot.has_mem {α : Type u_1} :
(semiquot α)
Equations
def semiquot.mk {α : Type u_1} {a : α} {s : set α} (h : a s) :

Construct a semiquot α from h : a ∈ s where s : set α.

Equations
theorem semiquot.ext_s {α : Type u_1} {q₁ q₂ : semiquot α} :
q₁ = q₂ q₁.s = q₂.s
theorem semiquot.ext {α : Type u_1} {q₁ q₂ : semiquot α} :
q₁ = q₂ ∀ (a : α), a q₁ a q₂
theorem semiquot.exists_mem {α : Type u_1} (q : semiquot α) :
∃ (a : α), a q
theorem semiquot.eq_mk_of_mem {α : Type u_1} {q : semiquot α} {a : α} (h : a q) :
q =
theorem semiquot.nonempty {α : Type u_1} (q : semiquot α) :
@[protected]
def semiquot.pure {α : Type u_1} (a : α) :

pure a is a reinterpreted as an unspecified element of {a}.

Equations
@[simp]
theorem semiquot.mem_pure' {α : Type u_1} {a b : α} :
a = b
def semiquot.blur' {α : Type u_1} (q : semiquot α) {s : set α} (h : q.s s) :

Replace s in a semiquot with a superset.

Equations
def semiquot.blur {α : Type u_1} (s : set α) (q : semiquot α) :

Replace s in a q : semiquot α with a union s ∪ q.s

Equations
theorem semiquot.blur_eq_blur' {α : Type u_1} (q : semiquot α) (s : set α) (h : q.s s) :
= q.blur' h
@[simp]
theorem semiquot.mem_blur' {α : Type u_1} (q : semiquot α) {s : set α} (h : q.s s) {a : α} :
a q.blur' h a s
def semiquot.of_trunc {α : Type u_1} (q : trunc α) :

Convert a trunc α to a semiquot α.

Equations
def semiquot.to_trunc {α : Type u_1} (q : semiquot α) :

Convert a semiquot α to a trunc α.

Equations
def semiquot.lift_on {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → β) (h : ∀ (a : α), a q∀ (b : α), b qf a = f b) :
β

If f is a constant on q.s, then q.lift_on f is the value of f at any point of q.

Equations
theorem semiquot.lift_on_of_mem {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → β) (h : ∀ (a : α), a q∀ (b : α), b qf a = f b) (a : α) (aq : a q) :
q.lift_on f h = f a
def semiquot.map {α : Type u_1} {β : Type u_2} (f : α → β) (q : semiquot α) :

Apply a function to the unknown value stored in a semiquot α.

Equations
@[simp]
theorem semiquot.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) (q : semiquot α) (b : β) :
b q ∃ (a : α), a q f a = b
def semiquot.bind {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → ) :

Apply a function returning a semiquot to a semiquot.

Equations
@[simp]
theorem semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → ) (b : β) :
b q.bind f ∃ (a : α) (H : a q), b f a
@[protected, instance]
Equations
@[simp]
theorem semiquot.map_def {α β : Type u_1} :
@[simp]
theorem semiquot.bind_def {α β : Type u_1} :
@[simp]
theorem semiquot.mem_pure {α : Type u_1} {a b : α} :
a = b
theorem semiquot.mem_pure_self {α : Type u_1} (a : α) :
@[simp]
theorem semiquot.pure_inj {α : Type u_1} {a b : α} :
a = b
@[protected, instance]
@[protected, instance]
def semiquot.has_le {α : Type u_1} :
Equations
@[protected, instance]
def semiquot.partial_order {α : Type u_1} :
Equations
@[protected, instance]
def semiquot.semilattice_sup {α : Type u_1} :
Equations
@[simp]
theorem semiquot.pure_le {α : Type u_1} {a : α} {s : semiquot α} :
a s
def semiquot.is_pure {α : Type u_1} (q : semiquot α) :
Prop

Assert that a semiquot contains only one possible value.

Equations
def semiquot.get {α : Type u_1} (q : semiquot α) (h : q.is_pure) :
α

Extract the value from a is_pure semiquotient.

Equations
theorem semiquot.get_mem {α : Type u_1} {q : semiquot α} (p : q.is_pure) :
q.get p q
theorem semiquot.eq_pure {α : Type u_1} {q : semiquot α} (p : q.is_pure) :
@[simp]
theorem semiquot.pure_is_pure {α : Type u_1} (a : α) :
theorem semiquot.is_pure_iff {α : Type u_1} {s : semiquot α} :
s.is_pure ∃ (a : α),
theorem semiquot.is_pure.mono {α : Type u_1} {s t : semiquot α} (st : s t) (h : t.is_pure) :
theorem semiquot.is_pure.min {α : Type u_1} {s t : semiquot α} (h : t.is_pure) :
s t s = t
theorem semiquot.is_pure_of_subsingleton {α : Type u_1} [subsingleton α] (q : semiquot α) :
def semiquot.univ {α : Type u_1} [inhabited α] :

univ : semiquot α represents an unspecified element of univ : set α.

Equations
@[protected, instance]
def semiquot.inhabited {α : Type u_1} [inhabited α] :
Equations
@[simp]
theorem semiquot.mem_univ {α : Type u_1} [inhabited α] (a : α) :
theorem semiquot.univ_unique {α : Type u_1} (I J : inhabited α) :
@[simp]
theorem semiquot.is_pure_univ {α : Type u_1} [inhabited α] :
@[protected, instance]
def semiquot.order_top {α : Type u_1} [inhabited α] :
Equations