Strange behavior of `simp`

Stream: new members

[Ching-Tsun Chou]

Why does the first example below work but the second doesn't? Lean tells me that simp made no progress. That doesn't make any sense.

import Mathlib
open Classical

example (k : ℕ) (h : k > 0) : 42 = if k = 0 then 13 else 42 := by
  have h' := (by omega : k ≠ 0)
  simp [h']

example (k : ℕ) (h : k > 0) : 42 = if k = 0 then 13 else 42 := by
  simp [(by omega : k ≠ 0)]
  sorry

[Kyle Miller]

The short answer is that simp [show k ≠ 0 by omega] works.

[Kyle Miller]

The longer answer is that have h' := (by omega : k ≠ 0) only works because of the order that unification happens. Roughly, by omega is deferred and is a metavariable, it gets the type k ≠ 0, and this unifies with the type of h' (which starts as a metavariable) which "locks in" the type.

[Kyle Miller]

However, as a simp argument, (by omega : k ≠ 0) doesn't have any such place the intended type is stored. Tactics don't guarantee that the term they produce is structurally the expected type, any more than other terms do. Using show adds in a discretionary term that ensures the type of the term is what you want.

[Kyle Miller]

You can verify it:

variable (k : ℕ) (h : k > 0)
#check (by omega : k ≠ 0)
-- fun a => _check._proof_1 k h a : k = 0 → False

So omega creates a term of type k = 0 → False.

[Kyle Miller]

There are other ways to incidentally capture the type too. For example simp [id (by omega : k ≠ 0)].

[Ching-Tsun Chou]

But putting (by omega : ...)inside the simp bracket seems to work most of the time. I just occasionally encounter the above behavior.

[Kyle Miller]

Yes, that is consistent with the fact that tactics don't guarantee that the term they produce has a type that is structurally the expected type. When it happens to work, it happens to work.

[Mario Carneiro]

if the proof gets extracted, it seems like it should have saved the type at that point though

[Kyle Miller]

What do you mean by 'extracted' @Mario Carneiro?

If simp fully elaborates each term in the simp list before taking a look, then even though the by metavariable has k ≠ 0 as its type, once the tactic assigns a term to the metavariable, that's gone. Tactics don't generally insert type hint terms, right?

[Mario Carneiro]

note that the proof above is _check._proof_1 and not a proof term

[Mario Carneiro]

at the point of extraction, you have to decide on the type of the term to extract

[Mario Carneiro]

and the logical choice for this is the expected type you started with, which if done would ensure that you get k ≠ 0 in this example

[Kyle Miller]

Omega proves by contradiction though, so I'm not surprised :shrug:

[Kyle Miller]

This is a common gotcha, the fact that type ascriptions don't ensure structural type hints, and the tip is to use show instead.

[Mario Carneiro]

the actual proof approach of omega doesn't really matter here

[Mario Carneiro]

because whatever it does is wrapped in "extract the result of this tactic"

[Mario Carneiro]

I'm saying that extraction is another kind of show

[Kyle Miller]

I'm not sure what point you're making — "since omega does extract proofs, it should try to use the expected type even though there's no guarantee that tactics in general create types that are structurally the expected type"?

[Mario Carneiro]

yes

[Mario Carneiro]

although many tactics do ensure this property

[Mario Carneiro]

norm_num pays specific attention to this, not because of making : T) work but because defeq unfolding can cause surprising slowdowns when the kernel decides to unfold the wrong thing

[Mario Carneiro]

dsimp also specifically puts in unfolding hints

[Mario Carneiro]

in fact most cases where the hints were skipped later get refactored when it turns out it was a bad idea

[Kyle Miller]

Whether or not there are concerns about the terms omega is creating, it's still not something you can rely on, that a tactic produces a term whose type is structurally equal to the expected type. (E.g. exact, refine, apply, intro, constructor, and so on.)

Using "show k ≠ 0 by omega" rather than a type ascription is a way to ensure the type is k ≠ 0.