weaker wlog

Stream: Is there code for X?

[Tristan Figueroa-Reid]

I use wlog as a general way to have guard statements in my proofs for cases that I don't care about - e.g. if I had 4 trivial cases, I wouldn't want to nest a by_cases statement or try to construct some hypothesis that I can plug into rcases. Is there some kind of wlog-like tactic that mimics this sort of style,?

Example:

unless h : a = b
· sorry
unless h : c = d
· sorry
-- The rest of the proof which holds when a ≠ b ∧ c ≠ d

[Eric Wieser]

Can you make a mwe?

[Eric Wieser]

(eg, a proof using by_cases you want a different spelling of)

[Eric Wieser]

Is the wlog here along the lines of what you want?

[Tristan Figueroa-Reid]

Eric Wieser said:

Is the wlog here along the lines of what you want?

That is the use case that I was thinking of :+1:

[Tristan Figueroa-Reid]

import Mathlib.Tactic

theorem div_le_self₁ (n k : Nat) : n / k ≤ n := by
  induction n using Nat.strongRecOn with
  | ind n ih =>
    rw [Nat.div_eq]
    by_cases h : (0 < k ∧ k ≤ n)
    · suffices (n - k) / k + 1 ≤ n by simp [h, this]
      have ⟨hK, hKN⟩ := h
      have hSub : n - k < n := Nat.sub_lt (Nat.lt_of_lt_of_le hK hKN) hK
      have : (n - k) / k ≤ n - k := ih (n - k) hSub
      exact Nat.succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)
    · simp [h]

theorem div_le_self₂ (n k : Nat) : n / k ≤ n := by
  induction n using Nat.strongRecOn with
  | ind n ih =>
    rw [Nat.div_eq]
    wlog h : (0 < k ∧ k ≤ n)
    · simp [h]
    suffices (n - k) / k + 1 ≤ n by simp [h, this]
    have ⟨hK, hKN⟩ := h
    have hSub : n - k < n := Nat.sub_lt (Nat.lt_of_lt_of_le hK hKN) hK
    have : (n - k) / k ≤ n - k := ih (n - k) hSub
    exact Nat.succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)

[Tristan Figueroa-Reid]

[Not exactly an MRE, but more of a motivating example]

Take this proof of div_le_self with by_cases vs with wlog - the latter reads more like a paper-and-pen proof. It would be nice if we had a version of wlog which didn't carry the symmetric hypothesis and was named unless.

[Eric Wieser]

I think unless in do notation is also missing the h: notation, maybe both should be added at once

[Jz Pan]

I think your unless h : a = b is just by_cases h : a = b; swap

[Tristan Figueroa-Reid]

I haven't seen anyone use swap after by_cases to replicate this but it is essentially just that.

I have seen the wlog pattern frequently like in the PR Eric Wieser mentioned above - though it does make sense not to add this tactic since it is a synonymous tactic to by_cases ...; swap or wlog ... ; clear this.

[Tristan Figueroa-Reid]

Though, are these sort of 'synonymous' tactics accepted? I've been using wlog to fill in this role for quite some time now, but I recently made a PR for the Seymour project that used this three times, and using wlog here is abuse of notation, but by_cases causes me to completely break the flow of the proof unless I consistently use the aforementioned swap.

[Jz Pan]

Tristan Figueroa-Reid said:

I haven't seen anyone use swap after by_cases to replicate this but it is essentially just that.

There are several use cases in mathlib: https://github.com/leanprover-community/mathlib4/blob/9b0c6a877559b4bb45860affaeafb705cee085aa/Mathlib/Order/Filter/ENNReal.lean#L136 https://github.com/leanprover-community/mathlib4/blob/9b0c6a877559b4bb45860affaeafb705cee085aa/Mathlib/RingTheory/RingHom/Integral.lean#L59 https://github.com/leanprover-community/mathlib4/blob/9b0c6a877559b4bb45860affaeafb705cee085aa/Mathlib/MeasureTheory/Function/UnifTight.lean#L253 https://github.com/leanprover-community/mathlib4/blob/9b0c6a877559b4bb45860affaeafb705cee085aa/Mathlib/Algebra/Homology/Embedding/Connect.lean#L86 and so on.

[Tristan Figueroa-Reid]

Interesting! Yet, we do also have plenty of examples of wlog being used without references to this! (I did check to make sure that these worked after clear this)

https://github.com/leanprover-community/mathlib4/blob/50e49dc2e9c35748e2313071052bdb6dd16a6fe5/Mathlib/Data/Matroid/Circuit.lean#L128 https://github.com/leanprover-community/mathlib4/blob/50e49dc2e9c35748e2313071052bdb6dd16a6fe5/Archive/Wiedijk100Theorems/BuffonsNeedle.lean#L325 https://github.com/leanprover-community/mathlib4/blob/50e49dc2e9c35748e2313071052bdb6dd16a6fe5/Mathlib/Order/KrullDimension.lean#L141 https://github.com/leanprover-community/mathlib4/blob/50e49dc2e9c35748e2313071052bdb6dd16a6fe5/Mathlib/Topology/Separation/Regular.lean#L256

[Tristan Figueroa-Reid]

Actually, even if synonymous tactics are discouraged, it could be worthwhile to add a linter looking for wlog without usages of the generated symmetric hypothesis and suggest a by_cases ...; swap.

[Ruben Van de Velde]

There's also by_cases; case neg =>

[Eric Wieser]

It sounds like the PR I linked should not be using wlog after all?

[Johan Commelin]

Tristan Figueroa-Reid said:

Though, are these sort of 'synonymous' tactics accepted? I've been using wlog to fill in this role for quite some time now, but I recently made a PR for the Seymour project that used this three times, and using wlog here is abuse of notation, but by_cases causes me to completely break the flow of the proof unless I consistently use the aforementioned swap.

I think that such synonymous tactics can improve the readability of the proof, and the intent of the author.
In this case, it sounds like the tactic can be implemented as a rather easy tactic macro, with a well-defined spec.
I would be open to adding it.

[Yaël Dillies]

Sorry, but I would like to stop you right here: We had been talking about making by_cases run push_neg, which here would allow you to do

by_cases hab : a ≠ b
· sorry -- `hab : a ≠ b` is in context
by_cases hcd : c ≠ d
· sorry -- `hab : a = b` and `hcd : c ≠ d` are in context
-- `hab : a = b` and `hcd : c = d` are in context

[Yaël Dillies]

IMO this is a much better solution than introducing yet another tactic

[Jz Pan]

Yaël Dillies said:

We had been talking about making by_cases run push_neg

Maybe we should introduce by_cases! to make by_cases backward compatible.

[Yaël Dillies]

We really should avoid introducing new tactics/variants thereof when the existing tactics can be modified. Does anyone really rely on getting hP : ¬ ¬ P in the second branch when doing by_cases hP : ¬ P?

[Jz Pan]

But contrapose and by_contra tactics normally do not push_neg, only their ! version do.

So IMHO this should be the same for by_cases.

[Ruben Van de Velde]

Probably most code that does that, but will be easy to fix

[Ruben Van de Velde]

Though I don't mind either way

[Yaël Dillies]

Jz Pan said:

But contrapose and by_contra tactics normally do not push_neg, only their ! version do.

Yes, I believe that should be fixed too

[Ruben Van de Velde]

I guess there's a stronger argument to do all three at the same time

[Mario Carneiro]

I would prefer if push_neg is called explicitly or via !. I don't want to see if running push_neg

[Yaël Dillies]

Tactic-mode if or term-mode if? I personally am happy to see both stay the way they are: if is computer-science, by_cases is mathematics, so the difference in behavior seems acceptable to me

[Mario Carneiro]

if is syntax for by_cases

[Mario Carneiro]

I don't think cs vs mathematics is the right way to differentiate push_neg vs not

[Mario Carneiro]

it has to do with whether you want to control the goal state or are just bashing away

[Yaël Dillies]

... whether the goal is Type- or Prop-valued?

[Mario Carneiro]

as well as whether you are wanting to hide details for e.g. a tutorial

[Mario Carneiro]

no, the goal is unrelated

[Mario Carneiro]

this is about rewriting the condition

[Tristan Figueroa-Reid]

(I forgot to check in with this thread) Thanks for this! I'll update the linting thread to reflect the conversation here :+1: