using eta-rfl for Equiv

Stream: mathlib4

[Yakov Pechersky]

I have a proposal for a possible non-port change for going from mathlib3 to mathlib4. Now that eta equivalence is rfl by the kernel, something like

def pprodEquivProd {α β : Type _} : PProd α β ≃ α × β where
  toFun x := (x.1, x.2)
  invFun x := ⟨x.1, x.2⟩

has proofs of both inverse conditions as intros; rfl. I propose that we port Equiv as

structure Equiv (α : Sort _) (β : Sort _) where
  toFun : α → β
  invFun : β → α
  left_inv : LeftInverse invFun toFun := by intros; rfl
  right_inv : RightInverse invFun toFun := by intros; rfl

Other options are by simp, by obviously, or even fancier "Try this:" which provide an explicit proof term a la tidy?. Is it out of scope to do this at this stage of the port?

[Mario Carneiro]

ext; rfl seems also applicable there

[Mario Carneiro]

in particular, your proof won't handle function extensionality

[Scott Morrison]

I think we could try some things like this. I propose that we do them separately from the porting PRs, so it's easier to undo if needed.

[Eric Wieser]

I feel like intros, rfl is unlikely to be true for many equivalences outside of that basic file, so the use-case doesn't seem that convincing to me

[Yaël Dillies]

I think a . obviously as in category theory would make more sense.

[Eric Rodriguez]

that's super slow thoguh

[Eric Wieser]

It feels like the tradeoff here is "make the really trivial cases even more trivial, but make the complex cases slower by running a tactic that will fail more than half the time"

[Kevin Buzzard]

We need to find a way to make obviously replace itself with the output of tidy? before committing :-)

[Eric Wieser]

That sounds like a lot of effort to save typing by tidy?

[Kevin Buzzard]

No I mean that tidy never runs. Right now if a goal is filled by tidy then it takes a long time and that long time is repeated the next 1000 times we compile mathlib. I want an autoparam which runs once and then replaces itself with a better autoparam that takes much less time

[Jireh Loreaux]

What we want is code folding so that you still see by tidy, but it's fast after the first run because it adds the proof script it found, but VS Code just optionally hides that from the user.

[Alex J. Best]

Or for the tidy tactic to cache what it did in an olean-like file somehow. It would be great if simp could do this too to remember which lemmas it used.
This is essentially the same as what Jireh says, just saving the script in a different file. For finishing tactics this wouldn't be too awkward to implement, the tactic could read this cache file, execute the same proof, and then if it fails revert to normal execution and save the proof. The slightly trickier thing would be when there are goals left at the end, to know if the script needs to be changed when re-run

[Eric Wieser]

Kevin Buzzard said:

No I mean that [...] I want an autoparam which runs once and then replaces itself with a better autoparam that takes much less time

Sure, and I'm saying that at the cost of the 8 characters by tidy? and a single click, you effectively have that behavior today

[Jireh Loreaux]

I would much prefer code-folding to a cache file because it would be easier to inspect the generated script.

[Kevin Buzzard]

@Eric Wieser no we don't have that today because we're talking about autoparams filling in structure fields, not humans