wlog tactic : documentation/howto?

Stream: general

[Antoine Chambert-Loir]

I am wondering whether there is a documentation or howto for the wlog tactic.
In one of the theorems I'm proving, I have m n : nat plus some properties such as a: s m b : s n and I wish to sort according m ≤ n or n ≤ m, while exchanging the roles of a, b if needed.

I have seen a few examples but they don't seem to happen in my case.

[Johan Commelin]

@Antoine Chambert-Loir unfortunately, the wlog tactic is not so easy to use.

[Antoine Chambert-Loir]

That's unfortunate !

[Johan Commelin]

Mario recently wrote a variant. It would be interesting to see if you find it better.

[Johan Commelin]

namespace tactic

meta def take_pi_args : nat → expr → list name
| (n+1) (expr.pi h _ _ e) := h :: take_pi_args n e
| _ _ := []

namespace interactive
setup_tactic_parser

meta def doneif (h : parse ident?) (t : parse (tk ":" *> texpr))
  (revert : parse (
    (tk "generalizing" *> ((none <$ tk "*") <|> some <$> ident*)) <|> pure (some []))) :
  tactic unit := do
  let h := h.get_or_else `this,
  t ← i_to_expr ``(%%t : Sort*),
  (num_generalized, goal) ← retrieve (do
    assert_core h t, swap,
    num_generalized ← match revert with
    | none := revert_all
    | some revert := revert.mmap tactic.get_local >>= revert_lst
    end,
    goal ← target,
    return (num_generalized, goal)),
  tactic.assert h goal,
  goal ← target,
  (take_pi_args num_generalized goal).reverse.mmap' $ λ h,
    try (tactic.get_local h >>= tactic.clear),
  intron (num_generalized + 1)

meta def wlog' (h : parse ident?) (t : parse (tk ":" *> texpr)) : tactic unit :=
doneif h t none >> swap

end interactive
end tactic

[Johan Commelin]

Could you please paste that somewhere near the top of your file, and then write wlog' hmn : m ≤ n in your proof?

[Johan Commelin]

This wlog does not (yet) try to close any trivial goals for you. But it does create goals that you would otherwise have to setup manually.

[Gabriel Ebner]

This wlog does not (yet) try to close any trivial goals for you. But it does create goals that you would otherwise have to setup manually.

This is so much better than the current wlog!

[Sebastien Gouezel]

Honestly, the current wlog is not so bad. Does

  wlog hmn : m ≤ n := le_total m n using [m n, n m] tactic.skip,

work for you?

[Johan Commelin]

I would love to see the pushout of both wlog variants.

[Kevin Buzzard]

I think we have pushouts in category theory

[Antoine Chambert-Loir]

@Sebastien Gouezel No, not quite because I needed to introduce a lot of stuff before:
m and n come from other objects a and b, and I need to exchange them as well,
as well as sets u and v such that hau: a ∈ u and hbv: b ∈ v…

When I try to add hau and hbv in the permutation, Lean complains that hau depends on u.

IDK, maybe that'll better wait for the moment when I have to PL this material.

[Antoine Chambert-Loir]

@Johan Commelin Neither. Strangely, the object hmn has more or less the same type as the theorem I need to prove, and not the type m ≤ n which is expected…

[Johan Commelin]

@Antoine Chambert-Loir The hmn should indeed have almost the same type as what you want to prove. But with an additional assumption m ≤ n somewhere in the middle. With this "bare bones" wlog' you have to do the case split on m ≤ n ∨ n ≤ m manually. And you also have to do all the permutation stuff manually.

[Johan Commelin]

What wlog' does is: you claim that it suffices to treat the case with m ≤ n, now you have to do two thing: (1) prove that it is sufficient to do that (2) prove the goal under this added assumption.

[Johan Commelin]

But it doesn't give you any help with (1). It only sets up the goal state for you.

[Sebastien Gouezel]

If you have a #mwe, we can have a more detailed look.

[Antoine Chambert-Loir]

Sebastien Gouezel said:

If you have a #mwe, we can have a more detailed look.

The following example is a working example, minimal in the sense that deleting any line makes it break ;-) , but not that small.
But Idk how to make it smaller (the complexity comes from the is_preconnected function).

import topology.connected

open set classical topological_space
open_locale classical topological_space

universes u
variables {α : Type u} [topological_space α] {s t : set α}


/--
The union Union s of an increasing mapping s of preconnected sets
is preconnected
-/

variable ι : Type _
variables [ linear_order ι ]

theorem is_preconnected.Union_of_directed  { s : ι → set α }
  (H : ∀ n: ι, is_preconnected (s n))
  (K : ∀ m n: ι, m ≤ n → s m ⊆ s n) :
  is_preconnected ( Union s ) :=
begin
  rw is_preconnected,
  intros u v hu hv Huv Ku Kv ,
  obtain ⟨ a, Kua ⟩ : ∃ a, a ∈ Union s ∩ u, from Ku,
  obtain ⟨ b, Kvb ⟩ : ∃ b, b ∈ Union s ∩ v, from Kv,
  obtain ⟨ m, Kam ⟩ : ∃ m, a ∈ s m , from mem_Union.1 Kua.left,
  obtain ⟨ n, Kbn ⟩ : ∃ n, b ∈ s n , from mem_Union.1 Kvb.left,

  cases le_total m n with hmn hnm,

  /- Le cas où m ≤ n -/
  have Kan : a ∈ s n := mem_of_mem_of_subset Kam ((K m n) hmn),

  have Hnuv : ((s n) ∩ (u ∩ v)).nonempty :=
  begin
      apply (H n), apply hu, apply hv,
      apply has_subset.subset.trans (subset_Union s n) Huv,
      apply nonempty_of_mem  (mem_inter Kan Kua.right),
      apply nonempty_of_mem (mem_inter Kbn Kvb.right),
  end,
  have Knuv : ((s n) ∩ (u ∩ v)) ⊆ Union s ∩ (u ∩ v) :=
  begin
  apply inter_subset_inter,
  apply subset_Union,
  apply eq.subset, refl,
  end,
  exact nonempty.mono Knuv Hnuv,

  /- Le cas où n ≤ m -/
  have Kbm : b ∈ s m := mem_of_mem_of_subset Kbn ((K n m) hnm),

  have Hnuv : ((s m) ∩ (u ∩ v)).nonempty :=
  begin
      apply (H m), apply hu, apply hv,
      apply has_subset.subset.trans (subset_Union s m) Huv,
      apply nonempty_of_mem (mem_inter Kam Kua.right),
      apply nonempty_of_mem (mem_inter Kbm Kvb.right),
  end,
  have Kmuv : ((s m) ∩ (u ∩ v)) ⊆ Union s ∩ (u ∩ v) :=
  begin
  apply inter_subset_inter,
  apply subset_Union,
  apply eq.subset, refl,
  end,
  exact nonempty.mono Kmuv Hnuv,
end

[Sebastien Gouezel]

You can try with

  revert a b u v,
  wlog hmn : m ≤ n := le_total m n using [m n, n m] tactic.skip,

Does it help?

[Antoine Chambert-Loir]

Sebastien Gouezel said:

You can try with

  revert a b u v,
  wlog hmn : m ≤ n := le_total m n using [m n, n m] tactic.skip,

Does it help?

Yes!
I could then just prove the second case using

 intros a b u v hu hv Huv Ku Kv Kau Kbv Kam Kbn,
  rw union_comm at Huv,
  rw inter_comm u v,
  exact this b a v u hv hu Huv Kv Ku Kbv Kau Kbn Kam

(and, by the way, I understood a bit more how this wlog tactic works, thanks!).
Thanks a lot!

[Johan Commelin]

This works with wlog'

  wlog' H : m ≤ n,
  { cases le_total m n with hmn hnm,
    { apply H, assumption' },
    { rw set.inter_comm u v, apply H, assumption', rwa set.union_comm, } },
  rename H_1 hmn,

[Johan Commelin]

That rename is a "bug" in wlog'. It should allow the user to specify the name of the hypothesis.

[Alex J. Best]

@Johan Commelin and @Mario Carneiro where did this variant of wlog come from, I ended up writing my own version of this wlog' today (at https://github.com/leanprover-community/flt-regular/blob/may-assume/src/tactic/may_assume.lean called may assume) without realising it basically already existed till after I was done! It would be great to have one or the other in mathlib

[Mario Carneiro]

It was requested by @Tom Barnet-Lamb in another stream a few weeks ago