Zulip Chat Archive

Stream: maths

Topic: homeo equiv etc.


view this post on Zulip Patrick Massot (Apr 03 2018 at 21:08):

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

view this post on Zulip Patrick Massot (Apr 03 2018 at 21:09):

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

view this post on Zulip Patrick Massot (Apr 03 2018 at 21:10):

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)

view this post on Zulip Patrick Massot (Apr 03 2018 at 21:11):

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

view this post on Zulip Patrick Massot (Apr 03 2018 at 21:12):

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

view this post on Zulip Patrick Massot (Apr 03 2018 at 21:13):

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).

view this post on Zulip Chris Hughes (Apr 03 2018 at 21:20):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:23):

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)?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:28):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:29):

You define suppp f to be supp f?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:30):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:30):

Yes, that definition is part of the problem

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:30):

I couldn't avoid it

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:33):

It's part of coercion/extension hell

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:33):

supp is defined on functions from X to X

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:34):

homeos have coercions to functions

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:34):

but it's not enough

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:34):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:35):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:36):

It's just too hard to make it work.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:36):

I have mathlib not compiling.

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:36):

make what work?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:36):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:37):

(only handling a renamed lemma)

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:40):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:40):

those are old stuff irrelevant here

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:40):

they are not updated

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:40):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:40):

Everything imported in support.lean is ok

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:41):

OK it now compiles. What's the question?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:41):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:42):

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

view this post on Zulip Chris Hughes (Apr 05 2018 at 20:44):

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

view this post on Zulip Chris Hughes (Apr 05 2018 at 20:47):

(deleted)

view this post on Zulip Chris Hughes (Apr 05 2018 at 20:48):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:49):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:49):

The issue is that you are using coe everywhere?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:50):

What do you mean using coe everywhere?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:50):

I need homeomorphisms to be able to act as functions

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:50):

So yes, they coerce to functions

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:50):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:52):

I have no idea

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:52):

Clearly there is something I'm doing wrong

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:52):

I only want to learn how to do it right

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:54):

ambiguous overload, possible interpretations
  right_inverse
  function.right_inverse

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:54):

where do you see that?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:54):

when I write #check right_inverse

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:55):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:55):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:55):

Is there an easy way to do that?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:55):

This is something I wonder all the time

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:55):

it seems the answer is no

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:55):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:58):

So what is (g.to_equiv).to_fun?

view this post on Zulip Mario Carneiro (Apr 05 2018 at 20:58):

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"

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:58):

he said lots of things

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:58):

maybe there were lots of errors :-)

view this post on Zulip Mario Carneiro (Apr 05 2018 at 20:59):

Could you at least post the error message?

view this post on Zulip Mario Carneiro (Apr 05 2018 at 20:59):

(s)

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:59):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:59):

Because I'm clearly going against Lean

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:59):

Are you being anti-idiomatic?

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:59):

Not writing idiomatic Lean

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:00):

exactly

view this post on Zulip Mario Carneiro (Apr 05 2018 at 21:00):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:01):

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.

view this post on Zulip Chris Hughes (Apr 05 2018 at 21:01):

@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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:01):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:01):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:02):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:02):

I'm honestly asking

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:02):

So what is (g.to_equiv).to_fun?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:03):

It's the function underlying the homeomorphism g

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:03):

for g : homeo X X

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:03):

But it goes through two conversions

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:03):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:03):

When you write g '' ...

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:03):

what do you think happens there?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:03):

That's mathlib notation for image of a subset

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:04):

Lean does figure out the coercions here

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:04):

set.image so it takes a function

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:04):

and which function does it take?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:05):

Is there some coe directly from homeo to the function?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:05):

(g.to_equiv).to_fun

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:05):

yes

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:05):

That's what it uses?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:05):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:05):

is defined in homeos.lean

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:06):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:06):

This is a funny error message then:

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:06):

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}

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:06):

Is it definitionally the same?

view this post on Zulip Chris Hughes (Apr 05 2018 at 21:07):

rw doesn't do definitionally equal things.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:07):

oh yeah

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:07):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:07):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:08):

Chris points out the problem

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:08):

Yes, I understand this is the problem with the rewrite

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:08):

definitionally equivalent is not enough

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:08):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:09):

without doing this swap, exact ... thing

view this post on Zulip Chris Hughes (Apr 05 2018 at 21:09):

Never use ( g.to_equiv).to_fun?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:09):

I don't write this myself

view this post on Zulip Chris Hughes (Apr 05 2018 at 21:09):

I usually use show otherwise.

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:09):

it only appears in goals and error messages

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:10):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:10):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:10):

and wrote everything out in full

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:10):

How do you do it in tactic mode?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:10):

show works in tactic mode

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:11):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:11):

show _ ≠ _ :-)

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:11):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:12):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:12):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:12):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:14):

There must be a better way

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:14):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:15):

the real world doesn't use dependent type theory

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:15):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:15):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:16):

with their silly pedantic fussing

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:16):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:16):

works for 193 ;-)

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:18):

I don't understand what show does here

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:18):

Usually I need to supply a proof after show

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:19):

it rewrites the goal into a definitionally equivalent form

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:19):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:19):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:19):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:19):

which I guess is in term mode

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:19):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:19):

tactic mode is the bomb

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:20):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:23):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:24):

i.e. I removed suppp

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:24):

Very interesting

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:24):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:25):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:25):

Probably because perm X is also a group

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:26):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:28):

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?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:28):

It's g⁻¹!

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:32):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:32):

but you are complaining about the congr?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:33):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:34):

No I don't complain about congr and funext

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:36):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:36):

I mean I complain that I'm not yet learned

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:36):

but I don't complain to anybody but me

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:37):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:38):

I can't translate it into tactic mode

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:38):

Hence I cannot understand it

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:38):

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)

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:39):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:40):

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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:40):

But the computation is a more serious matter.

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:41):

The computation is the actual proof

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:41):

everything before the computation is distraction

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:42):

oh wait

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:42):

the computation

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:42):

you write Prop = Prop?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:42):

There's no other way?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:42):

yes I write Prop = Prop

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:42):

Maybe iff would be better with props

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:43):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:43):

oh

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:44):

So the goal is really Prop = Prop

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:44):

eew

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:44):

because we use funext to get rid of X here

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:44):

Ok so your question really is something else

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:44):

But of course on paper I would write iff

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:44):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:45):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:45):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:45):

yes

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:45):

iff

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:45):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:45):

sure

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:45):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:46):

or whatever

view this post on Zulip Chris Hughes (Apr 05 2018 at 21:46):

set.ext is what you're talking about

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:46):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:46):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:47):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:48):

I would use set.ext instead of congr, funext

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:48):

and then try the calc with iff's

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:48):

indeed apply set.ext transforms the goal to iff

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:49):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:51):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:51):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:52):

I don't understand what you don't know

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:52):

I have never seen congr_n in my life

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:52):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:52):

how is that different to just show

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:53):

can you just write it for me?

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:53):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:54):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:54):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:54):

In this case f is not

view this post on Zulip Patrick Massot (Apr 05 2018 at 21:56):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:57):

not_iff_not.2

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:57):

but there's a catch...

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:57):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:57):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:57):

;-)

view this post on Zulip Andrew Ashworth (Apr 05 2018 at 21:58):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:58):

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

view this post on Zulip Andrew Ashworth (Apr 05 2018 at 21:59):

I think it's simply familiarity with functional programming concepts

view this post on Zulip Andrew Ashworth (Apr 05 2018 at 21:59):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:00):

I just found it using find!

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:00):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:00):

:tada: @Sebastian Ullrich

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 22:01):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:02):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 22:02):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:02):

Why isn't it enough

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:02):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:03):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:04):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:06):

I have enough food for thought on the train

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:06):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 22:07):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 22:33):

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?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 22:38):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 03:42):

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

local attribute [instance] classical.prop_decidable should do that

view this post on Zulip Patrick Massot (Apr 06 2018 at 04:30):

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

view this post on Zulip Patrick Massot (Apr 06 2018 at 04:31):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:35):

What's the context?

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:36):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:36):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:37):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:37):

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₂

view this post on Zulip Mario Carneiro (Apr 06 2018 at 04:40):

This works for supp_conj:

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 05:23):

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

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:36):

A million thanks!

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:36):

This looks very nice

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:37):

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

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:40):

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.

view this post on Zulip Mario Carneiro (Apr 06 2018 at 05:43):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 05:45):

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

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:48):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 05:49):

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

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:55):

Ok. Thank you very much

view this post on Zulip Patrick Massot (Apr 06 2018 at 05:55):

I even managed to merge using the crappy train station wifi

view this post on Zulip Mario Carneiro (Apr 06 2018 at 05:58):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 10:37):

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.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 10:39):

I even managed to merge using the crappy train station wifi

git is great for that isn't it.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 10:42):

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"?

view this post on Zulip Chris Hughes (Apr 06 2018 at 10:46):

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


Last updated: May 11 2021 at 16:22 UTC