Zulip Chat Archive

Stream: general

Topic: wlog example


view this post on Zulip Simon Hudon (Apr 02 2018 at 15:24):

What about:

Lean: 28f4143be31b7aa3c63a907be5443ca100025ef1
mathlib: d84af03bdb8ec4e02c96b6262e7b78c8f3de412b

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:31):

Thanks

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:32):

But now rcases doesn't work in my code

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:33):

Sorry

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:33):

It's gone now

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:33):

I missed one server restart

view this post on Zulip Simon Hudon (Apr 02 2018 at 15:34):

Sorry

I can't evaluate that

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:34):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 02 2018 at 15:37):

Is that instance used in your proof?

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:37):

What proof?

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:37):

I have no proof yet

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:37):

(actually I have one but without wlog)

view this post on Zulip Simon Hudon (Apr 02 2018 at 15:38):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:38):

Of course

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:38):

everything makes use of that

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:38):

it's the topological space structure on X

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:38):

https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/support.lean#L133

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 02 2018 at 15:41):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:43):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:44):

Maybe I completely misunderstood what wlog is meant to do

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:46):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:47):

How did you do that?

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 02 2018 at 15:55):

Is that the only goal being printed?

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:57):

yes

view this post on Zulip Simon Hudon (Apr 02 2018 at 16:00):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 16:01):

Thanks a lot!

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 19 2018 at 04:09):

how is wlog now?

view this post on Zulip Kenny Lau (Apr 19 2018 at 04:10):

I don't really think one can use wlog

view this post on Zulip Kenny Lau (Apr 19 2018 at 04:10):

I mean, it passed those simple examples in the tests

view this post on Zulip Simon Hudon (Apr 19 2018 at 22:54):

Can you show what you tried?


Last updated: May 16 2021 at 21:11 UTC