Relations between and equivalence of weak sequences

This file defines a relation between weak sequences as a relation between their some elements, ignoring computation time (none elements). Equivalence is then defined in the obvious way.

Main definitions

• Stream'.WSeq.LiftRelO: Lift a relation to a relation over weak sequences.
• Stream'.WSeq.LiftRel: Two sequences are LiftRel R-related if their corresponding some elements are R-related.
• Stream'.WSeq.Equiv: Two sequences are equivalent if they are LiftRel (· = ·)-related.

def Stream'.WSeq.LiftRelO {α : Type u} {β : Type v} (R : α → β → Prop) (C : WSeq α → WSeq β → Prop) : Option (α × WSeq α) → Option (β × WSeq β) → Prop

lift a relation to a relation over weak sequences

Equations

• Stream'.WSeq.LiftRelO R C none none = True
• Stream'.WSeq.LiftRelO R C (some (a, s)) (some (b, t)) = (R a b ∧ C s t)
• Stream'.WSeq.LiftRelO R C x✝¹ x✝ = False

theorem Stream'.WSeq.LiftRelO.imp {α : Type u} {β : Type v} {R S : α → β → Prop} {C D : WSeq α → WSeq β → Prop} (H1 : ∀ (a : α) (b : β), R a b → S a b) (H2 : ∀ (s : WSeq α) (t : WSeq β), C s t → D s t) {o : Option (α × WSeq α)} {p : Option (β × WSeq β)} : LiftRelO R C o p → LiftRelO S D o p

theorem Stream'.WSeq.LiftRelO.imp_right {α : Type u} {β : Type v} (R : α → β → Prop) {C D : WSeq α → WSeq β → Prop} (H : ∀ (s : WSeq α) (t : WSeq β), C s t → D s t) {o : Option (α × WSeq α)} {p : Option (β × WSeq β)} : LiftRelO R C o p → LiftRelO R D o p

theorem Stream'.WSeq.LiftRelO.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : WSeq α → WSeq β → Prop) : Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)

def Stream'.WSeq.BisimO {α : Type u} (R : WSeq α → WSeq α → Prop) : Option (α × WSeq α) → Option (α × WSeq α) → Prop

Definition of bisimilarity for weak sequences

Equations

• Stream'.WSeq.BisimO R = Stream'.WSeq.LiftRelO (fun (x1 x2 : α) => x1 = x2) R

theorem Stream'.WSeq.BisimO.imp {α : Type u} {R S : WSeq α → WSeq α → Prop} (H : ∀ (s t : WSeq α), R s t → S s t) {o p : Option (α × WSeq α)} : BisimO R o p → BisimO S o p

def Stream'.WSeq.LiftRel {α : Type u} {β : Type v} (R : α → β → Prop) (s : WSeq α) (t : WSeq β) : Prop

Two weak sequences are LiftRel R related if they are either both empty, or they are both nonempty and the heads are R related and the tails are LiftRel R related. (This is a coinductive definition.)

Equations

• One or more equations did not get rendered due to their size.

theorem Stream'.WSeq.liftRel_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : WSeq α} {t : WSeq β} : LiftRel R s t → Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

theorem Stream'.WSeq.liftRel_destruct_iff {α : Type u} {β : Type v} {R : α → β → Prop} {s : WSeq α} {t : WSeq β} : LiftRel R s t ↔ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

theorem Stream'.WSeq.LiftRel.swap_lem {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : WSeq α} {s2 : WSeq β} (h : LiftRel R s1 s2) : LiftRel (Function.swap R) s2 s1

theorem Stream'.WSeq.LiftRel.swap {α : Type u} {β : Type v} (R : α → β → Prop) : Function.swap (LiftRel R) = LiftRel (Function.swap R)

theorem Stream'.WSeq.LiftRel.refl {α : Type u} (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R)

theorem Stream'.WSeq.LiftRel.symm {α : Type u} (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R)

theorem Stream'.WSeq.LiftRel.trans {α : Type u} (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R)

theorem Stream'.WSeq.LiftRel.equiv {α : Type u} (R : α → α → Prop) : Equivalence R → Equivalence (LiftRel R)

def Stream'.WSeq.Equiv {α : Type u} : WSeq α → WSeq α → Prop

If two sequences are equivalent, then they have the same values and the same computational behavior (i.e. if one loops forever then so does the other), although they may differ in the number of thinks needed to arrive at the answer.

Equations

• Stream'.WSeq.Equiv = Stream'.WSeq.LiftRel fun (x1 x2 : α) => x1 = x2

def Stream'.WSeq.«term_~ʷ_» : Lean.TrailingParserDescr

If two sequences are equivalent, then they have the same values and the same computational behavior (i.e. if one loops forever then so does the other), although they may differ in the number of thinks needed to arrive at the answer.

Equations

• Stream'.WSeq.«term_~ʷ_» = Lean.ParserDescr.trailingNode `Stream'.WSeq.«term_~ʷ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ʷ ") (Lean.ParserDescr.cat `term 51))

theorem Stream'.WSeq.Equiv.refl {α : Type u} (s : WSeq α) : s ~ʷ s

theorem Stream'.WSeq.Equiv.symm {α : Type u} {s t : WSeq α} : s ~ʷ t → t ~ʷ s

theorem Stream'.WSeq.Equiv.trans {α : Type u} {s t u : WSeq α} : s ~ʷ t → t ~ʷ u → s ~ʷ u

theorem Stream'.WSeq.Equiv.equivalence {α : Type u} : Equivalence Equiv

theorem Stream'.WSeq.destruct_congr {α : Type u} {s t : WSeq α} : s ~ʷ t → Computation.LiftRel (BisimO fun (x1 x2 : WSeq α) => x1 ~ʷ x2) s.destruct t.destruct

theorem Stream'.WSeq.destruct_congr_iff {α : Type u} {s t : WSeq α} : s ~ʷ t ↔ Computation.LiftRel (BisimO fun (x1 x2 : WSeq α) => x1 ~ʷ x2) s.destruct t.destruct

theorem Stream'.WSeq.liftRel_dropn_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : WSeq α} {t : WSeq β} (H : LiftRel R s t) (n : ℕ) : Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop n).destruct (t.drop n).destruct

theorem Stream'.WSeq.exists_of_liftRel_left {α : Type u} {β : Type v} {R : α → β → Prop} {s : WSeq α} {t : WSeq β} (H : LiftRel R s t) {a : α} (h : a ∈ s) : ∃ (b : β), b ∈ t ∧ R a b

theorem Stream'.WSeq.exists_of_liftRel_right {α : Type u} {β : Type v} {R : α → β → Prop} {s : WSeq α} {t : WSeq β} (H : LiftRel R s t) {b : β} (h : b ∈ t) : ∃ (a : α), a ∈ s ∧ R a b

@[simp]

theorem Stream'.WSeq.liftRel_nil {α : Type u} {β : Type v} (R : α → β → Prop) : LiftRel R nil nil

@[simp]

theorem Stream'.WSeq.liftRel_cons {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) (s : WSeq α) (t : WSeq β) : LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t

@[simp]

theorem Stream'.WSeq.liftRel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (s : WSeq α) (t : WSeq β) : LiftRel R s.think t ↔ LiftRel R s t

@[simp]

theorem Stream'.WSeq.liftRel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (s : WSeq α) (t : WSeq β) : LiftRel R s t.think ↔ LiftRel R s t

theorem Stream'.WSeq.cons_congr {α : Type u} {s t : WSeq α} (a : α) (h : s ~ʷ t) : cons a s ~ʷ cons a t

theorem Stream'.WSeq.think_equiv {α : Type u} (s : WSeq α) : s.think ~ʷ s

theorem Stream'.WSeq.think_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) : s.think ~ʷ t.think

theorem Stream'.WSeq.head_congr {α : Type u} {s t : WSeq α} : s ~ʷ t → s.head.Equiv t.head

theorem Stream'.WSeq.flatten_equiv {α : Type u} {c : Computation (WSeq α)} {s : WSeq α} (h : s ∈ c) : flatten c ~ʷ s

theorem Stream'.WSeq.liftRel_flatten {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : Computation (WSeq α)} {c2 : Computation (WSeq β)} (h : Computation.LiftRel (LiftRel R) c1 c2) : LiftRel R (flatten c1) (flatten c2)

theorem Stream'.WSeq.flatten_congr {α : Type u} {c1 c2 : Computation (WSeq α)} : Computation.LiftRel Equiv c1 c2 → flatten c1 ~ʷ flatten c2

theorem Stream'.WSeq.tail_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) : s.tail ~ʷ t.tail

theorem Stream'.WSeq.dropn_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) (n : ℕ) : s.drop n ~ʷ t.drop n

theorem Stream'.WSeq.get?_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) (n : ℕ) : (s.get? n).Equiv (t.get? n)

theorem Stream'.WSeq.mem_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) (a : α) : a ∈ s ↔ a ∈ t

theorem Stream'.WSeq.Equiv.ext {α : Type u} {s t : WSeq α} (h : ∀ (n : ℕ), (s.get? n).Equiv (t.get? n)) : s ~ʷ t

theorem Stream'.WSeq.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : WSeq α} {s2 : WSeq β} {f1 : α → γ} {f2 : β → δ} (h1 : LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) : LiftRel S (map f1 s1) (map f2 s2)

theorem Stream'.WSeq.map_congr {α : Type u} {β : Type v} (f : α → β) {s t : WSeq α} (h : s ~ʷ t) : map f s ~ʷ map f t

theorem Stream'.WSeq.liftRel_append {α : Type u} {β : Type v} (R : α → β → Prop) {s1 s2 : WSeq α} {t1 t2 : WSeq β} (h1 : LiftRel R s1 t1) (h2 : LiftRel R s2 t2) : LiftRel R (s1.append s2) (t1.append t2)

theorem Stream'.WSeq.liftRel_join.lem {α : Type u} {β : Type v} (R : α → β → Prop) {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} {U : WSeq α → WSeq β → Prop} (ST : LiftRel (LiftRel R) S T) (HU : ∀ (s1 : WSeq α) (s2 : WSeq β), (∃ (s : WSeq α), ∃ (t : WSeq β), ∃ (S : WSeq (WSeq α)), ∃ (T : WSeq (WSeq β)), s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2) {a : Option (α × WSeq α)} (ma : a ∈ S.join.destruct) : ∃ (b : Option (β × WSeq β)), b ∈ T.join.destruct ∧ LiftRelO R U a b

theorem Stream'.WSeq.liftRel_join {α : Type u} {β : Type v} (R : α → β → Prop) {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (h : LiftRel (LiftRel R) S T) : LiftRel R S.join T.join

theorem Stream'.WSeq.join_congr {α : Type u} {S T : WSeq (WSeq α)} (h : LiftRel Equiv S T) : S.join ~ʷ T.join

theorem Stream'.WSeq.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : WSeq α} {s2 : WSeq β} {f1 : α → WSeq γ} {f2 : β → WSeq δ} (h1 : LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → LiftRel S (f1 a) (f2 b)) : LiftRel S (s1.bind f1) (s2.bind f2)

theorem Stream'.WSeq.bind_congr {α : Type u} {β : Type v} {s1 s2 : WSeq α} {f1 f2 : α → WSeq β} (h1 : s1 ~ʷ s2) (h2 : ∀ (a : α), f1 a ~ʷ f2 a) : s1.bind f1 ~ʷ s2.bind f2

@[simp]

theorem Stream'.WSeq.join_ret {α : Type u} (s : WSeq α) : (ret s).join ~ʷ s

@[simp]

theorem Stream'.WSeq.join_map_ret {α : Type u} (s : WSeq α) : (map ret s).join ~ʷ s

@[simp]

theorem Stream'.WSeq.join_append {α : Type u} (S T : WSeq (WSeq α)) : (S.append T).join ~ʷ S.join.append T.join

@[simp]

theorem Stream'.WSeq.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : WSeq α) : s.bind (ret ∘ f) ~ʷ map f s

@[simp]

theorem Stream'.WSeq.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → WSeq β) : (ret a).bind f ~ʷ f a

@[simp]

theorem Stream'.WSeq.join_join {α : Type u} (SS : WSeq (WSeq (WSeq α))) : SS.join.join ~ʷ (map join SS).join

@[simp]

theorem Stream'.WSeq.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : WSeq α) (f : α → WSeq β) (g : β → WSeq γ) : (s.bind f).bind g ~ʷ s.bind fun (x : α) => (f x).bind g