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

instance Semiquot.instMembershipSemiquot {α : Type u_1} :

Membership α (Semiquot α)

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

Semiquot.mk h = { s := s, val := Trunc.mk { val := a, property := h } }

theorem Semiquot.ext_s {α : Type u_1} {q₁ : Semiquot α} {q₂ : Semiquot α} :

q₁ = q₂ ↔ q₁.s = q₂.s

theorem Semiquot.ext {α : Type u_1} {q₁ : Semiquot α} {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 = Semiquot.mk h

theorem Semiquot.nonempty {α : Type u_1} (q : Semiquot α) :

Set.Nonempty q.s

def Semiquot.pure {α : Type u_1} (a : α) :

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

Equations

Semiquot.pure a = Semiquot.mk (_ : a ∈ {a})

@[simp]

theorem Semiquot.mem_pure' {α : Type u_1} {a : α} {b : α} :

a ∈ Semiquot.pure 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

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

def Semiquot.blur {α : Type u_1} (s : Set α) (q : Semiquot α) :

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

Equations

Semiquot.blur s q = Semiquot.blur' q (_ : q.s ⊆ s ∪ q.s)

theorem Semiquot.blur_eq_blur' {α : Type u_1} (q : Semiquot α) (s : Set α) (h : q.s ⊆ s) :

Semiquot.blur s q = Semiquot.blur' q h

@[simp]

theorem Semiquot.mem_blur' {α : Type u_1} (q : Semiquot α) {s : Set α} (h : q.s ⊆ s) {a : α} :

a ∈ Semiquot.blur' q h ↔ a ∈ s

def Semiquot.ofTrunc {α : Type u_1} (q : Trunc α) :

Convert a Trunc α to a Semiquot α.

Equations

Semiquot.ofTrunc q = { s := Set.univ, val := Trunc.map (fun a => { val := a, property := trivial }) q }

def Semiquot.toTrunc {α : Type u_1} (q : Semiquot α) :

Convert a Semiquot α to a Trunc α.

Equations

Semiquot.toTrunc q = Trunc.map Subtype.val q.val

def Semiquot.liftOn {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → β) (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f 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

Semiquot.liftOn q f h = 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 : Semiquot α) (f : α → β) (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b) (a : α) (aq : a ∈ q) :

Semiquot.liftOn q 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

Semiquot.map f q = { 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 : Semiquot α) (b : β) :

b ∈ Semiquot.map f q ↔ ∃ a, a ∈ q ∧ f a = b

def Semiquot.bind {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → Semiquot β) :

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 : Semiquot α) (f : α → Semiquot β) (b : β) :

b ∈ Semiquot.bind q f ↔ ∃ a, a ∈ q ∧ b ∈ f a

instance Semiquot.instMonadSemiquot :

Equations

Semiquot.instMonadSemiquot = Monad.mk

@[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 : α) :

@[simp]

theorem Semiquot.pure_inj {α : Type u_1} {a : α} {b : α} :

pure a = pure b ↔ a = b

instance Semiquot.instLawfulMonadSemiquotInstMonadSemiquot :

LawfulMonad Semiquot

Equations

Semiquot.instLawfulMonadSemiquotInstMonadSemiquot = Semiquot.instLawfulMonadSemiquotInstMonadSemiquot.proof_1

instance Semiquot.instLESemiquot {α : Type u_1} :

LE (Semiquot α)

Equations

Semiquot.instLESemiquot = { le := fun s t => s.s ⊆ t.s }

instance Semiquot.partialOrder {α : Type u_1} :

PartialOrder (Semiquot α)

Equations

Semiquot.partialOrder = PartialOrder.mk (_ : ∀ (s t : Semiquot α), s ≤ t → t ≤ s → s = t)

instance Semiquot.instSemilatticeSupSemiquot {α : Type u_1} :

SemilatticeSup (Semiquot α)

Equations

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

@[simp]

theorem Semiquot.pure_le {α : Type u_1} {a : α} {s : Semiquot α} :

pure a ≤ s ↔ a ∈ s

def Semiquot.IsPure {α : Type u_1} (q : Semiquot α) :

Assert that a Semiquot contains only one possible value.

Equations

Semiquot.IsPure q = ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → a = b

def Semiquot.get {α : Type u_1} (q : Semiquot α) (h : Semiquot.IsPure q) :

α

Extract the value from a IsPure semiquotient.

Equations

Semiquot.get q h = Semiquot.liftOn q id h

theorem Semiquot.get_mem {α : Type u_1} {q : Semiquot α} (p : Semiquot.IsPure q) :

Semiquot.get q p ∈ q

theorem Semiquot.eq_pure {α : Type u_1} {q : Semiquot α} (p : Semiquot.IsPure q) :

q = pure (Semiquot.get q p)

@[simp]

theorem Semiquot.pure_isPure {α : Type u_1} (a : α) :

Semiquot.IsPure (pure a)

theorem Semiquot.isPure_iff {α : Type u_1} {s : Semiquot α} :

Semiquot.IsPure s ↔ ∃ a, s = pure a

theorem Semiquot.IsPure.mono {α : Type u_1} {s : Semiquot α} {t : Semiquot α} (st : s ≤ t) (h : Semiquot.IsPure t) :

Semiquot.IsPure s

theorem Semiquot.IsPure.min {α : Type u_1} {s : Semiquot α} {t : Semiquot α} (h : Semiquot.IsPure t) :

s ≤ t ↔ s = t

theorem Semiquot.isPure_of_subsingleton {α : Type u_1} [inst : Subsingleton α] (q : Semiquot α) :

Semiquot.IsPure q

def Semiquot.univ {α : Type u_1} [inst : Inhabited α] :

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

Equations

Semiquot.univ = Semiquot.mk (_ : default ∈ Set.univ)

instance Semiquot.instInhabitedSemiquot {α : Type u_1} [inst : Inhabited α] :

Inhabited (Semiquot α)

Equations

Semiquot.instInhabitedSemiquot = { default := Semiquot.univ }

@[simp]

theorem Semiquot.mem_univ {α : Type u_1} [inst : Inhabited α] (a : α) :

a ∈ Semiquot.univ

theorem Semiquot.univ_unique {α : Type u_1} (I : Inhabited α) (J : Inhabited α) :

Semiquot.univ = Semiquot.univ

@[simp]

theorem Semiquot.isPure_univ {α : Type u_1} [inst : Inhabited α] :

Semiquot.IsPure Semiquot.univ ↔ Subsingleton α

instance Semiquot.instOrderTopSemiquotInstLESemiquot {α : Type u_1} [inst : Inhabited α] :

OrderTop (Semiquot α)

Equations

Semiquot.instOrderTopSemiquotInstLESemiquot = OrderTop.mk (_ : ∀ (x : Semiquot α), x.s ⊆ Set.univ)