data out of emptiness

Stream: general

[Sebastien Gouezel]

Look at the following (on current mathlib):

import linear_algebra.determinant

def linear_equiv.of_det_ne_zero
  {𝕜 : Type*} [field 𝕜] {M : Type*} [add_comm_group M] [module 𝕜 M]
  [finite_dimensional 𝕜 M] {f : M →ₗ[𝕜] M} (hf : linear_map.det f ≠ 0) :
  M ≃ₗ[𝕜] M :=
begin
  rw ← linear_map.det_to_matrix (finite_dimensional.fin_basis 𝕜 M) at hf,
  -- goals accomplished
end

Lean says that there is no goal left, after an innocent rewrite. Printing the def, it turns out that it uses linear_equiv.refl 𝕜 M as the definition. My guess is that rw tries refl after a rewrite, and indeed here refl works, but it is not the usual one :-) I am sure I can work this around, but I wanted to share this with you as the unexpected proof of the day.

[Yakov Pechersky]

Are the refl, symm, and trans tags for (linear_)equivs solely to make calc mode for data work properly?

[Kevin Buzzard]

Of course refl also works to close the goal, so this proof is not so surpsiring. Note that in contrast to the term rfl, the tactic refl will close any goal of the form R X X with R a reflexive relation such that theorem saying R X X is tagged with @[refl] (and #print linear_equiv.refl shows that it is).

[Kevin Buzzard]

I think that the symmetry tactic looks for @[symm] tags.

[Eric Wieser]

I don't think rw ... at has any right to touch the main goal, so IMO this is a bug

[Kyle Miller]

rw does a weak version of refl at the end. It does tactic.reflexivity reducible, where refl does tactic.reflexivity semireducible. I gather that this means rw's version of refl will only unfold definitions marked reducible, for example abbreviations.

[Eric Wieser]

I don't think it should do that for rw ... at h, only for rw ... or rw ... at ⊢. I can't think of any situation in which doing it for the former would be anything but surprising and unhelpful

[Kyle Miller]

I just mean to confirm Sebastien's guess (though with the caveat that it's not quite refl).

If you wanted to make it only do this when it's rewriting the goal, this might be a replacement for rw_core (though I didn't test it)

private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
match loca with
| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules >> try (reflexivity reducible))
| _            := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules >> try (reflexivity reducible))
end >> (returnopt rs.end_pos >>= save_info <|> skip)

[Eric Rodriguez]

I think it'd be nice if we could give it a separate argument for reducibility - I find often that I want to do rw! where it does rw and then a stronger refl. Would everyone be fine with both of these in core lean?

[Mario Carneiro]

I prefer using rw; refl for this

[Martin Dvořák]

Is the conclusion that @Kyle Miller was indeed right — that rw does a weak version of refl even when it is called asrw ... at h? Or is it something else that closed the goal?

[Martin Dvořák]

That was a question. I am really confused now.

[Kevin Buzzard]

You can experiment for yourself:

import tactic

example (a b : ℕ) (h : a + b = 37) : 2 = 2 :=
begin
  rw add_comm at h,
end

[Floris van Doorn]

That is correct, Martin. rw ... at h does try a weak version of refl.

[Martin Dvořák]

Thank you!

[Eric Wieser]

If you have a multiple choice question I recommend separate messages to avoid reactions being confusing!