mathlib3 documentation

data.semiquot

Semiquotients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

s : set α
val : trunc ↥(self.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 semiquot

@[protected, instance]

def semiquot.has_mem {α : Type u_1} :

has_mem α (semiquot α)

Equations

semiquot.has_mem = {mem := λ (a : α) (q : semiquot α), 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 ⟨a, h⟩}

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 = semiquot.mk h

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

semiquot.pure a = semiquot.mk _

@[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

q.blur' h = {s := s, val := trunc.lift (λ (a : ↥(q.s)), trunc.mk ⟨a.val, _⟩) _ q.val}

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 = q.blur' _

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

semiquot.blur s q = 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

semiquot.of_trunc q = {s := set.univ α, val := trunc.map (λ (a : α), ⟨a, trivial⟩) q}

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

Convert a semiquot α to a trunc α.

Equations

q.to_trunc = trunc.map subtype.val q.val

def semiquot.lift_on {α : 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.lift_on f is the value of f at any point of q.

Equations

q.lift_on f h = q.val.lift_on (λ (x : ↥(q.s)), f x.val) _

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

semiquot.map f q = {s := f '' q.s, val := trunc.map (λ (x : ↥(q.s)), ⟨f x.val, _⟩) 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

q.bind f = {s := ⋃ (a : α) (H : a ∈ q.s), (f a).s, val := q.val.bind (λ (a : ↥(q.s)), trunc.map (λ (b : ↥((f a.val).s)), ⟨b.val, _⟩) (f a.val).val)}

@[simp]

theorem semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → semiquot β) (b : β) :

b ∈ q.bind f ↔ ∃ (a : α) (H : a ∈ q), b ∈ f a

@[protected, instance]

def semiquot.monad :

Equations

semiquot.monad = monad.mk

@[simp]

theorem semiquot.map_def {α β : Type u_1} :

functor.map = semiquot.map

@[simp]

theorem semiquot.bind_def {α β : Type u_1} :

has_bind.bind = semiquot.bind

@[simp]

theorem semiquot.mem_pure {α : Type u_1} {a b : α} :

a ∈ has_pure.pure b ↔ a = b

theorem semiquot.mem_pure_self {α : Type u_1} (a : α) :

a ∈ has_pure.pure a

@[simp]

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

has_pure.pure a = has_pure.pure b ↔ a = b

@[protected, instance]

def semiquot.is_lawful_monad :

is_lawful_monad semiquot

@[protected, instance]

def semiquot.has_le {α : Type u_1} :

has_le (semiquot α)

Equations

semiquot.has_le = {le := λ (s t : semiquot α), s.s ⊆ t.s}

@[protected, instance]

def semiquot.partial_order {α : Type u_1} :

partial_order (semiquot α)

Equations

semiquot.partial_order = {le := λ (s t : semiquot α), ∀ ⦃x : α⦄, x ∈ s → x ∈ t, lt := preorder.lt._default (λ (s t : semiquot α), ∀ ⦃x : α⦄, x ∈ s → x ∈ t), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def semiquot.semilattice_sup {α : Type u_1} :

semilattice_sup (semiquot α)

Equations

semiquot.semilattice_sup = {sup := λ (s : semiquot α), semiquot.blur s.s, le := partial_order.le semiquot.partial_order, lt := partial_order.lt semiquot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

@[simp]

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

has_pure.pure a ≤ s ↔ a ∈ s

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

Prop

Assert that a semiquot contains only one possible value.

Equations

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

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

α

Extract the value from a is_pure semiquotient.

Equations

q.get h = q.lift_on id h

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) :

q = has_pure.pure (q.get p)

@[simp]

theorem semiquot.pure_is_pure {α : Type u_1} (a : α) :

(has_pure.pure a).is_pure

theorem semiquot.is_pure_iff {α : Type u_1} {s : semiquot α} :

s.is_pure ↔ ∃ (a : α), s = has_pure.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

semiquot.univ = semiquot.mk semiquot.univ._proof_1

@[protected, instance]

def semiquot.inhabited {α : Type u_1} [inhabited α] :

inhabited (semiquot α)

Equations

semiquot.inhabited = {default := semiquot.univ _inst_1}

@[simp]

theorem semiquot.mem_univ {α : Type u_1} [inhabited α] (a : α) :

a ∈ semiquot.univ

theorem semiquot.univ_unique {α : Type u_1} (I J : inhabited α) :

semiquot.univ = semiquot.univ

@[simp]

theorem semiquot.is_pure_univ {α : Type u_1} [inhabited α] :

semiquot.univ.is_pure ↔ subsingleton α

@[protected, instance]

def semiquot.order_top {α : Type u_1} [inhabited α] :

order_top (semiquot α)

Equations

semiquot.order_top = {top := semiquot.univ _inst_1, le_top := _}