Stream: new members

Topic: How to check whether something reduces?

Jessie Grosen (Mar 08 2022 at 17:19):

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 (Mar 08 2022 at 17:25):

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 (Mar 08 2022 at 18:21):

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

Kyle Miller (Mar 08 2022 at 20:33):

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 (Mar 08 2022 at 20:34):

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 (Mar 08 2022 at 20:43):

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


Last updated: Dec 20 2023 at 11:08 UTC