foldr append

Stream: general

[Iocta]

The theorem works fine, assuming it says what I meant. But I'm stuck on the example.

import init.data.list.basic
import tactic.basic
import tactic.squeeze

variables {α β γ : Type}

open list

theorem finite_foldr_fusion
(f : α → β → β)
(g : α → γ → γ)
(h : β → γ)
(b : β)
(xs : list α)
(hh : ∀ (x : α) (y : β), h (f x y) = g x (h y)) :
h (foldr f b xs) = foldr g (h b) xs :=
list.rec_on xs
(show h (foldr f b nil) = foldr g (h b) nil, from rfl)
(λa as, assume H: h (foldr f b as) = foldr g (h b) as,
  show h (foldr f b (a :: as)) = foldr g (h b) (a :: as),
  from by rw [foldr, hh, foldr, H])


example (f : α → β → β) (e : β) (xs ys : list α) :
foldr f (foldr f e ys) xs = foldr f e (xs ++ ys) :=
begin
  apply finite_foldr_fusion f _ _ e xs _,
end



expected type:
αβ: Type
f: α → β → β
e: β
xsys: list α
⊢ ?m_2 (foldr f e xs) = _
Messages (1)
proofs01.lean:62:2
invalid apply tactic, failed to unify
  foldr f (foldr f e ys) xs = foldr f e (xs ++ ys)
with
  ?m_2 (foldr f e xs) = foldr ?m_3 (?m_2 e) xs
state:
5 goals
α β : Type,
f : α → β → β,
e : β,
xs ys : list α
⊢ foldr f (foldr f e ys) xs = foldr f e (xs ++ ys)

α β : Type,
f : α → β → β,
e : β,
xs ys : list α
⊢ Type

α β : Type,
f : α → β → β,
e : β,
xs ys : list α
⊢ α → ?m_1 → ?m_1

α β : Type,
f : α → β → β,
e : β,
xs ys : list α
⊢ β → ?m_1

α β : Type,
f : α → β → β,
e : β,
xs ys : list α
⊢ ∀ (x : α) (y : β), ?m_2 (f x y) = ?m_3 x (?m_2 y)

[Patrick Johnson]

Why do you need finite_foldr_fusion? Your example is just a symmetry version of foldr_append:

example (f : α → β → β) (e : β) (xs ys : list α) :
foldr f (foldr f e ys) xs = foldr f e (xs ++ ys) :=
by symmetry; apply foldr_append

[Iocta]

finite_foldr_fusion is supposed to be the general case and I want to try to apply it

[Yakov Pechersky]

docs#list.foldr_rec_on