## Stream: general

### Topic: wlog example

#### Simon Hudon (Apr 02 2018 at 15:24):

Lean: 28f4143be31b7aa3c63a907be5443ca100025ef1
mathlib: d84af03bdb8ec4e02c96b6262e7b78c8f3de412b


Thanks

#### Patrick Massot (Apr 02 2018 at 15:32):

In the mean time I've found that March 27th nightly seems to allow compiling mathlib HEAD

#### Patrick Massot (Apr 02 2018 at 15:32):

But now rcases doesn't work in my code

#### Patrick Massot (Apr 02 2018 at 15:33):

I see tactic.rcases_patt.has_reflect._rec_2: trying to evaluate sorry  each time I use rcases

Sorry

It's gone now

#### Patrick Massot (Apr 02 2018 at 15:33):

I missed one server restart

#### Simon Hudon (Apr 02 2018 at 15:34):

Sorry

I can't evaluate that

#### Patrick Massot (Apr 02 2018 at 15:34):

Now I need to figure out how wlog is meant to be used

#### Patrick Massot (Apr 02 2018 at 15:35):

My naive attempt leads to  failed to revert '_inst_3', it is a frozen local instance (possible solution: use tactic tactic.unfreeze_local_instances to reset the set of local instances)

#### Patrick Massot (Apr 02 2018 at 15:36):

context is

X : Type,
_inst_3 : topological_space X,
f g : homeo X X,
H : supp f ∩ supp g = ∅,
x : X,
h : x ∈ supp f ∪ supp g
⊢ (f ∘ g) x = (g ∘ f) x


#### Patrick Massot (Apr 02 2018 at 15:37):

I'm trying to use wlog (without knowing anything about it, only hoping from the name) to say it suffices to prove the statement when x is in the support of f

#### Simon Hudon (Apr 02 2018 at 15:37):

Is that instance used in your proof?

What proof?

#### Patrick Massot (Apr 02 2018 at 15:37):

I have no proof yet

#### Patrick Massot (Apr 02 2018 at 15:37):

(actually I have one but without wlog)

#### Simon Hudon (Apr 02 2018 at 15:38):

Right ... and does the part that wlog would replace make use of _inst_3?

Of course

#### Patrick Massot (Apr 02 2018 at 15:38):

everything makes use of that

#### Patrick Massot (Apr 02 2018 at 15:38):

it's the topological space structure on X

#### Simon Hudon (Apr 02 2018 at 15:40):

It's curious because wlog shouldn't need to revert anything but f, g, H and h

#### Simon Hudon (Apr 02 2018 at 15:41):

Can you show me the command that you're using?

#### Patrick Massot (Apr 02 2018 at 15:43):

I'm trying to replace the proof with:

lemma fundamental' (f g : homeo X X) (H : supp f ∩ supp g = ∅) : f ∘ g = g ∘ f  :=
begin
funext,
by_cases h : x ∈ supp f ∪ supp g,
{ wlog  h : x ∈ supp f using x y,
},
{ replace h : x ∈ -(supp f ∪ supp g) := h,
rw compl_union (supp f) (supp g) at h,

have f_x : f x = x := compl_supp_subset_fix f h.1,
have g_x : g x = x := compl_supp_subset_fix g h.2,

exact calc (f ∘ g) x = f (g x) : rfl
... = f x : by rw g_x
... = x : by  rw f_x
... = g x : by rw g_x
... = g (f x) : by rw f_x }
end


#### Patrick Massot (Apr 02 2018 at 15:43):

I only remove everything inside the first branch of the by_cases and wlog there

#### Patrick Massot (Apr 02 2018 at 15:44):

Maybe I completely misunderstood what wlog is meant to do

#### Patrick Massot (Apr 02 2018 at 15:46):

I also don't manage to change the topic of messages that should be elsewhere

#### Patrick Massot (Apr 02 2018 at 15:47):

How did you do that?

#### Simon Hudon (Apr 02 2018 at 15:48):

I went to one of my messages preceding most of this conversation, I changed its topic and selected the option "change the topic of everything that came later"

#### Simon Hudon (Apr 02 2018 at 15:49):

Maybe I completely misunderstood what wlog is meant to do

I think I misled you. Try wlog h : x ∈ supp f using f g instead.

#### Patrick Massot (Apr 02 2018 at 15:50):

intron tactic failed, insufficient binders
state:
X : Type,
_inst_3 : topological_space X,
x : X,
f g : homeo X X,
this :
∀ (f g : homeo X X),
x ∈ supp f → supp f ∩ supp g = ∅ → x ∈ supp f ∪ supp g → (f ∘ g) x = (g ∘ f) x,
h : x ∈ supp f
⊢ homeo X X


#### Simon Hudon (Apr 02 2018 at 15:55):

Is that the only goal being printed?

yes

#### Simon Hudon (Apr 02 2018 at 16:00):

Ok I'm going to clone your repo and see what I can do

Thanks a lot!

#### Simon Hudon (Apr 02 2018 at 16:43):

No worries! I found a serious bug in wlog. I'll let you know when I figured out a fix. In the mean time, I hope this is not stopping you

#### Patrick Massot (Apr 02 2018 at 16:44):

No I'm not stopped, I have a working proof (with lot of duplication, hence I thought that would be a good opportunity to learn wlog)

how is wlog now?

#### Kenny Lau (Apr 19 2018 at 04:10):

I don't really think one can use wlog

#### Kenny Lau (Apr 19 2018 at 04:10):

I mean, it passed those simple examples in the tests

#### Simon Hudon (Apr 19 2018 at 22:54):

Can you show what you tried?

Last updated: May 16 2021 at 21:11 UTC