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

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

  • )
Instances For
    instance Semiquot.instMembership {α : Type u_1} :
    Equations
    • Semiquot.instMembership = { mem := fun (q : Semiquot α) (a : α) => 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
    Instances For
      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 α) :
      q.s.Nonempty
      def Semiquot.pure {α : Type u_1} (a : α) :

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

      Equations
      Instances For
        @[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
        • q.blur' h = { s := s, val := Trunc.lift (fun (a : q.s) => Trunc.mk a, ) q.val }
        Instances For
          def Semiquot.blur {α : Type u_1} (s : Set α) (q : Semiquot α) :

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

          Equations
          Instances For
            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.ofTrunc {α : Type u_1} (q : Trunc α) :

            Convert a Trunc α to a Semiquot α.

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

              Convert a Semiquot α to a Trunc α.

              Equations
              Instances For
                def Semiquot.liftOn {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : αβ) (h : aq, bq, 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)
                Instances For
                  theorem Semiquot.liftOn_ofMem {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : αβ) (h : aq, bq, 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 α) :

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

                  Equations
                  Instances For
                    @[simp]
                    theorem Semiquot.mem_map {α : Type u_1} {β : Type u_2} (f : αβ) (q : Semiquot α) (b : β) :
                    b Semiquot.map f q aq, 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 := aq.s, (f a).s, val := q.val.bind fun (a : q.s) => Trunc.map (fun (b : (f a).s) => b, ) (f a).val }
                    Instances For
                      @[simp]
                      theorem Semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : αSemiquot β) (b : β) :
                      b q.bind f aq, b f a
                      @[simp]
                      theorem Semiquot.map_def {α : Type u_1} {β : Type u_1} :
                      (fun (x1 : αβ) (x2 : Semiquot α) => x1 <$> x2) = Semiquot.map
                      @[simp]
                      theorem Semiquot.bind_def {α : Type u_1} {β : Type u_1} :
                      (fun (x1 : Semiquot α) (x2 : αSemiquot β) => x1 >>= x2) = 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.instLE {α : Type u_1} :
                      Equations
                      • Semiquot.instLE = { le := fun (s t : Semiquot α) => s.s t.s }
                      Equations
                      Equations
                      @[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
                      • q.IsPure = aq, bq, a = b
                      Instances For
                        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
                        Instances For
                          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 : Semiquot α} {t : Semiquot α} (st : s t) (h : t.IsPure) :
                          s.IsPure
                          theorem Semiquot.IsPure.min {α : Type u_1} {s : Semiquot α} {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 α] :

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

                          Equations
                          Instances For
                            instance Semiquot.instInhabited {α : Type u_1} [Inhabited α] :
                            Equations
                            • Semiquot.instInhabited = { default := Semiquot.univ }
                            @[simp]
                            theorem Semiquot.mem_univ {α : Type u_1} [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} [Inhabited α] :
                            Semiquot.univ.IsPure Subsingleton α
                            Equations