Search code examples
lean

How to do cases on a function between finite types?

I'm just starting out with lean.

Say I want to prove something about functions between two finite types. For example

example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := sorry

since there are just a few possibilities for f ideally I'd want something like cases x <;> cases f <;> rfl, but I can't do cases f.

Currently, I don't know how to prove this at all, I'd think cases/match on (f false) and (f true) but lean doesn't seem to remember this information about the function once it goes into the case.

Solution

  • Here's a proof along your original lines (not dec_trivial), note we use the h : syntax to name the case hypothesis:

    example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := 
by
  intro x
  cases x <;>
  cases h : f true <;>
  cases h2 : f false <;>
  simp [h, h2]