How to check whether something reduces?

Stream: new members

[Jessie Grosen]

Maybe I'm trying to do too much programming with dependent types than Lean is meant for, but I'm having some trouble figuring out which eliminators I should expect to reduce and which I shouldn't. I've been trying to figure this out experimentally with #reduce, but it seems like that reduces things further than the type checker will. Is there a better way to figure out how much the type checker will reduce something?

[Jessie Grosen]

For example (based on what I'm working with right now),

#reduce @fin.last_cases 0 (λ _, bool) tt (λ _, ff) 0

gives tt, but

#check (rfl : @fin.last_cases 0 (λ _, bool) tt (λ _, ff) 0 = tt)

fails...

[Eric Wieser]

What 0 is lean inferring there? nevermind, I missed the @

[Kyle Miller]

I believe #reduce uses the kernel to reduce, but the typechecker/elaborator has its own term reducer. This one takes into account the reducible/semireducible/irreducible visibility attributes. With this example, I tried making everything reducible, but it seems to get stuck. I'm guessing it's that fin.reverse_induction is defined using well-founded recursion, which usually is the culprit.

The expectation seems to be that you'll at some point rewrite using the equation lemmas for the definition, which you can explore with the command

#print prefix fin.reverse_induction.equations

The simp tactic uses these lemmas to unfold definitions, and once this is unfolded, refl goes through:

example : @fin.last_cases 0 (λ _, bool) tt (λ _, ff) 0 = tt :=
begin
  simp only [fin.last_cases, fin.reverse_induction],
  refl,
end

[Kyle Miller]

A bit more manually:

example : @fin.last_cases 0 (λ _, bool) tt (λ _, ff) 0 = tt :=
begin
  rw [fin.last_cases.equations._eqn_1, fin.reverse_induction.equations._eqn_1],
  exact rfl
end

[Kyle Miller]

However, a lot of mathlib definitions are designed to be used through an "API". In this case, fin.last_cases has a reduction lemma for this purpose, which you can use after putting 0 into the right form.

example : @fin.last_cases 0 (λ _, bool) tt (λ _, ff) 0 = tt :=
begin
  rw show 0 = fin.last 0, from rfl,
  -- ⊢ fin.last_cases tt (λ (_x : fin 0), ff) (fin.last 0) = tt
  rw fin.last_cases_last,
end