by_cases renames wrong hypothesis

Stream: lean4

[Horațiu Cheval]

In the example below I used the mathlib by_cases tactic to go by cases on q and Not q. The names h2 I gave in the two cases rename the hypothesis ¬q → ¬p from its initial name h` to h2, instead of be used for the newly introduced hypotheses.

import Mathlib


theorem contraposition' (p q : Prop) : (¬q → ¬p) → (p → q) := by
  intros h hp
  by_cases q
  case pos h2 =>
  /-
  p q : Prop
  h2 : ¬q → ¬p
  hp : p
  h : q
  ⊢ q
  -/
  case neg h2 => sorry

Is it a bug in by_cases or am I misunderstanding how to use it?

[Mario Carneiro]

the mathlib by_cases tactic is "unhygienic" in the sense that it introduces a variable named h which you are allowed to directly refer to

[Mario Carneiro]

which means that the case tactic will not rename it because it only renames newly introduced inaccessible variables

[Horațiu Cheval]

So if I need to give it another name do I just rename the newly introduced h?

[Mario Carneiro]

the syntax for naming the variable in by_cases is by_cases h2 : q

[Horațiu Cheval]

I see, thanks! I was confused by the difference between this and the builtin by_cases

[Mario Carneiro]

std also introduces another syntax for by_cases that IMO looks better:

theorem contraposition' (p q : Prop) : (¬q → ¬p) → (p → q) := by
  intros h hp
  if h2 : q then
    sorry
  else
    sorry

[Jireh Loreaux]

Are we just allowing the unhygienic by_cases in mathlib4 in order to ease porting? In my mind it would be nice to remove these kinds of "features".

[Mario Carneiro]

yes

[Mario Carneiro]

the std version of by_cases doesn't have this "feature"

[Mario Carneiro]

once mathlib4 is mostly ported, it will be much easier to do semi-automated linter-powered refactors like replacing induction' with induction and fixing the case name references

[Mario Carneiro]

these are things that mathport can't do because it needs the lean4-side syntax to typecheck, so it is easier to apply post-port, either as a refactoring step encouraged by a linter like the unnecessarySeqFocus linter, or a full pass over the library when we are done