Unfold cases tactic #

In Lean, pattern matching expressions are not atomic parts of the syntax, but rather they are compiled down into simpler terms that are later checked by the kernel.

This allows Lean to have a minimalistic kernel but can occasionally lead an explosion of cases that need to be considered. What looks like one case in the match expression can in fact be compiled into many different cases that all need to proved by case analysis.

This tactic automates the process by allowing us to write down an equation f x = y where we know that f x = y is provably true, but does not hold definitionally. In that case the unfold_cases tactic will continue unfolding f and introducing cases where necessary until the left hand side becomes definitionally equal to the right hand side.

Consider a definition as follows:

def myand : bool → bool → bool
| ff _ := ff
| _ ff := ff
| _ _ := tt

The equation compiler generates 4 equation lemmas for us:

myand ff ff = ff
myand ff tt = ff
myand tt ff = ff
myand tt tt = tt

This is not in line with what one might expect looking at the definition. Whilst it is provably true, that ∀ x, myand ff x = ff and ∀ x, myand x ff = ff, we do not get these stronger lemmas from the compiler for free but must in fact prove them using cases or some other local reasoning.

In other words, the following does not constitute a proof that lean accepts.

example : ∀ x, myand ff x = ff :=
begin
  intros, refl
end

However, you can use unfold_cases { refl } to prove ∀ x, myand ff x = ff and ∀ x, myand x ff = ff. For definitions with many cases, the savings can be very significant.

The term that gets generated for the above definition looks like this:

λ (a a_1 : bool),
a.cases_on
  (a_1.cases_on (id_rhs bool ff) (id_rhs bool ff))
  (a_1.cases_on (id_rhs bool ff) (id_rhs bool tt))

When the tactic tries to prove the goal ∀ x, myand ff x = ff, it starts by intros, followed by unfolding the definition:

⊢ ff.cases_on
  (x.cases_on (id_rhs bool ff) (id_rhs bool ff))
  (x.cases_on (id_rhs bool ff) (id_rhs bool tt)) = ff

At this point, it can make progress using dsimp. But then it gets stuck:

⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) x = ff

Next, it can introduce a case split on x. At this point, it has to prove two goals:

⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) ff = ff
⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) tt = ff

Now, however, both goals can be discharged using refl.

source

meta def tactic.unfold_cases.find_splitting_expr :

expr → tactic expr

Given an equation f x = y, this tactic tries to infer an expression that can be used to do distinction by cases on to make progress.

Pre-condition: assumes that the outer-most application cannot be beta-reduced (e.g. whnf or dsimp).

source

meta def tactic.unfold_cases.unfold_cases_core (inner : tactic.interactive.itactic) :

tactic unit

Tries to finish the current goal using the inner tactic. If the tactic fails, it tries to find an expression on which to do a distinction by cases and calls itself recursively.

The order of operations is significant. Because the unfolding can potentially be infinite, it is important to apply the inner tactic at every step.

Notice, that if the inner tactic succeeds, the recursive unfolding is stopped.

source

meta def tactic.unfold_cases.unfold_tgt :

expr → tactic unit

Given a target of the form ⊢ f x₁ ... xₙ = y, unfolds f using a delta reduction.

source

meta def tactic.interactive.unfold_cases (inner : tactic.interactive.itactic) :

tactic unit

This tactic unfolds the definition of a function or match expression. Then it recursively introduces a distinction by cases. The decision what expression to do the distinction on is driven by the pattern matching expression.

A typical use case is using unfold_cases { refl } to collapse cases that need to be considered in a pattern matching.

have h : foo x = y, by unfold_cases { refl },
rw h,

The tactic expects a goal in the form of an equation, possibly universally quantified.

We can prove a theorem, even if the various case do not directly correspond to the function definition. Here is an example application of the tactic:

def foo : ℕ → ℕ → ℕ
| 0     0 := 17
| (n+2) 17 := 17
| 1     0 := 23
| 0     (n+18) := 15
| 0     17 := 17
| 1     17 := 17
| _     (n+18) := 27
| _     _ := 15

example : ∀ x, foo x 17 = 17 :=
begin
  unfold_cases { refl },
end

The compiler generates 57 cases for foo. However, when we look at the definition, we see that whenever the function is applied to 17 in the second argument, it returns 17.

Proving this property consists of merely considering all the cases, eliminating invalid ones and applying refl on the ones which remain.

Further examples can be found in test/unfold_cases.lean.

source

def tactic_doc.tactic.unfold_cases :

tactic_doc_entry

A typical use case is using unfold_cases { refl } to collapse cases that need to be considered in a pattern matching.

have h : foo x = y, by unfold_cases { refl },
rw h,

The tactic expects a goal in the form of an equation, possibly universally quantified.

We can prove a theorem, even if the various case do not directly correspond to the function definition. Here is an example application of the tactic:

def foo : ℕ → ℕ → ℕ
| 0     0 := 17
| (n+2) 17 := 17
| 1     0 := 23
| 0     (n+18) := 15
| 0     17 := 17
| 1     17 := 17
| _     (n+18) := 27
| _     _ := 15

example : ∀ x, foo x 17 = 17 :=
begin
  unfold_cases { refl },
end

The compiler generates 57 cases for foo. However, when we look at the definition, we see that whenever the function is applied to 17 in the second argument, it returns 17.

Proving this property consists of merely considering all the cases, eliminating invalid ones and applying refl on the ones which remain.

Further examples can be found in test/unfold_cases.lean.