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
    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) :
    theorem Semiquot.nonempty {α : Type u_1} (q : Semiquot α) :
    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 : α} :
    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
    theorem Semiquot.blur_eq_blur' {α : Type u_1} (q : Semiquot α) (s : Set α) (h : q.s s) :
    @[simp]
    theorem Semiquot.mem_blur' {α : Type u_1} (q : Semiquot α) {s : Set α} (h : q.s s) {a : α} :
    def Semiquot.ofTrunc {α : Type u_1} (q : Trunc α) :

    Convert a Trunc α to a Semiquot α.

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

    Convert a Semiquot α to a Trunc α.

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

    Equations
    theorem Semiquot.liftOn_ofMem {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : αβ) (h : ∀ (a : α), a q∀ (b : α), b qf 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
    @[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
    @[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} :
    Equations
    • Semiquot.instLESemiquot = { le := fun s t => s.s t.s }
    Equations
    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
    def Semiquot.get {α : Type u_1} (q : Semiquot α) (h : Semiquot.IsPure q) :
    α

    Extract the value from a IsPure semiquotient.

    Equations
    theorem Semiquot.get_mem {α : Type u_1} {q : Semiquot α} (p : Semiquot.IsPure q) :
    theorem Semiquot.eq_pure {α : Type u_1} {q : Semiquot α} (p : Semiquot.IsPure q) :
    @[simp]
    theorem Semiquot.pure_isPure {α : Type u_1} (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) :
    theorem Semiquot.IsPure.min {α : Type u_1} {s : Semiquot α} {t : Semiquot α} (h : Semiquot.IsPure t) :
    s t s = t
    def Semiquot.univ {α : Type u_1} [inst : Inhabited α] :

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

    Equations
    instance Semiquot.instInhabitedSemiquot {α : Type u_1} [inst : Inhabited α] :
    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 α] :
    Equations