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 [e-mail] with your suggestions!

Comments

[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.

[Daan Wilmer]

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

$\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}$

[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)

[José A. Alonso]

In Isabelle/HOL

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

[joomy]

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

[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

[José A. Alonso]

And with another notation

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