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.

• mk' :: (
• s : Set α

  Set containing some element of α

• val : Trunc ↑self.s

  Assertion of non-emptiness via Trunc

• )

instance Semiquot.instMembership {α : Type u_1} : Membership α (Semiquot α)

Equations

• Semiquot.instMembership = { mem := fun (q : Semiquot α) (a : α) => a ∈ q.s }

def Semiquot.mk {α : Type u_1} {a : α} {s : Set α} (h : a ∈ s) : Semiquot α

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

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

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

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

Replace s in a Semiquot with a superset.

Equations

• q.blur' h = { s := s, val := Trunc.lift (fun (a : ↑q.s) => Trunc.mk ⟨↑a, ⋯⟩) ⋯ q.val }

def Semiquot.blur {α : Type u_1} (s : Set α) (q : Semiquot α) : 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) : 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.ofTrunc {α : Type u_1} (q : Trunc α) : Semiquot α

Convert a Trunc α to a Semiquot α.

Equations

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

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

Convert a Semiquot α to a Trunc α.

Equations

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

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

• q.liftOn f h = q.val.liftOn (fun (x : ↑q.s) => f ↑x) ⋯

theorem Semiquot.liftOn_ofMem {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → β) (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b) (a : α) (aq : a ∈ q) : q.liftOn f h = f a

def Semiquot.map {α : Type u_1} {β : Type u_2} (f : α → β) (q : Semiquot α) : 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 : ↑q.s) => ⟨f ↑x, ⋯⟩) q.val }

@[simp]

theorem Semiquot.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) (q : Semiquot α) (b : β) : b ∈ map f q ↔ ∃ a ∈ q, f a = b

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

Apply a function returning a Semiquot to a Semiquot.

Equations

• q.bind f = { s := ⋃ a ∈ q.s, (f a).s, val := q.val.bind fun (a : ↑q.s) => Trunc.map (fun (b : ↑(f ↑a).s) => ⟨↑b, ⋯⟩) (f ↑a).val }

@[simp]

theorem Semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → Semiquot β) (b : β) : b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

instance Semiquot.instMonad : Monad Semiquot

Equations

• Semiquot.instMonad = Monad.mk

@[simp]

theorem Semiquot.map_def {α β : Type u_1} : (fun (x1 : α → β) (x2 : Semiquot α) => x1 <$> x2) = map

@[simp]

theorem Semiquot.bind_def {α β : Type u_1} : (fun (x1 : Semiquot α) (x2 : α → Semiquot β) => x1 >>= x2) = 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.instLawfulMonad : LawfulMonad Semiquot

instance Semiquot.instLE {α : Type u_1} : LE (Semiquot α)

Equations

• Semiquot.instLE = { le := fun (s t : Semiquot α) => s.s ⊆ t.s }

instance Semiquot.partialOrder {α : Type u_1} : PartialOrder (Semiquot α)

Equations

• Semiquot.partialOrder = PartialOrder.mk ⋯

instance Semiquot.instSemilatticeSup {α : Type u_1} : SemilatticeSup (Semiquot α)

Equations

• Semiquot.instSemilatticeSup = SemilatticeSup.mk (fun (s : Semiquot α) => Semiquot.blur s.s) ⋯ ⋯ ⋯

@[simp]

theorem Semiquot.pure_le {α : Type u_1} {a : α} {s : Semiquot α} : pure a ≤ s ↔ a ∈ s

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

Assert that a Semiquot contains only one possible value.

Equations

• q.IsPure = ∀ a ∈ q, ∀ b ∈ q, a = b

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

Extract the value from an IsPure semiquotient.

Equations

• q.get h = q.liftOn id h

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

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

@[simp]

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

theorem Semiquot.isPure_iff {α : Type u_1} {s : Semiquot α} : s.IsPure ↔ ∃ (a : α), s = pure a

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

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

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

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

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

Equations

• Semiquot.univ = Semiquot.mk ⋯

instance Semiquot.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Semiquot α)

Equations

• Semiquot.instInhabited = { default := Semiquot.univ }

@[simp]

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

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

@[simp]

theorem Semiquot.isPure_univ {α : Type u_1} [Inhabited α] : univ.IsPure ↔ Subsingleton α

instance Semiquot.instOrderTopOfInhabited {α : Type u_1} [Inhabited α] : OrderTop (Semiquot α)

Equations

• Semiquot.instOrderTopOfInhabited = OrderTop.mk ⋯