5 ms·
You can solve this by working backwards from the outside in, replacing a (b x) with c a b x wherever you can (not inside out, or else you get into an infinite l
by Icy0 2y ago
You can solve this by working backwards from the outside in, replacing a (b x) with c a b x wherever you can (not inside out, or else you get into an infinite loop!)
A cute alternative expression to solve the curried composition puzzle is c c c c c, just 5 c's in a row :)
Finally, Lean is a great language to do these puzzles in. See the following code:
/-- Compose! -/
def c (g : β → γ) (f : α → β) := g ∘ f
/-
?f (?g (?h ?x))
-/
#reduce c (c c) c ?f ?g ?h ?x
/-
?f (?g (?h ?x))
-/
#reduce c c c c c ?f ?g ?h ?x
- kmill 2y agoI used Lean too earlier today :-) I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution. May as well include a formalized proof while we're at it: def c (g : β → γ) (f : α → β) (x : α) : γ := g (f x) example (h : γ → δ) (g : β → γ) (f : α → β) (x : α) : h (g (f x)) = (c (c c) c) h g f x := rfl -- Or example : (fun (h : γ → δ) (g : β → γ) (f : α → β) (x : α) => h (g (f x))) = (c (c c) c) := rfl