Zulip Chat Archive

Stream: general

Topic: wlog example

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

What about:

Lean: 28f4143be31b7aa3c63a907be5443ca100025ef1
mathlib: d84af03bdb8ec4e02c96b6262e7b78c8f3de412b

Patrick Massot (Apr 02 2018 at 15:31):

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

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

Sorry

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

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?

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

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?

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

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

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

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

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