homeo equiv etc.

Stream: maths

[Patrick Massot]

A more specific version of https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20vs.20class/near/124574243 (it may be easier to understand my problem by looking at code) is https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/support.lean#L188 where I'm clearly very stupidly trying to Lean some trivial lemma. I'm completely tangled in coercions and type classes

[Patrick Massot]

I need two version of supp because I don't know how to have only one

[Patrick Massot]

Then we have a classical rw failure on line 193 (always the same thing, rw itself doesn't do some kind of elaboration or reduction that is needed, and I still can't quite point out what)

[Patrick Massot]

Then I would like line 196 to be unnecessary (with the ugly (g.to_equiv).inv_fun never appearing)

[Patrick Massot]

And finally the computation which should be easy (but still the core of the proof) and cannot do it

[Patrick Massot]

I'd like to know whether the full setup is broken from the beginning or I only need a couple a carefully crafted simp lemmas to hide this mess (and prove stuff).

[Chris Hughes]

cons_inj tells me about the lists being equal. Oops wrong topic.

[Patrick Massot]

I can see this topic has not much success. Maybe the context is too complicated because of topology. But I really think this will come up in other places. The question is: how to do group theory with groups of transformations? As long as you don't need to use the inverse of a transformation, you can easily functions and composition of function. But what about inverses? Say I'm working with permutations of a type (not necessarily encoded as perm in current mathlib). I define the support of a permutation f as the complement supp f of the fixed point set (no topology here). I want to prove supp gfg⁻¹ = g(supp f). And ideally I would really like f, g and g⁻¹ to live in a type endowed with a group structure, because I have other group theoretic stuff to do. What encoding should I use? How to then talk about the image of a subset as in g(supp f)?

[Kevin Buzzard]

I got as far as cutting and pasting a 230 line file and then realising I didn't have the imports

[Kevin Buzzard]

You define suppp f to be supp f?

[Patrick Massot]

If you want to directly play with code it's much faster to git clone

[Patrick Massot]

Yes, that definition is part of the problem

[Patrick Massot]

I couldn't avoid it

[Patrick Massot]

It's part of coercion/extension hell

[Patrick Massot]

supp is defined on functions from X to X

[Patrick Massot]

homeos have coercions to functions

[Patrick Massot]

but it's not enough

[Patrick Massot]

try to replace suppp by supp in the statement following that def and it won't type check

[Patrick Massot]

But it's probably easier to solve the problem as I described it today than to add the topology layer

[Kevin Buzzard]

It's just too hard to make it work.

[Kevin Buzzard]

I have mathlib not compiling.

[Patrick Massot]

make what work?

[Patrick Massot]

I just pushed a version compatible with latest Lean nightly and mathlib head

[Patrick Massot]

(only handling a renamed lemma)

[Kevin Buzzard]

Now I have errors in commutators.lean and groups.lean

[Patrick Massot]

those are old stuff irrelevant here

[Patrick Massot]

they are not updated

[Patrick Massot]

(this repo is my garbage repo, I'm sorry)

[Patrick Massot]

Everything imported in support.lean is ok

[Kevin Buzzard]

OK it now compiles. What's the question?

[Kevin Buzzard]

Not that I'm likely to be able to answer it...

[Patrick Massot]

How do you sort out the mess with supp vs suppp, fundamental vs fundamental'', how to remove the sorries in the proof of supp_conj

[Chris Hughes]

open equiv
variables {α : Type*}

lemma mul_apply (a b : perm α) (x : α) : (a * b) x = (a (b x)) := rfl

@[simp] lemma one_apply (x : α) : (1 : perm α) x = x := rfl

def support (a : perm α) : set α := {x : α | a x ≠ x}

example (f g : perm α) : support (g * f * g⁻¹) = set.image g (support f) :=
set.ext $ λ y, ⟨λ h : _ ≠ _, ⟨g⁻¹ y, λ h₁, by
  rw [mul_apply, mul_apply, h₁, ← mul_apply, mul_inv_self] at h;
  exact h rfl,
show (g * g⁻¹) y = y,by rw mul_inv_self; refl⟩,
λ ⟨x, (hx : _ ≠ _ ∧ _)⟩, show _ ≠ _, from
begin
  rw [mul_apply, ← hx.2, ← mul_apply, ← mul_apply, mul_assoc, inv_mul_self, mul_one, mul_apply],
  assume h,
  rw (equiv.bijective g).1 h at hx,
  exact hx.1 rfl
end⟩

[Chris Hughes]

(deleted)

[Chris Hughes]

I proved a bit of stuff about permutations a few months ago.

[Patrick Massot]

Thank you very much. Now I need to rewrite it in full tactic mode to see how it could help

[Kevin Buzzard]

The issue is that you are using coe everywhere?

[Patrick Massot]

What do you mean using coe everywhere?

[Patrick Massot]

I need homeomorphisms to be able to act as functions

[Patrick Massot]

So yes, they coerce to functions

[Kevin Buzzard]

Is the reason the rw doesn't work on line 193 that you are pushing type class inference too hard?

[Patrick Massot]

I have no idea

[Patrick Massot]

Clearly there is something I'm doing wrong

[Patrick Massot]

I only want to learn how to do it right

[Kevin Buzzard]

ambiguous overload, possible interpretations
  right_inverse
  function.right_inverse

[Patrick Massot]

where do you see that?

[Kevin Buzzard]

when I write #check right_inverse

[Kevin Buzzard]

I don't know how to check types of objects in the middle of Lean code.

[Patrick Massot]

@Chris Hughes don't you have a version of your proof before obfuscation?

[Kevin Buzzard]

Is there an easy way to do that?

[Patrick Massot]

This is something I wonder all the time

[Patrick Massot]

it seems the answer is no

[Kevin Buzzard]

You'd wonder it more if you were reading someone else's code...

[Kevin Buzzard]

So what is (g.to_equiv).to_fun?

[Mario Carneiro]

The reason this topic didn't get much discussion is because you basically said "there is something wrong, check out my code base and find the error"

[Kevin Buzzard]

he said lots of things

[Kevin Buzzard]

maybe there were lots of errors :-)

[Mario Carneiro]

Could you at least post the error message?

[Mario Carneiro]

(s)

[Patrick Massot]

There is no error message. I can't prove stuff

[Patrick Massot]

Because I'm clearly going against Lean

[Kevin Buzzard]

Are you being anti-idiomatic?

[Patrick Massot]

Not writing idiomatic Lean

[Patrick Massot]

exactly

[Mario Carneiro]

what? I am not in a position to see what you are talking about unless you say it here

[Kevin Buzzard]

If you want to get to the bottom of the reason rewrite fails on line 193 you should write a MWE. But I know this isn't your real question.

[Chris Hughes]

@Chris Hughes don't you have a version of your proof before obfuscation?

That's how I wrote it first time. I shouldn't have opened the perm namespace, so if it didn't work that's probably why.

[Kevin Buzzard]

@Mario Carneiro Is there a way of checking the type of a term in the middle of a tactic proof?

[Patrick Massot]

I tried to describe my problems in https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20vs.20class/near/124574243 without code, and then I posted link to my actual code. Then I tried to describe a simplified problem. I don't what I could do better to ask for help

[Kevin Buzzard]

i.e. I can't check it outside the begin/end block because the term is only constructed within the block

[Patrick Massot]

I'm honestly asking

[Kevin Buzzard]

So what is (g.to_equiv).to_fun?

[Patrick Massot]

It's the function underlying the homeomorphism g

[Kevin Buzzard]

for g : homeo X X

[Patrick Massot]

But it goes through two conversions

[Patrick Massot]

First to equiv X X and then to X -> X

[Kevin Buzzard]

When you write g '' ...

[Kevin Buzzard]

what do you think happens there?

[Patrick Massot]

That's mathlib notation for image of a subset

[Patrick Massot]

Lean does figure out the coercions here

[Kevin Buzzard]

set.image so it takes a function

[Kevin Buzzard]

and which function does it take?

[Kevin Buzzard]

Is there some coe directly from homeo to the function?

[Patrick Massot]

(g.to_equiv).to_fun

[Patrick Massot]

yes

[Kevin Buzzard]

That's what it uses?

[Patrick Massot]

instance : has_coe_to_fun (homeo α β) := ⟨_, λ f, f.to_fun⟩

[Patrick Massot]

is defined in homeos.lean

[Patrick Massot]

It's indeed the same as (g.to_equiv).to_fun

[Kevin Buzzard]

This is a funny error message then:

[Kevin Buzzard]

rewrite tactic failed, did not find instance of the pattern in the target expression
  (g.to_equiv).to_fun '' {a : X | (λ (x : X), f x ≠ x) a}
state:
X : Type,
_inst_3 : topological_space X,
f g : homeo X X
⊢ {x : X | conj g f x ≠ x} = g '' {x : X | f x ≠ x}

[Kevin Buzzard]

Is it definitionally the same?

[Chris Hughes]

rw doesn't do definitionally equal things.

[Kevin Buzzard]

oh yeah

[Kevin Buzzard]

that's the second time I've forgotten that this week

[Patrick Massot]

variable (g: homeo X X)
example : (g : X → X) = g.to_equiv.to_fun := rfl

[Kevin Buzzard]

Chris points out the problem

[Patrick Massot]

Yes, I understand this is the problem with the rewrite

[Kevin Buzzard]

definitionally equivalent is not enough

[Patrick Massot]

But I'd like to know the proper way of either not having this problem or workaround it

[Patrick Massot]

without doing this swap, exact ... thing

[Chris Hughes]

Never use ( g.to_equiv).to_fun?

[Patrick Massot]

I don't write this myself

[Chris Hughes]

I usually use show otherwise.

[Patrick Massot]

it only appears in goals and error messages

[Patrick Massot]

What is this λ h : _ ≠ _, dark magic?

[Kevin Buzzard]

I had problems with coercions when I was doing schemes so I just stopped using them completely

[Kevin Buzzard]

and wrote everything out in full

[Patrick Massot]

How do you do it in tactic mode?

[Kevin Buzzard]

show works in tactic mode

[Patrick Massot]

Kevin, how would you do group theory with permutations of a Type without coercions?

[Kevin Buzzard]

show _ ≠ _ :-)

[Patrick Massot]

You both need elements of the group to act on points and to have inverses

[Patrick Massot]

Re: _ ≠ _ he does this in place of intro

[Kevin Buzzard]

I'm just saying that you just write the coercions explicitly.

[Kevin Buzzard]

That was what I did when I got sick of getting type class inference to work. I just wrote down everything myself.

[Patrick Massot]

There must be a better way

[Patrick Massot]

In real world you would never need to distinguish the element of a group of transformation from themselves like this

[Kevin Buzzard]

the real world doesn't use dependent type theory

[Kevin Buzzard]

it uses one piece of notation to mean more than one thing

[Kevin Buzzard]

and we're so used to that, that this world can be kind of annoying sometimes

[Kevin Buzzard]

with their silly pedantic fussing

[Kevin Buzzard]

show {x : X | conj g f x ≠ x} = g.to_equiv.to_fun '' {x : X | f x ≠ x},
rw aux_1 g.right_inv,

[Kevin Buzzard]

works for 193 ;-)

[Patrick Massot]

I don't understand what show does here

[Patrick Massot]

Usually I need to supply a proof after show

[Kevin Buzzard]

it rewrites the goal into a definitionally equivalent form

[Kevin Buzzard]

If the goal is X, then show X, does nothing

[Kevin Buzzard]

if the goal is definitionally equal to X, it changes the goal to X

[Patrick Massot]

I can see it's doing that here. But what's the link with show I usually use?

[Patrick Massot]

which I guess is in term mode

[Kevin Buzzard]

I don't know, this is the only show I use

[Kevin Buzzard]

tactic mode is the bomb

[Patrick Massot]

I use show in arguments to rw and simp for easy stuff I don't want to state and name using have beforehand

[Kevin Buzzard]

Line 190: lemma supp_conj (f g : homeo X X) : supp (conj g f : homeo X X) = g '' supp f := works

[Kevin Buzzard]

i.e. I removed suppp

[Patrick Massot]

Very interesting

[Kevin Buzzard]

You are using f and g to mean two different things, and it guessed you wanted the map not the homeo here

[Kevin Buzzard]

the second suppp could just be removed, but the first one had to be persuaded

[Patrick Massot]

Probably because perm X is also a group

[Patrick Massot]

and Lean doesn't know the group structure on homeo X X is induced as a subgroup of perm X

[Kevin Buzzard]

Then I would like line 196 to be unnecessary (with the ugly (g.to_equiv).inv_fun never appearing)

I don't understand this one. Is there another name for g.to_equiv.inv_fun?

[Patrick Massot]

It's g⁻¹!

[Kevin Buzzard]

You can put show {x : X | conj g f x ≠ x} = {b : X | f (g⁻¹ b) ≠ g⁻¹ b} on line 196 if you like...

[Kevin Buzzard]

but you are complaining about the congr?

[Kevin Buzzard]

You want to prove two sets are equal and you don't want to use congr then funext?

[Patrick Massot]

No I don't complain about congr and funext

[Patrick Massot]

I don't complain at all actually, I try to learn

[Patrick Massot]

I mean I complain that I'm not yet learned

[Patrick Massot]

but I don't complain to anybody but me

[Patrick Massot]

I really don't understand Chris's proof at all

[Patrick Massot]

I can't translate it into tactic mode

[Patrick Massot]

Hence I cannot understand it

[Patrick Massot]

I have a really hard time imagining people actually thinking like this (without first writing the tactic proof and then obfuscate it in term mode)

[Patrick Massot]

I do believe you Chris, but my imagination is failing me

[Kevin Buzzard]

Your comments before the computation seem a bit superficial to me, in the sense that I would not care about any of them myself if they came up in my Lean work.

[Kevin Buzzard]

But the computation is a more serious matter.

[Patrick Massot]

The computation is the actual proof

[Patrick Massot]

everything before the computation is distraction

[Kevin Buzzard]

oh wait

[Kevin Buzzard]

the computation

[Kevin Buzzard]

you write Prop = Prop?

[Kevin Buzzard]

There's no other way?

[Patrick Massot]

yes I write Prop = Prop

[Kevin Buzzard]

Maybe iff would be better with props

[Patrick Massot]

That's because we see sets as map from X to Prop

[Kevin Buzzard]

oh

[Patrick Massot]

So the goal is really Prop = Prop

[Kevin Buzzard]

eew

[Patrick Massot]

because we use funext to get rid of X here

[Kevin Buzzard]

Ok so your question really is something else

[Patrick Massot]

But of course on paper I would write iff

[Kevin Buzzard]

You want to show {x | p x} = {x | q x}

[Patrick Massot]

x is in this set iff .. iff .. iff ... done

[Kevin Buzzard]

I don't think you should use congr and then funext

[Kevin Buzzard]

yes

[Kevin Buzzard]

iff

[Patrick Massot]

Remember {x | p x} is only syntactic sugar for p

[Kevin Buzzard]

sure

[Kevin Buzzard]

but there are lemmas like sets X and Y are equal iff X subseteq Y and Y subseteq X

[Kevin Buzzard]

or whatever

[Chris Hughes]

set.ext is what you're talking about

[Patrick Massot]

Sure, but here I can prove (on paper) direct equality

[Kevin Buzzard]

But you can't prove any of your intermediate steps!

[Kevin Buzzard]

So surely this is an indication that trying to prove p x = q x is a bad idea

[Kevin Buzzard]

I would use set.ext instead of congr, funext

[Kevin Buzzard]

and then try the calc with iff's

[Patrick Massot]

indeed apply set.ext transforms the goal to iff

[Patrick Massot]

But my sorry where there because I couldn't use rw, not because I was proving p x = q x

[Kevin Buzzard]

So what happens if you use set.ext and then try to push the calc through? I can't pass the rw show ∀ b, (g.to_equiv).inv_fun b = g⁻¹ b, from λ b, rfl, line

[Kevin Buzzard]

because I don't really know what's going on

[Patrick Massot]

I don't understand what you don't know

[Kevin Buzzard]

I have never seen congr_n in my life

[Kevin Buzzard]

I don't know what all this rw show business is all about

[Kevin Buzzard]

how is that different to just show

[Kevin Buzzard]

can you just write it for me?

[Patrick Massot]

congr_n 1 is like congr but stops after one step instead of recursing

[Kevin Buzzard]

how do you get from not X iff not Y to X iff Y?

[Patrick Massot]

if the goal is f (a + b) = f (c + d) and you congr_n 1, the new goal will be a+b = c+d. With congr it would become two random goals like a=c and b = d

[Patrick Massot]

In this case f is not

[Patrick Massot]

By the way, I don't know how to get rid of these not once I go to iff instead of =

[Kevin Buzzard]

not_iff_not.2

[Kevin Buzzard]

but there's a catch...

[Kevin Buzzard]

⊢ decidable (f (g⁻¹ x) = g⁻¹ x)

[Kevin Buzzard]

so I hope you are only interested in decidable topological spaces...

[Kevin Buzzard]

;-)

[Andrew Ashworth]

It's funny, as you saw with Adam, most people with a cs background start out in term mode

[Kevin Buzzard]

most people with a maths background think lambda is a real number

[Andrew Ashworth]

I think it's simply familiarity with functional programming concepts

[Andrew Ashworth]

Once you spend enough time looking at term mode statements they really do become more understandable :simple_smile:

[Patrick Massot]

I just found it using find!

[Patrick Massot]

#find (¬ _ ↔ ¬ _) ↔ (_ ↔ _) does work!

[Patrick Massot]

:tada: @Sebastian Ullrich

[Kevin Buzzard]

I found it by guessing what it was called ;-)

[Patrick Massot]

Now what is this decidable crap? I have noncomputable theory local attribute [instance] classical.prop_decidable on top of my file

[Kevin Buzzard]

Even the iff's need some work. I'm beginning to think you were better off with =. but I have to go now, childcare calls

[Patrick Massot]

Why isn't it enough

[Patrick Massot]

I need to sleep actually, I have a train to catch at an insane time tomorrow to go and give a talk about fuzzy maths in Köln

[Patrick Massot]

and why this decidable stuff didn't come up in my = instead of iff stuff?

[Patrick Massot]

Anyway, thank you very much for your help, and thank Chris to

[Patrick Massot]

I have enough food for thought on the train

[Patrick Massot]

Except that I would like to understand how to tell Lean I really don't care about the decidable metaphysics

[Patrick Massot]

@Mario Carneiro is there a global command to say everything should be assumed to have decidable equality?

[Kevin Buzzard]

Is your problem simply that g is not an element of perm X? What happens if you define fp to be the permutation underlying f and gp for g, then use lemmas about groups acting on sets?

[Kevin Buzzard]

All those iff statements are going to follow from standard lemmas about groups acting on sets. I have no idea if they're there already but that is surely the way to finish the job. Groups acting on sets should be in mathlib (I don't know if it's there already) and then all the lemmas should be proved in the same file and then you just apply them and you're home

[Mario Carneiro]

is there a global command to say everything should be assumed to have decidable equality?

local attribute [instance] classical.prop_decidable should do that

[Patrick Massot]

Hum. It turns out I can indeed use apply_instance in both cases. This is the first time I need this tactic in a context where I'm not using example to check whether an instance is working

[Patrick Massot]

Do you understand why apply not_iff_not.2, can spawn those goals without trying apply_instance?

[Mario Carneiro]

What's the context?

[Mario Carneiro]

Also, you should probably use not_congr instead, which doesn't have those extra assumptions

[Mario Carneiro]

I'm currently working on doing what I can with your file

[Mario Carneiro]

I don't think aux_1 is true without assuming f and g are two-sided inverses

[Mario Carneiro]

lemma aux_1 {α : Type*} {β : Type*} {f : α → β} {g : β → α}
  (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f)
  (p : α → Prop) : f '' {a : α | p a} = {b : β | p (g b)} :=
set.ext $ λ b, mem_image_iff_of_inverse h₁ h₂

[Mario Carneiro]

This works for supp_conj:

lemma supp_conj (f g : homeo X X) : supp (conj g f : homeo X X) = g '' supp f :=

[Mario Carneiro]

Here's a proof of supp_conj:

-- should be in equiv.lean
theorem equiv.left_inverse (f : α ≃ β) : left_inverse f.symm f := f.left_inv

theorem equiv.right_inverse (f : α ≃ β) : function.right_inverse f.symm f := f.right_inv

-- should be in homeos.lean
theorem homeo.left_inverse (f : homeo α β) : left_inverse f.symm f := f.left_inv

theorem homeo.right_inverse (f : homeo α β) : function.right_inverse f.symm f := f.right_inv

theorem homeo.bijective (f : homeo α β) : bijective f := f.to_equiv.bijective

@[simp] theorem aut_mul_val (f g : homeo α α) (x) : (f * g) x = f (g x) :=
homeo.comp_val _ _ _

@[simp] theorem aut_one_val (x) : (1 : homeo α α) x = x := rfl

@[simp] theorem aut_inv (f : homeo α α) : f⁻¹ = f.symm := rfl

lemma supp_conj (f g : homeo X X) : supp (conj g f : homeo X X) = g '' supp f :=
begin
  unfold supp,
  rw homeo.image_closure,
  congr_n 1,
  apply set.ext (λ x, _),
  rw mem_image_iff_of_inverse g.left_inverse g.right_inverse,
  apply not_congr,
  dsimp [conj],
  exact calc
     (g * f * g⁻¹) x = x
        ↔ g⁻¹ (g (f (g⁻¹ x))) = g⁻¹ x : by simp [(g⁻¹).bijective.1.eq_iff]
    ... ↔ (f (g⁻¹ x)) = g⁻¹ x : by rw [← aut_mul_val, mul_left_inv]; simp
end

[Patrick Massot]

A million thanks!

[Patrick Massot]

This looks very nice

[Patrick Massot]

Right now I'm at the train station typing on my phone but I'll try this on the train

[Patrick Massot]

Question about stuff you indicated as belonging to homeos.lean: are those restatements needed because of modeling mistakes I made or is it normal? I don't mind having them but I try to understand how to do things right.

[Mario Carneiro]

It is normal. Since you have a coe_fn instance for homeo, the coercion there is not written by composing other coercions so you have to restate theorems about the underlying function if you want them as simp lemmas or projections

[Mario Carneiro]

I put all the stuff together and PR'd it to your repo: https://github.com/PatrickMassot/lean-scratchpad/pull/1

[Patrick Massot]

Should I remove this coercion and have a coercion to equiv?

[Mario Carneiro]

I think it is okay, especially if you expect it will get a lot of use. Otherwise the arrows can pile up

[Patrick Massot]

Ok. Thank you very much

[Patrick Massot]

I even managed to merge using the crappy train station wifi

[Mario Carneiro]

let me know if you want an explanation on something I did there

[Kevin Buzzard]

I tried to describe my problems in https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20vs.20class/near/124574243 without code, and then I posted link to my actual code. Then I tried to describe a simplified problem. I don't what I could do better to ask for help

Write a MWE. I am much more inclined to look at code if I can just cut and paste it and it works first time. Git cloning and then downloading a new mathlib and building everything was a PITA and I couldn't possibly answer a question of the form "why does line 193 not work" without doing all that.

[Kevin Buzzard]

I even managed to merge using the crappy train station wifi

git is great for that isn't it.

[Kevin Buzzard]

Should I remove this coercion and have a coercion to equiv?

It seemed to me that one problem was you had coes from homeo to perm, from perm to fun and from homeo to fun. You had set it up so that the two maps from homeo to fun were definitionally equal (and if they weren't it would surely have been a nightmare) but even with definitional equality this didn't help with rw. @Mario Carneiro Can there be some version of rw which takes definitonal equality into account? i.e. "the user said rw (proof of X = Y) and I can't find X in the goal so I'll now start trying to find some term in the goal which is definitionally equal to X"?

[Chris Hughes]

I've read erw does that, but I've never managed to use it.