pattern matching prevents `refl` proof from working

Stream: new members

[David Renshaw]

How can I prove the break_into_words_def lemma below? It works if I redefine everything to not use pattern matching, but I would prefer not to do that.

import data.stream.defs

variable {α : Type}

-- I want to be able to rewrite applications of this function.
-- I expect to be able to use `refl` to reduce it.

def break_into_words :
   (stream ℕ) → -- word lengths
   (stream α) → -- original sequence
   (stream (list α)) -- sequence of words
 := function.curry
     (stream.corec
       (λ ⟨lengths, a'⟩, stream.take (lengths.head) a')
       (λ ⟨lengths, a'⟩, ⟨lengths.tail, stream.drop (lengths.head) a'⟩))

#eval (stream.take 4 (break_into_words id id))
-- [[], [0], [1, 2], [3, 4, 5]]

lemma break_into_words_def
    (b : stream ℕ)
    (a : stream α)
    (n : ℕ)
   : break_into_words b a n =
    ((λ ⟨lengths, a'⟩, stream.take (lengths.head) a') : stream ℕ × stream α → list α)
    ((@stream.iterate (stream ℕ × stream α) (λ ⟨lengths, a'⟩,
                     ⟨lengths.tail, stream.drop (lengths.head) a'⟩) ⟨b,a⟩) n) :=
begin
  refl -- I expect this to work, but it does not.
end


-- If I don't use any pattern matching, then it works as expected:

def break_into_words' :
   (stream ℕ) → -- word lengths
   (stream α) → -- original sequence
   (stream (list α)) -- sequence of words
 := function.curry
     (stream.corec
       (λ x, stream.take (x.fst.head) x.snd)
       (λ x, ⟨x.fst.tail, stream.drop (x.fst.head) x.snd⟩))

#eval (stream.take 4 (break_into_words' id id))
-- [[], [0], [1, 2], [3, 4, 5]]

lemma break_into_words_def'
    (b : stream ℕ)
    (a : stream α)
    (n : ℕ)
   : break_into_words' b a n =
    ((λ x, stream.take (x.fst.head) x.snd) : stream ℕ × stream α → list α)
    ((@stream.iterate (stream ℕ × stream α) (λ x,
                     ⟨x.fst.tail, stream.drop (x.fst.head) x.snd⟩) ⟨b,a⟩) n) :=
begin
  refl -- does work
end

[Kyle Miller]

One trick is to do cases on the arguments that participate in pattern matching first. This can "unstick" the reduction involved in a refl proof. (I haven't checked if it works here.)

[Kyle Miller]

Oh, this doesn't seem to apply here, sorry.

[Patrick Johnson]

lemma break_into_words_def
  (b : stream ℕ)
  (a : stream α)
  (n : ℕ) :
  break_into_words b a n =
  ((λ ⟨lengths, a'⟩, stream.take (lengths.head) a') :
  stream ℕ × stream α → list α)
  ((@stream.iterate (stream ℕ × stream α) (λ ⟨lengths, a'⟩,
  ⟨lengths.tail, stream.drop (lengths.head) a'⟩) ⟨b, a⟩) n) :=
begin
  convert_to
    (function.curry (stream.corec
    (λ x, stream.take (x.fst.head) x.snd)
    (λ x, ⟨x.fst.tail, stream.drop (x.fst.head) x.snd⟩)) :
    stream ℕ → stream α → stream (list α)) b a n =
    (((λ x, stream.take (x.fst.head) x.snd) : stream ℕ × stream α → list α)
    ((@stream.iterate (stream ℕ × stream α) (λ x,
    ⟨x.fst.tail, stream.drop (x.fst.head) x.snd⟩) ⟨b, a⟩) n)),
  { rw break_into_words, congr; ext ⟨a, b⟩; refl },
  { simp_rw prod_rec },
  refl,
end

[David Renshaw]

@Patrick Johnson what is prod_rec? I don't see that anywhere in mathlib or core lean.

[Patrick Johnson]

Sorry, I edited the post, but that lemma somehow disappeared. Fixed.

[David Renshaw]

Thanks!

[David Renshaw]

I still don't understand why this isn't a direct definitional equality, though.