Documentation

Mathlib.Data.Seq.Computation

Coinductive formalization of unbounded computations. #

This file provides a Computation type where Computation α is the type of unbounded computations returning α.

def Computation (α : Type u) :

Computation α is the type of unbounded computations returning α. An element of Computation α is an infinite sequence of Option α such that if f n = some a for some n then it is constantly some a after that.

Equations
Instances For
    def Computation.pure {α : Type u} (a : α) :

    pure a is the computation that immediately terminates with result a.

    Equations
    Instances For
      Equations
      • Computation.instCoeTCComputation = { coe := Computation.pure }
      def Computation.think {α : Type u} (c : Computation α) :

      think c is the computation that delays for one "tick" and then performs computation c.

      Equations
      Instances For
        def Computation.thinkN {α : Type u} (c : Computation α) :

        thinkN c n is the computation that delays for n ticks and then performs computation c.

        Equations
        Instances For
          def Computation.head {α : Type u} (c : Computation α) :

          head c is the first step of computation, either some a if c = pure a or none if c = think c'.

          Equations
          Instances For
            def Computation.tail {α : Type u} (c : Computation α) :

            tail c is the remainder of computation, either c if c = pure a or c' if c = think c'.

            Equations
            Instances For

              empty α is the computation that never returns, an infinite sequence of thinks.

              Equations
              Instances For
                Equations
                def Computation.runFor {α : Type u} :
                Computation αOption α

                runFor c n evaluates c for n steps and returns the result, or none if it did not terminate after n steps.

                Equations
                • Computation.runFor = Subtype.val
                Instances For
                  def Computation.destruct {α : Type u} (c : Computation α) :

                  destruct c is the destructor for Computation α as a coinductive type. It returns inl a if c = pure a and inr c' if c = think c'.

                  Equations
                  Instances For
                    unsafe def Computation.run {α : Type u} :
                    Computation αα

                    run c is an unsound meta function that runs c to completion, possibly resulting in an infinite loop in the VM.

                    Equations
                    Instances For
                      @[simp]
                      def Computation.recOn {α : Type u} {C : Computation αSort v} (s : Computation α) (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C (Computation.think s)) :
                      C s

                      Recursion principle for computations, compare with List.recOn.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Computation.Corec.f {α : Type u} {β : Type v} (f : βα β) :
                        α βOption α × (α β)

                        Corecursor constructor for corec

                        Equations
                        Instances For
                          def Computation.corec {α : Type u} {β : Type v} (f : βα β) (b : β) :

                          corec f b is the corecursor for Computation α as a coinductive type. If f b = inl a then corec f b = pure a, and if f b = inl b' then corec f b = think (corec f b').

                          Equations
                          Instances For
                            def Computation.lmap {α : Type u} {β : Type v} {γ : Type w} (f : αβ) :
                            α γβ γ

                            left map of

                            Equations
                            Instances For
                              def Computation.rmap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
                              α βα γ

                              right map of

                              Equations
                              Instances For
                                @[simp]
                                theorem Computation.corec_eq {α : Type u} {β : Type v} (f : βα β) (b : β) :
                                def Computation.BisimO {α : Type u} (R : Computation αComputation αProp) :
                                α Computation αα Computation αProp

                                Bisimilarity over a sum of Computations

                                Equations
                                Instances For

                                  Attribute expressing bisimilarity over two Computations

                                  Equations
                                  Instances For
                                    theorem Computation.eq_of_bisim {α : Type u} (R : Computation αComputation αProp) (bisim : Computation.IsBisimulation R) {s₁ : Computation α} {s₂ : Computation α} (r : R s₁ s₂) :
                                    s₁ = s₂
                                    def Computation.Mem {α : Type u} (a : α) (s : Computation α) :

                                    Assertion that a Computation limits to a given value

                                    Equations
                                    Instances For
                                      Equations
                                      • Computation.instMembershipComputation = { mem := Computation.Mem }
                                      theorem Computation.le_stable {α : Type u} (s : Computation α) {a : α} {m : } {n : } (h : m n) :
                                      s m = some as n = some a
                                      theorem Computation.mem_unique {α : Type u} {s : Computation α} {a : α} {b : α} :
                                      a sb sa = b
                                      theorem Computation.Mem.left_unique {α : Type u} :
                                      Relator.LeftUnique fun (x : α) (x_1 : Computation α) => x x_1
                                      class Computation.Terminates {α : Type u} (s : Computation α) :

                                      Terminates s asserts that the computation s eventually terminates with some value.

                                      • term : ∃ (a : α), a s

                                        assertion that there is some term a such that the Computation terminates

                                      Instances
                                        theorem Computation.terminates_iff {α : Type u} (s : Computation α) :
                                        Computation.Terminates s ∃ (a : α), a s
                                        theorem Computation.terminates_of_mem {α : Type u} {s : Computation α} {a : α} (h : a s) :
                                        theorem Computation.ret_mem {α : Type u} (a : α) :
                                        theorem Computation.eq_of_pure_mem {α : Type u} {a : α} {a' : α} (h : a' Computation.pure a) :
                                        a' = a
                                        Equations
                                        • =
                                        theorem Computation.think_mem {α : Type u} {s : Computation α} {a : α} :
                                        theorem Computation.of_think_mem {α : Type u} {s : Computation α} {a : α} :
                                        theorem Computation.thinkN_mem {α : Type u} {s : Computation α} {a : α} (n : ) :
                                        def Computation.Promises {α : Type u} (s : Computation α) (a : α) :

                                        Promises s a, or s ~> a, asserts that although the computation s may not terminate, if it does, then the result is a.

                                        Equations
                                        Instances For

                                          Promises s a, or s ~> a, asserts that although the computation s may not terminate, if it does, then the result is a.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem Computation.mem_promises {α : Type u} {s : Computation α} {a : α} :

                                            length s gets the number of steps of a terminating computation

                                            Equations
                                            Instances For
                                              def Computation.get {α : Type u} (s : Computation α) [h : Computation.Terminates s] :
                                              α

                                              get s returns the result of a terminating computation

                                              Equations
                                              Instances For
                                                theorem Computation.get_eq_of_mem {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} :
                                                a sComputation.get s = a
                                                theorem Computation.mem_of_get_eq {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} :
                                                Computation.get s = aa s
                                                theorem Computation.mem_of_promises {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} (p : Computation.Promises s a) :
                                                a s
                                                def Computation.Results {α : Type u} (s : Computation α) (a : α) (n : ) :

                                                Results s a n completely characterizes a terminating computation: it asserts that s terminates after exactly n steps, with result a.

                                                Equations
                                                Instances For
                                                  theorem Computation.Results.mem {α : Type u} {s : Computation α} {a : α} {n : } :
                                                  Computation.Results s a na s
                                                  theorem Computation.Results.val_unique {α : Type u} {s : Computation α} {a : α} {b : α} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results s b n) :
                                                  a = b
                                                  theorem Computation.Results.len_unique {α : Type u} {s : Computation α} {a : α} {b : α} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results s b n) :
                                                  m = n
                                                  theorem Computation.exists_results_of_mem {α : Type u} {s : Computation α} {a : α} (h : a s) :
                                                  ∃ (n : ), Computation.Results s a n
                                                  @[simp]
                                                  theorem Computation.results_think {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results s a n) :
                                                  theorem Computation.of_results_think {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results (Computation.think s) a n) :
                                                  ∃ (m : ), Computation.Results s a m n = m + 1
                                                  @[simp]
                                                  theorem Computation.results_thinkN {α : Type u} {s : Computation α} {a : α} {m : } (n : ) :
                                                  theorem Computation.eq_thinkN {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results s a n) :
                                                  def Computation.memRecOn {α : Type u} {C : Computation αSort v} {a : α} {s : Computation α} (M : a s) (h1 : C (Computation.pure a)) (h2 : (s : Computation α) → C sC (Computation.think s)) :
                                                  C s

                                                  Recursor based on membership

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Computation.terminatesRecOn {α : Type u} {C : Computation αSort v} (s : Computation α) [Computation.Terminates s] (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C sC (Computation.think s)) :
                                                    C s

                                                    Recursor based on assertion of Terminates

                                                    Equations
                                                    Instances For
                                                      def Computation.map {α : Type u} {β : Type v} (f : αβ) :

                                                      Map a function on the result of a computation.

                                                      Equations
                                                      Instances For
                                                        def Computation.Bind.g {α : Type u} {β : Type v} :

                                                        bind over a Sum of Computation

                                                        Equations
                                                        Instances For
                                                          def Computation.Bind.f {α : Type u} {β : Type v} (f : αComputation β) :

                                                          bind over a function mapping α to a Computation

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def Computation.bind {α : Type u} {β : Type v} (c : Computation α) (f : αComputation β) :

                                                            Compose two computations into a monadic bind operation.

                                                            Equations
                                                            Instances For
                                                              theorem Computation.has_bind_eq_bind {α : Type u} {β : Type u} (c : Computation α) (f : αComputation β) :

                                                              Flatten a computation of computations into a single computation.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Computation.map_pure {α : Type u} {β : Type v} (f : αβ) (a : α) :
                                                                @[simp]
                                                                theorem Computation.map_think {α : Type u} {β : Type v} (f : αβ) (s : Computation α) :
                                                                @[simp]
                                                                theorem Computation.map_id {α : Type u} (s : Computation α) :
                                                                theorem Computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : Computation α) :
                                                                @[simp]
                                                                theorem Computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : αComputation β) :
                                                                @[simp]
                                                                theorem Computation.bind_pure {α : Type u} {β : Type v} (f : αβ) (s : Computation α) :
                                                                Computation.bind s (Computation.pure f) = Computation.map f s
                                                                @[simp]
                                                                theorem Computation.bind_pure' {α : Type u} (s : Computation α) :
                                                                Computation.bind s Computation.pure = s
                                                                @[simp]
                                                                theorem Computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : αComputation β) (g : βComputation γ) :
                                                                theorem Computation.results_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results (f a) b n) :
                                                                theorem Computation.mem_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} (h1 : a s) (h2 : b f a) :
                                                                theorem Computation.of_results_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {b : β} {k : } :
                                                                Computation.Results (Computation.bind s f) b k∃ (a : α), ∃ (m : ), ∃ (n : ), Computation.Results s a m Computation.Results (f a) b n k = n + m
                                                                theorem Computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {b : β} (h : b Computation.bind s f) :
                                                                ∃ (a : α), a s b f a
                                                                theorem Computation.bind_promises {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} (h1 : Computation.Promises s a) (h2 : Computation.Promises (f a) b) :
                                                                theorem Computation.has_map_eq_map {α : Type u} {β : Type u} (f : αβ) (c : Computation α) :
                                                                @[simp]
                                                                theorem Computation.pure_def {α : Type u} (a : α) :
                                                                @[simp]
                                                                theorem Computation.map_pure' {α : Type u_1} {β : Type u_1} (f : αβ) (a : α) :
                                                                @[simp]
                                                                theorem Computation.map_think' {α : Type u_1} {β : Type u_1} (f : αβ) (s : Computation α) :
                                                                theorem Computation.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Computation α} (m : a s) :
                                                                theorem Computation.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Computation α} (h : b Computation.map f s) :
                                                                ∃ (a : α), a s f a = b
                                                                Equations
                                                                • =
                                                                def Computation.orElse {α : Type u} (c₁ : Computation α) (c₂ : UnitComputation α) :

                                                                c₁ <|> c₂ calculates c₁ and c₂ simultaneously, returning the first one that gives a result.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : Computation α) :
                                                                  @[simp]
                                                                  theorem Computation.orElse_pure {α : Type u} (c₁ : Computation α) (a : α) :
                                                                  @[simp]
                                                                  theorem Computation.orElse_think {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :
                                                                  @[simp]
                                                                  theorem Computation.empty_orElse {α : Type u} (c : Computation α) :
                                                                  (HOrElse.hOrElse (Computation.empty α) fun (x : Unit) => c) = c
                                                                  @[simp]
                                                                  theorem Computation.orElse_empty {α : Type u} (c : Computation α) :
                                                                  (HOrElse.hOrElse c fun (x : Unit) => Computation.empty α) = c
                                                                  def Computation.Equiv {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :

                                                                  c₁ ~ c₂ asserts that c₁ and c₂ either both terminate with the same result, or both loop forever.

                                                                  Equations
                                                                  Instances For

                                                                    equivalence relation for computations

                                                                    Equations
                                                                    Instances For
                                                                      theorem Computation.Equiv.equivalence {α : Type u} :
                                                                      Equivalence Computation.Equiv
                                                                      theorem Computation.equiv_of_mem {α : Type u} {s : Computation α} {t : Computation α} {a : α} (h1 : a s) (h2 : a t) :
                                                                      theorem Computation.promises_congr {α : Type u} {c₁ : Computation α} {c₂ : Computation α} (h : Computation.Equiv c₁ c₂) (a : α) :
                                                                      theorem Computation.bind_congr {α : Type u} {β : Type v} {s1 : Computation α} {s2 : Computation α} {f1 : αComputation β} {f2 : αComputation β} (h1 : Computation.Equiv s1 s2) (h2 : ∀ (a : α), Computation.Equiv (f1 a) (f2 a)) :
                                                                      def Computation.LiftRel {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :

                                                                      LiftRel R ca cb is a generalization of Equiv to relations other than equality. It asserts that if ca terminates with a, then cb terminates with some b such that R a b, and if cb terminates with b then ca terminates with some a such that R a b.

                                                                      Equations
                                                                      Instances For
                                                                        theorem Computation.LiftRel.swap {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :
                                                                        theorem Computation.lift_eq_iff_equiv {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :
                                                                        Computation.LiftRel (fun (x x_1 : α) => x = x_1) c₁ c₂ Computation.Equiv c₁ c₂
                                                                        theorem Computation.LiftRel.refl {α : Type u} (R : ααProp) (H : Reflexive R) :
                                                                        theorem Computation.LiftRel.symm {α : Type u} (R : ααProp) (H : Symmetric R) :
                                                                        theorem Computation.LiftRel.trans {α : Type u} (R : ααProp) (H : Transitive R) :
                                                                        theorem Computation.LiftRel.imp {α : Type u} {β : Type v} {R : αβProp} {S : αβProp} (H : ∀ {a : α} {b : β}, R a bS a b) (s : Computation α) (t : Computation β) :
                                                                        theorem Computation.rel_of_liftRel {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} :
                                                                        Computation.LiftRel R ca cb∀ {a : α} {b : β}, a cab cbR a b
                                                                        theorem Computation.liftRel_of_mem {α : Type u} {β : Type v} {R : αβProp} {a : α} {b : β} {ca : Computation α} {cb : Computation β} (ma : a ca) (mb : b cb) (ab : R a b) :
                                                                        theorem Computation.exists_of_liftRel_left {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} (H : Computation.LiftRel R ca cb) {a : α} (h : a ca) :
                                                                        ∃ (b : β), b cb R a b
                                                                        theorem Computation.exists_of_liftRel_right {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} (H : Computation.LiftRel R ca cb) {b : β} (h : b cb) :
                                                                        ∃ (a : α), a ca R a b
                                                                        theorem Computation.liftRel_def {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} :
                                                                        Computation.LiftRel R ca cb (Computation.Terminates ca Computation.Terminates cb) ∀ {a : α} {b : β}, a cab cbR a b
                                                                        theorem Computation.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : Computation α} {s2 : Computation β} {f1 : αComputation γ} {f2 : βComputation δ} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bComputation.LiftRel S (f1 a) (f2 b)) :
                                                                        @[simp]
                                                                        theorem Computation.liftRel_pure_left {α : Type u} {β : Type v} (R : αβProp) (a : α) (cb : Computation β) :
                                                                        Computation.LiftRel R (Computation.pure a) cb ∃ (b : β), b cb R a b
                                                                        @[simp]
                                                                        theorem Computation.liftRel_pure_right {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (b : β) :
                                                                        Computation.LiftRel R ca (Computation.pure b) ∃ (a : α), a ca R a b
                                                                        @[simp]
                                                                        theorem Computation.liftRel_pure {α : Type u} {β : Type v} (R : αβProp) (a : α) (b : β) :
                                                                        @[simp]
                                                                        theorem Computation.liftRel_think_left {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :
                                                                        @[simp]
                                                                        theorem Computation.liftRel_think_right {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :
                                                                        theorem Computation.liftRel_mem_cases {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} (Ha : ∀ (a : α), a caComputation.LiftRel R ca cb) (Hb : ∀ (b : β), b cbComputation.LiftRel R ca cb) :
                                                                        theorem Computation.liftRel_congr {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {ca' : Computation α} {cb : Computation β} {cb' : Computation β} (ha : Computation.Equiv ca ca') (hb : Computation.Equiv cb cb') :
                                                                        theorem Computation.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : Computation α} {s2 : Computation β} {f1 : αγ} {f2 : βδ} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bS (f1 a) (f2 b)) :
                                                                        theorem Computation.map_congr {α : Type u} {β : Type v} {s1 : Computation α} {s2 : Computation α} {f : αβ} (h1 : Computation.Equiv s1 s2) :
                                                                        def Computation.LiftRelAux {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) :
                                                                        α Computation αβ Computation βProp

                                                                        Alternate definition of LiftRel over relations between Computations

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Computation.liftRelAux_inl_inl :
                                                                          ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {a : α} {b : α_1}, Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
                                                                          @[simp]
                                                                          theorem Computation.liftRelAux_inl_inr :
                                                                          ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {a : α} {cb : Computation α_1}, Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ (b : α_1), b cb R a b
                                                                          @[simp]
                                                                          theorem Computation.liftRelAux_inr_inl :
                                                                          ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {b : α_1} {ca : Computation α}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ (a : α), a ca R a b
                                                                          @[simp]
                                                                          theorem Computation.liftRelAux_inr_inr :
                                                                          ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {ca : Computation α} {cb : Computation α_1}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
                                                                          @[simp]
                                                                          theorem Computation.LiftRelAux.ret_left {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) (a : α) (cb : Computation β) :
                                                                          Computation.LiftRelAux R C (Sum.inl a) (Computation.destruct cb) ∃ (b : β), b cb R a b
                                                                          theorem Computation.LiftRelAux.swap {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) (a : α Computation α) (b : β Computation β) :
                                                                          @[simp]
                                                                          theorem Computation.LiftRelAux.ret_right {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) (b : β) (ca : Computation α) :
                                                                          Computation.LiftRelAux R C (Computation.destruct ca) (Sum.inl b) ∃ (a : α), a ca R a b
                                                                          theorem Computation.LiftRelRec.lem {α : Type u} {β : Type v} {R : αβProp} (C : Computation αComputation βProp) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cbComputation.LiftRelAux R C (Computation.destruct ca) (Computation.destruct cb)) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) (a : α) (ha : a ca) :
                                                                          theorem Computation.liftRel_rec {α : Type u} {β : Type v} {R : αβProp} (C : Computation αComputation βProp) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cbComputation.LiftRelAux R C (Computation.destruct ca) (Computation.destruct cb)) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) :