α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ Seq.IsBisimulation fun s1 s2 => flatten (Computation.pure s2) = s1
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ flatten (Computation.pure s) = s
refine' Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) _ rfl
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct s') (Seq.destruct s)
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ Seq.IsBisimulation fun s1 s2 => flatten (Computation.pure s2) = s1
intro s' s h
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s)))
    (Seq.destruct s)
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct s') (Seq.destruct s)
rw [← h]
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match Seq.destruct s with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    Seq.destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s)))
    (Seq.destruct s)
simp [flatten]
no goals
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match Seq.destruct s with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    Seq.destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
cases Seq.destruct s with
| none => simp
| some val =>
  cases' val with o s'
  simp
no goals
case none
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match none with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    none with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
simp
case some.mk
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
case some
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
val : Seq1 (Option α)
⊢ match
    match
      match some val with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some val with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
cases' val with o s'
no goals
case some.mk
α : Type u
β : Type v
γ : Type w
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match Computation.destruct c with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match Computation.destruct c with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
simp