feat(Mathlib/Logic/Equiv/LocalEquiv): add the `mfld_set_tac` tactic

[dupuisf]

trafficstars

This PR adds the mfld_set_tac tactic. This tactic relies on a custom simp set which mostly contain lemmas about advanced math that is not yet in mathlib4. In the test file, we have created stubs of a random subset of the various definitions and lemmas it needs; this will need to be revisited during the port.

Co-authored-by: @hrmacbeth

[dupuisf]

I changed it to register the simp attribute the easy way (i.e. the way Leo showed us in the demo after we wrote the tactic). This means that now the file MfldSimpsAttr.lean contains a grand total of one line of code -- I guess we can just move it to Mathlib/Tactic/Basic...?

[dupuisf]

The linter is now complaining about the absence of docstring on the register_simp_attr line, but this currently cannot be done.

[digama0]

@dupuisf Like I mentioned earlier, this declaration should go near where it was placed in lean 3, not in Tactic.Basic.

[gebner]

Looks good to me modulo the build error.

For completeness, I should mentioned that you can also define this tactic as a macro:

local macro "mfld_set_simp_aux" : tactic =>
  `(intro h_my_y; try { simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps] })

macro "mfld_set_simp" : tactic => `(first
  | show _ = _; apply Set.ext; intro my_y; constructor <;> { mfld_set_simp_aux }
  | show _ ⊆ _; intro my_y; mfld_set_simp_aux
  | fail "mfld_set_simp goal should be = or ⊆")

(Although show _ ⊆ _ is extremely underpowered as a goal matching tool. For example, show (_ : Set _) ⊆ _ doesn't work because of some implicit lambda shenanigans (afaict). We also don't have a nice way to commit to a branch in first.)

[dupuisf]

On the simp attribute, I just copied the string that is passed as an argument to the command into the docstring. I assume that the string that is passed is also meant to be documentation, if this is not the case I am happy to change it.

[gebner]

I just copied the string that is passed as an argument to the command into the docstring.

That's a surprising duplication, but we should fix that in core.

Thanks!

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build