# Documentation

Mathlib.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
• mk' :: (
• Set containing some element of α

s : Set α
• Assertion of non-emptiness via Trunc

val : Trunc s
• )

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
Equations
• Semiquot.instMembershipSemiquot = { mem := fun a q => a q.s }
def Semiquot.mk {α : Type u_1} {a : α} {s : Set α} (h : a s) :

Construct a Semiquot α from h : a ∈ s where s : Set α.

Equations
• = { s := s, val := Trunc.mk { val := a, property := h } }
theorem Semiquot.ext_s {α : Type u_1} {q₁ : } {q₂ : } :
q₁ = q₂ q₁.s = q₂.s
theorem Semiquot.ext {α : Type u_1} {q₁ : } {q₂ : } :
q₁ = q₂ ∀ (a : α), a q₁ a q₂
theorem Semiquot.exists_mem {α : Type u_1} (q : ) :
a, a q
theorem Semiquot.eq_mk_of_mem {α : Type u_1} {q : } {a : α} (h : a q) :
q =
theorem Semiquot.nonempty {α : Type u_1} (q : ) :
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 : ) {s : Set α} (h : q.s s) :

Replace s in a Semiquot with a superset.

Equations
• One or more equations did not get rendered due to their size.
def Semiquot.blur {α : Type u_1} (s : Set α) (q : ) :

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

Equations
theorem Semiquot.blur_eq_blur' {α : Type u_1} (q : ) (s : Set α) (h : q.s s) :
=
@[simp]
theorem Semiquot.mem_blur' {α : Type u_1} (q : ) {s : Set α} (h : q.s s) {a : α} :
a a s
def Semiquot.ofTrunc {α : Type u_1} (q : ) :

Convert a Trunc α to a Semiquot α.

Equations
• = { s := Set.univ, val := Trunc.map (fun a => { val := a, property := trivial }) q }
def Semiquot.toTrunc {α : Type u_1} (q : ) :

Convert a Semiquot α to a Trunc α.

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

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

Equations
• = Trunc.liftOn q.val (fun x => f x) (_ : ∀ (x y : q.s), f x = f y)
theorem Semiquot.liftOn_ofMem {α : Type u_1} {β : Type u_2} (q : ) (f : αβ) (h : ∀ (a : α), a q∀ (b : α), b qf a = f b) (a : α) (aq : a q) :
= f a
def Semiquot.map {α : Type u_1} {β : Type u_2} (f : αβ) (q : ) :

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

Equations
• = { s := f '' q.s, val := Trunc.map (fun x => { val := f x, property := (_ : f x f '' q.s) }) q.val }
@[simp]
theorem Semiquot.mem_map {α : Type u_1} {β : Type u_2} (f : αβ) (q : ) (b : β) :
b a, a q f a = b
def Semiquot.bind {α : Type u_1} {β : Type u_2} (q : ) (f : α) :

Apply a function returning a Semiquot to a Semiquot.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : ) (f : α) (b : β) :
b a, a q b f a
@[simp]
theorem Semiquot.map_def {α : Type u_1} {β : Type u_1} :
(fun x x_1 => x <\$> x_1) = Semiquot.map
@[simp]
theorem Semiquot.bind_def {α : Type u_1} {β : Type u_1} :
(fun x x_1 => x >>= x_1) = Semiquot.bind
@[simp]
theorem Semiquot.mem_pure {α : Type u_1} {a : α} {b : α} :
a pure b a = b
theorem Semiquot.mem_pure_self {α : Type u_1} (a : α) :
a pure a
@[simp]
theorem Semiquot.pure_inj {α : Type u_1} {a : α} {b : α} :
pure a = pure b a = b
instance Semiquot.instLESemiquot {α : Type u_1} :
LE ()
Equations
• Semiquot.instLESemiquot = { le := fun s t => s.s t.s }
instance Semiquot.partialOrder {α : Type u_1} :
Equations
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Semiquot.pure_le {α : Type u_1} {a : α} {s : } :
pure a s a s
def Semiquot.IsPure {α : Type u_1} (q : ) :

Assert that a Semiquot contains only one possible value.

Equations
• = ∀ (a : α), a q∀ (b : α), b qa = b
def Semiquot.get {α : Type u_1} (q : ) (h : ) :
α

Extract the value from a IsPure semiquotient.

Equations
theorem Semiquot.get_mem {α : Type u_1} {q : } (p : ) :
q
theorem Semiquot.eq_pure {α : Type u_1} {q : } (p : ) :
q = pure ()
@[simp]
theorem Semiquot.pure_isPure {α : Type u_1} (a : α) :
theorem Semiquot.isPure_iff {α : Type u_1} {s : } :
a, s = pure a
theorem Semiquot.IsPure.mono {α : Type u_1} {s : } {t : } (st : s t) (h : ) :
theorem Semiquot.IsPure.min {α : Type u_1} {s : } {t : } (h : ) :
s t s = t
theorem Semiquot.isPure_of_subsingleton {α : Type u_1} [inst : ] (q : ) :
def Semiquot.univ {α : Type u_1} [inst : ] :

univ : Semiquot α represents an unspecified element of univ : Set α.

Equations
instance Semiquot.instInhabitedSemiquot {α : Type u_1} [inst : ] :
Equations
• Semiquot.instInhabitedSemiquot = { default := Semiquot.univ }
@[simp]
theorem Semiquot.mem_univ {α : Type u_1} [inst : ] (a : α) :
a Semiquot.univ
theorem Semiquot.univ_unique {α : Type u_1} (I : ) (J : ) :
Semiquot.univ = Semiquot.univ
@[simp]
theorem Semiquot.isPure_univ {α : Type u_1} [inst : ] :
Semiquot.IsPure Semiquot.univ
Equations
• Semiquot.instOrderTopSemiquotInstLESemiquot = OrderTop.mk (_ : ∀ (x : ), x.s Set.univ)