WLOGgery

Stream: maths

[Kevin Buzzard]

I have got two terms P and Q of a certain type, and I want to make a third term R of this type with some properties -- it has to be less than P and less than Q. The construction of R is completely symmetric in P and Q, at some point I extract a real eP from P and a real eQ from Q, and then I define eR to be min eP eQ and build R from this. My goal is now R < P \and R < Q. The proofs of these things will be (a) mildly lengthy and (b) essentially identical, there just being one point where I'll use le_min_left in one thread and le_min_right in the other, and one point where I'll use hP in
one thread and hQ in the other.

Is there some WLOGgery trick I can use to halve the amount of work I'm about to do?

Out of interest, my tactic state is this (this is not really relevant to the question but it gives some kind of an idea as to the situation I'm in):

X : Type,
d : X → X → ℝ,
_inst_1 : is_pseudometric d,
P Q : cover X,
εP : ℝ,
hεP : 0 < εP,
hP : ∀ (x : X), ∃ (U : set X) (H : U ∈ P.C), closed_ball d x εP ⊆ U,
εQ : ℝ,
ε : ℝ := min εP εQ / 2,
hεQ : 0 < εQ,
hQ : ∀ (x : X), ∃ (U : set X) (H : U ∈ Q.C), closed_ball d x εQ ⊆ U,
hε : 0 < min εP εQ,
hε : ε = min εP εQ / 2
⊢ closed_ball_cover d ε _ <* P ∧ closed_ball_cover d ε _ <* Q

[Kevin Buzzard]

(this is teaching material, I'm using non-standard versions of metric spaces, closed balls etc, this is not the issue)

[Kevin Buzzard]

Over the board I'd just say "of course the proof of the second case is the same"

[Kevin Buzzard]

I finished my proof and just cut and pasted it; I had to change two lines for the second case.

  { rw star_ref_iff,
    rintros _ ⟨x, rfl⟩,
    rcases hP x with ⟨U, hUP, hUε⟩, -- <- changes to rcases hQ x
    use [U, hUP],
    rintros _ ⟨y, rfl⟩ hxy,
    rw ne_empty_iff_nonempty at hxy,
    rcases hxy with ⟨z, hzx, hzy⟩,
    refine subset.trans _ hUε,
    intros t hty,
    rw mem_closed_ball at ⊢ hzx hzy hty,
    suffices : d x t ≤ 3 * ε,
    { refine le_trans this _,
      rw hε,
      convert min_le_left εP εQ, -- <- changes to min_le_right
      linarith,
    },
    calc d x t ≤ d x z + d z t : d_triangle d x z t
    ...        ≤ d x z + (d z y + d y t) : by linarith [d_triangle d z y t]
    ...        = d x z + (d y z + d y t) : by rw d_comm d z y
    ...        ≤ 3 * ε : by linarith
  },

[Jalex Stark]

I think the thing I would do is generalize some tail of the proof script so that it closes both goals

[Jalex Stark]

So in this part,

      rw hε,
      convert min_le_left εP εQ, -- <- changes to min_le_right
      linarith,

I'd make it so that linarith just needs to be told min_le_left and min_le_right, and I'd have the line before it put both of those inequalities into the tactic state

[Jalex Stark]

and in this part,

 { rw star_ref_iff,
    rintros _ ⟨x, rfl⟩,
    rcases hP x with ⟨U, hUP, hUε⟩, -- <- changes to rcases hQ x

I'd do something like

all_goals  { rw star_ref_iff,   rintros _ ⟨x, rfl⟩},
rcases hP x with ⟨U, hUP, hUε⟩,
swap, rcases hQ x with ⟨U, hUP, hUε⟩,
all_goals {...

[Jalex Stark]

I guess this is bad pedagogy, though, you're really hoping for one thing you can say at the beginning that's like the mathematician's wlog

[Kevin Buzzard]

I am looking for a WLOG but I might be asking for too much. I feel like I want to be able to say "Anything you can ask me for P, I can tell you the analogous thing for Q" but I'm unclear about whether this is ludicrously optimistic.

[Yury G. Kudryashov]

Did you trywlog?

[Jalex Stark]

The last time I tried to use wlog from just reading tactic#wlog i didn't understand it. I found a couple of examples in the library, and it looks pretty to use and looks like it covers kevin's case:
https://github.com/leanprover-community/mathlib/blob/ff3130da134188aa6491efa6cebe94efa4247273/src/algebra/char_zero.lean
https://github.com/leanprover-community/mathlib/blob/64e464f1970e29ab77e8bdf0a9d3751cdd429f5a/src/data/set/disjointed.lean

[Jalex Stark]

kevin, do you have a mwe? or just a pointer to a file in a github project?

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/uniform-structures/blob/5e2e7ab47fcc425a801f8568d2638fccf2a4e511/exercises/covers_from_pseudometric.lean#L125

The goal at the split is R < P \and R < Q.
The last time I tried to use wlog I didn't understand it either. I'll try it again now.

[Kevin Buzzard]

@Yury G. Kudryashov my (limited) understanding of wlog is that it is able to add extra hypotheses of the form "a <= b" if everything is symmetric in a and b. I have a goal of the form P and Q and I want to say "it suffices to prove P, because a proof of P can be used to generate a proof of Q".

[Yury G. Kudryashov]

Can you say wlog p implies q?