DEV Community

dev.to staff
dev.to staff

Posted on

Daily Challenge #168 - [Code golf] f (f (f b)) = f b

The kata is inspired by a Stack Overflow question.

It is easy to prove that f(f(f b)) = f b for all functions f : bool -> bool. But can you do it in less than 92 characters?

More specifically, your task is to prove the following lemma:

Lemma lemma : forall (f : bool -> bool) (b : bool), f (f (f b)) = f b.

And the size of your solution (including all declarations) should be 91 characters or less.


This challenge comes from monadius on CodeWars. Thank you to CodeWars, who has licensed redistribution of this challenge under the 2-Clause BSD License!

Want to propose a challenge idea for a future post? Email yo+challenge@dev.to with your suggestions!

Top comments (7)

Collapse
 
cattheory profile image
joomy

Here's my solution in Coq:

Lemma lemma : forall (f : bool -> bool) (b : bool), f (f (f b)) = f b.
intros;case b eqn:G,(f b) eqn:H,(f (f b)) eqn:I;rewrite G,H,I in*;intuition. Qed.

The second line has 80 characters.

Collapse
 
dwilmer profile image
Daan Wilmer • Edited

Not a code golfer, but pretty compact with writing the way I learned in uni:

f(x)=c → f(f(f(x)))=c=f(x)
f(x)=x → f(f(f(x)))=x=f(x)
f(x)=¬x → f(f(f(x)))=¬¬¬x=¬x=f(x)

Above code is 82 characters, excluding whitespace.

EDIT: now in LaTeX

f(x)=cf(f(f(x)))=c=f(x)f(x)=xf(f(f(x)))=x=f(x)f(x)=¬xf(f(f(x)))=¬¬¬x=¬x=f(x) \begin{aligned} f(x) = c &\rightarrow f(f(f(x))) = c = f(x) \\ f(x) = x &\rightarrow f(f(f(x))) = x = f(x) \\ f(x) = \neg x &\rightarrow f(f(f(x))) = \neg \neg \neg x = \neg x = f(x) \end{aligned}
Collapse
 
jose_a_alonso profile image
José A. Alonso

Another proof in Isabelle/HOL

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b; cases "f True"; cases "f False"; simp)
Collapse
 
jose_a_alonso profile image
José A. Alonso

In Isabelle/HOL

lemma "(f :: bool ⇒ bool) (f (f b)) = f b"
  by smt
Collapse
 
cattheory profile image
joomy

You have a typo in the lemma statement, f is applied twice instead of three times.

Collapse
 
jose_a_alonso profile image
José A. Alonso

In Isabelle/HOL equivalent to the above but with a different notation

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"
  by smt
Thread Thread
 
jose_a_alonso profile image
José A. Alonso

And with another notation

lemma 
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by smt