feat: Remove ext attribute on Rat

[adomani]

Following this discussion, I would like to remove the ext attribute from Rat.

This is my first Std PR: I hope that I am doing things correctly!

[adomani]

awaiting-review

[fgdorais]

Could you summarize the Zulip discussion here?

[adomani]

The discussion was essentially that ext digging into ℚ is like ext digging into ℂ and ℂ's ext was removed.

In the specific case, calling ext on an equality of polynomials with rational coefficients entered the polynomials through the equality of their coefficients and then broke up the (rational) coefficients into their numerators and denominators. This leads you astray more often than it is helpful.

[fgdorais]

Approved after minor change.

[adomani]

In the process of fixing Mathlib, Rat.ext was useful exactly once, to prove NNRat.ext_num_den.

Thus, I propose to add also this lemma, but not tagging it with ext.

theorem Rat.ext (p q : ℚ) (hn : p.num = q.num) (hd : p.den = q.den) : p = q := by
  cases p; cases q; subst hn hd; rfl

If this is reasonable, then I will add it to this PR.

Also, the proof of Rat.toNNRat_mul had ext <;> simp ... and is ext; simp ... after the PR.

I am happy to do a pre-emptive PR to Mathlib to make explicit use of the Rat.ext lemma, rather than relying on the ext tactic, if this is the standard approach.

[fgdorais]

Yes, please add the manual Rat.ext lemma (p and q should be implicit) along with a comment explaining why this is not marked @[ext].

[digama0]

Does it work to use local attribute [ext] Rat in the Lemmas file?

[adomani]

@digama0, local attribute complains:

unexpected token 'attribute'; expected 'binder_predicate', 'builtin_simproc', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'

[digama0]

@digama0, local attribute complains:

unexpected token 'attribute'; expected 'binder_predicate', 'builtin_simproc', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'

sorry, the syntax is attribute [local ext] instead of local attribute [ext]

[adomani]

@digama0 I'll try it, but tomorrow, although I'm sure that it will work, since you suggested it!

I imagine that this means to revert all the remaining changes, right?

[adomani]

@digama0 and @fgdorais -- I reverted all changes and made ext a local attribute!

The extra simp lemma that I had added seemed to make proof nicer, in my opinion: can you say why the current ones are better?

[fgdorais]

I think Mario meant the file on Mathlib, not this file. Could you unrevert the changes?

[digama0]

No I did mean to use attribute [local ext] Rat here in Std, because this has the side effect of creating Rat.ext (and marking it [local ext] for the file, which might be useful since this file wants to prove facts about Rat). Downstream, mathlib can use attribute [local ext] Rat.ext to use it in ext proofs.

[fgdorais]

But the generated Rat.ext doesn't have the implicit p and q so it is less suitable for manual use. This is better:

@[local ext] theorem Rat.ext : {p q : Rat} → p.num = q.num → p.den = q.den → p = q
  | ⟨_,_,_,_⟩, ⟨_,_,_,_⟩, rfl, rfl => rfl

The changes Damiano had made were all simplifications of the original and ultimately showed that this ext lemma is not necessary even in this file.

[digama0]

in that case we should fix ext. I don't like the precedent this sets, that @[ext] on structures should be avoided even when it is producing the correct extensionality lemma. This seems like it's working around either an issue in ext or a misuse of it.

[fgdorais]

Yes, it's an issue in ext. This workaround also shows up in Std.Tactic.Ext itself.

[fgdorais]

I still don't want to lose the simpler ext-free proofs that Damiano had proposed.

[adomani]

Can I suggest merging the current minimalistic state of the PR and I can producemoving the discussion about ext to #617, where I also add the rest of the changes?

New PR: #617.

[adomani]

Also, as far as I understand, the reason there was no need to use ext in the earlier version was the new simp lemma that took care of closing the missing goals: I initially did not introduce the manual Rat.ext lemma, I simply removed it.

[fgdorais]

In addition to the sub-optimal binders, there is another bug in ext where marking a structure with @[local ext] generates the .ext and .ext_iff lemmas and incorrectly marks .ext with [ext] instead of [local ext].

[fgdorais]

I don't want this PR to depend on fixing ext. Since the @[local ext] attribute currently does the same thing as just @[ext] and this is undesirable, the workaround

@[local ext] theorem Rat.ext : {p q : Rat} → p.num = q.num → p.den = q.den → p = q
  | ⟨_,_,_,_⟩, ⟨_,_,_,_⟩, rfl, rfl => rfl

at the top of the lemma file is the best option.

In the future, this should be replaced by attribute [local ext] Rat at the top of the file.

[fgdorais]

This currently doesn't work as intended. See #618.

[adomani]

@fgdorais I agree with you: in a file that imports another one containing attribute [local ext] Rat the ext tactic works on Rats.

@digama0 I can revert this PR to its original form, where I had simply removed the ext attribute, introduced mk_den_one and fix the ext proofs in Std, if you think that you would merge it. Otherwise, I am also happy to wait for the fix to the local ext, since the workaround for avoiding ext on Rat is simply to add a stopper ext x : whatever.