cases' in Data/Seq/Seq

Stream: mathlib4

[Jeremy Tan]

@Johan Commelin complained about my replacement of cases' in #22079 with respect to Data.Seq.Seq, because the replacement was significantly longer.

-- If two streams are bisimilar, then they are equal
theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ := by
  apply Subtype.eq
  apply Stream'.eq_of_bisim fun x y => ∃ s s' : Seq α, s.1 = x ∧ s'.1 = y ∧ R s s'
  · dsimp [Stream'.IsBisimulation]
    intro t₁ t₂ e
    exact
    match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ => by
      suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
          by cases s' using Subtype.recOn; rfl, r⟩) this
      have := bisim r; revert r this
      cases s with
      | nil =>
        cases s' with
        | nil =>
          intro r _
          constructor
          · rfl
          · assumption
        | cons x' s' =>
          intro _ this
          rw [destruct_nil, destruct_cons] at this
          exact False.elim this
      | cons x s =>
        cases s' with
        | nil =>
          intro _ this
          rw [destruct_nil, destruct_cons] at this
          exact False.elim this
        | cons x' s' =>
          intro _ this
          rw [destruct_cons, destruct_cons] at this
          rw [head_cons, head_cons, tail_cons, tail_cons]
          obtain ⟨h1, h2⟩ := this
          constructor
          · rw [h1]
          · exact h2
  · exact ⟨s₁, s₂, rfl, rfl, r⟩

But the one-line replacements for cases' (rcases and obtain), I can't get them to work. What do I do?

[Aaron Liu]

You can use case:

-- If two streams are bisimilar, then they are equal
theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ := by
  apply Subtype.eq
  apply Stream'.eq_of_bisim fun x y => ∃ s s' : Seq α, s.1 = x ∧ s'.1 = y ∧ R s s'
  · dsimp [Stream'.IsBisimulation]
    intro t₁ t₂ e
    exact
    match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ => by
      suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
          by cases s' using Subtype.recOn; rfl, r⟩) this
      have := bisim r; revert r this
      cases s <;> cases s'
      case nil.nil => exact fun r _ => ⟨rfl, r⟩
      case nil.cons | cons.nil =>
        intro _ this
        rw [destruct_nil, destruct_cons] at this
        exact False.elim this
      case cons.cons =>
        intro _ this
        rw [destruct_cons, destruct_cons] at this
        rw [head_cons, head_cons, tail_cons, tail_cons]
        obtain ⟨h1, h2⟩ := this
        constructor
        · rw [h1]
        · exact h2
  · exact ⟨s₁, s₂, rfl, rfl, r⟩

It turns out we don't actually need to name the introduced variables either.

[Jeremy Tan]

#22079 has been updated with this fix

[Eric Wieser]

Does match work here too?

[Jeremy Tan]

Eric Wieser said:

Does match work here too?

No?