deprecated lean3-ism convention

Stream: mathlib4

[James Gallicchio]

is there a convention for naming theorems that should be deprecated but are ported for backwards compatibility? i'd rather avoid potentially-useful names like (lean3) perm_induction_on -> (lean4) perm_induction_on'.

would perm_induction_on_deprecated or perm_induction_on_old be acceptable?

[Mario Carneiro]

the usual convention is just @[deprecated] def perm_induction_on, unless you want something else to take the name

[Mario Carneiro]

(just in case this has to do with a certain std4 PR: don't PR things that are deprecated from the start, just remove them and keep them in mathlib)

[James Gallicchio]

I think in this case we would like to have a lemma called perm_induction_on, but its statement will be different from the mathlib3 perm_induction_on :/

[James Gallicchio]

(and I'd rather rename the deprecated version than the desired version...)

[James Gallicchio]

If there's no convention, I'll just rename the lean3 version to perm_induction_on_old. Seems reasonable enough.

[Mario Carneiro]

James Gallicchio said:

I think in this case we would like to have a lemma called perm_induction_on, but its statement will be different from the mathlib3 perm_induction_on :/

In that case, you should name the other one to perm_induction_on', and use #align to ensure that mathlib uses go to the deprecated one

[Yury G. Kudryashov]

What will be the difference between lemmas?

[Yury G. Kudryashov]

E.g., for list.repeat vs list.replicate, I just backported the change.

[James Gallicchio]

It changes the induction principle statement to work with the new elab_as_elim stuff. So it's a lean4-specific change.

[Mario Carneiro]

but how specifically?

[Mario Carneiro]

it's not necessarily a lean4 specific change if it also works in lean 3

[James Gallicchio]

The comment from the ad-hoc port was:

/-- The way Lean 4 computes the motive with `elab_as_elim` has changed
relative to the behaviour of `elab_as_eliminator` in Lean 3.
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Potential.20elaboration.20bug.20with.20.60elabAsElim.60/near/299573172
for an explanation of the change made here relative to mathlib3.
-/

[Mario Carneiro]

that is missing the important part of the definition :)

[Yury G. Kudryashov]

Can you just copy+paste the statements of 2 lemmas?

[James Gallicchio]

theorem perm_induction_on
    {P : (l₁ : List α) → (l₂ : List α) → l₁ ~ l₂ → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (nil : P [] [] .nil)
    (cons : ∀ x l₁ l₂, (h : l₁ ~ l₂) → P l₁ l₂ h → P (x :: l₁) (x :: l₂) (.cons x h))
    (swap : ∀ x y l₁ l₂, (h : l₁ ~ l₂) → P l₁ l₂ h →
      P (y :: x :: l₁) (x :: y :: l₂) (.trans (.swap x y _) (.cons _ (.cons _ h))))
    (trans : ∀ l₁ l₂ l₃, (h₁ : l₁ ~ l₂) → (h₂ : l₂ ~ l₃) → P l₁ l₂ h₁ → P l₂ l₃ h₂ →
      P l₁ l₃ (.trans h₁ h₂)) : P l₁ l₂ p := ...

theorem perm_induction_on {P : List α → List α → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂) (h₁ : P [] [])
    (h₂ : ∀ x l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (x :: l₁) (x :: l₂))
    (h₃ : ∀ x y l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (y :: x :: l₁) (x :: y :: l₂))
    (h₄ : ∀ l₁ l₂ l₃, l₁ ~ l₂ → l₂ ~ l₃ → P l₁ l₂ → P l₂ l₃ → P l₁ l₃) : P l₁ l₂ := ...

[James Gallicchio]

top is the new one

[Mario Carneiro]

it seems fine to me, lean 3 uses probably won't even notice the difference

[Mario Carneiro]

so a backport should just work

[Mario Carneiro]

unless the motive is being provided explicitly but that's a relatively easy fix

[James Gallicchio]

Hum, okay. Are there instructions on how to do backports?

[Mario Carneiro]

it's like any other mathlib3 change that may touch a ported file, you make the mathlib3 change and a parallel mathlib4 change

[Eric Wieser]

For heavier changes, it can be easier to make the mathlib3 change and wait for mathlib3port to regenerate before making the mathlib4 change