α : Type u
β : Type v
γ : Type w
l : List α
s : WSeq α
s1 s2 : Computation (List α)
h :
  ∃ l' s,
    s1 =
        Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l' ++ l, s) ∧
      s2 =
        Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
          (Computation.corec
            (fun x =>
              match x with
              | (l, s) =>
                match Seq.destruct s with
                | none => Sum.inl (List.reverse l)
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct s1) (Computation.destruct s2)
α : Type u
β : Type v
γ : Type w
l : List α
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ l' s,
      c1 =
          Computation.corec
            (fun x =>
              match x with
              | (l, s) =>
                match Seq.destruct s with
                | none => Sum.inl (List.reverse l)
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l' ++ l, s) ∧
        c2 =
          Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
            (Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l', s))
intro s1 s2 h
case intro.intro
α : Type u
β : Type v
γ : Type w
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct s1) (Computation.destruct s2)
α : Type u
β : Type v
γ : Type w
l : List α
s : WSeq α
s1 s2 : Computation (List α)
h :
  ∃ l' s,
    s1 =
        Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l' ++ l, s) ∧
      s2 =
        Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
          (Computation.corec
            (fun x =>
              match x with
              | (l, s) =>
                match Seq.destruct s with
                | none => Sum.inl (List.reverse l)
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct s1) (Computation.destruct s2)
rcases h with ⟨l', s, h⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct
      (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s)))
    (Computation.destruct
      (Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))))
case intro.intro
α : Type u
β : Type v
γ : Type w
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct s1) (Computation.destruct s2)
rw [h.left, h.right]
case intro.intro.h2
α : Type u
β : Type v
γ : Type w
l : List α
s✝¹ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s✝ : WSeq α
h✝ :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s✝) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s✝))
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ ∃ l'_1 s_1,
    Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (a :: (l' ++ l), s) =
        Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l'_1 ++ l, s_1) ∧
      Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (a :: l', s)) =
        Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l'_1, s_1))

case intro.intro.h3
α : Type u
β : Type v
γ : Type w
l : List α
s✝¹ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s✝ : WSeq α
h✝ :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s✝) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s✝))
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, think s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', think s))
⊢ ∃ l'_1 s_1,
    Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l' ++ l, s) =
        Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l'_1 ++ l, s_1) ∧
      Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l', s)) =
        Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l'_1, s_1))
case intro.intro
α : Type u
β : Type v
γ : Type w
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))
⊢ Computation.BisimO
    (fun c1 c2 =>
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x =>
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl (List.reverse l)
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
              (Computation.corec
                (fun x =>
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl (List.reverse l)
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.destruct
      (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s)))
    (Computation.destruct
      (Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s))))
induction' s using WSeq.recOn with a s s <;> simp [toList, nil, cons, think, length]
no goals
case intro.intro.h2
α : Type u
β : Type v
γ : Type w
l : List α
s✝¹ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s✝ : WSeq α
h✝ :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s✝) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s✝))
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ ∃ l'_1 s_1,
    Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (a :: (l' ++ l), s) =
        Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l'_1 ++ l, s_1) ∧
      Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (a :: l', s)) =
        Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l'_1, s_1))
refine' ⟨a::l', s, _, _⟩ <;> simp
no goals
case intro.intro.h3
α : Type u
β : Type v
γ : Type w
l : List α
s✝¹ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s✝ : WSeq α
h✝ :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s✝) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s✝))
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl (List.reverse l)
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, think s) ∧
    s2 =
      Computation.map ((fun x x_1 => x ++ x_1) (List.reverse l))
        (Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl (List.reverse l)
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', think s))
⊢ ∃ l'_1 s_1,
    Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l' ++ l, s) =
        Computation.corec
          (fun x =>
            match Seq.destruct x.snd with
            | none => Sum.inl (List.reverse x.fst)
            | some (none, s') => Sum.inr (x.fst, s')
            | some (some a, s') => Sum.inr (a :: x.fst, s'))
          (l'_1 ++ l, s_1) ∧
      Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l', s)) =
        Computation.map (fun x => List.reverse l ++ x)
          (Computation.corec
            (fun x =>
              match Seq.destruct x.snd with
              | none => Sum.inl (List.reverse x.fst)
              | some (none, s') => Sum.inr (x.fst, s')
              | some (some a, s') => Sum.inr (a :: x.fst, s'))
            (l'_1, s_1))
refine' ⟨l', s, _, _⟩ <;> simp