const_comp

Stream: new members

[Nicolò Cavalleri]

Suppose that, in a proof, I find the following ({A : Type*} {B : Type*} {C : Type*} (c : C) (f : A → B))

(λ b : B, c) ∘ f

in the goal. Simp does not simplify it to (λ a : A, c). Library_search does not find an existing lemma for this but tells me it is true by rfl. In order to simplify it, should I define a lemma

@[simp] lemma comp_const {A : Type*} {B : Type*} {C : Type*} (c : C) (f : A → B) : (λ b : B, c) ∘ f = (λ a : A, c)
  := rfl

or am I supposed to use some kind of tactic that simplifies things true by definition that I am not aware of?

[Anatole Dedecker]

Have you tried dsimp ?

[Nicolò Cavalleri]

Yeah and it does not work as much as simp (even if I am not sure when I should try simp and when dsimp)

[Kevin Buzzard]

I am certainly not an expert in simp but I will note that proving lemmas with rfl because simp needs to know about them is certainly not uncommon in the library -- it happens all the time in data.complex.basic for example.

[Kevin Buzzard]

The difference between simp and dsimp is that dsimp will only apply simp lemmas whose proof is rfl, so it preserves definitional equality, whereas simp is just a general confluent rewriting system; it will know add_zero and zero_add, even though (at least on nat) only one of these is definitional.

[Anatole Dedecker]

Oh just throwing random ideas, but sometimes unfolding function.comp helps with tactics.

[Patrick Massot]

We can only help you if you provide an actual #mwe.

[Reid Barton]

In general ∘ is not used heavily, so it doesn't surprise me much that this lemma would be absent

[Nicolò Cavalleri]

Patrick Massot said:

We can only help you if you provide an actual #mwe.

Well my question was a general question about rfl lemmas, I am not interested specifically in this example, but if you want to try this case any toy example should work (I do not include my original proof because it is exagerately complicated to illustrate this example), for instance:

import topology.basic

@[simp] lemma const_comp {A : Type*} {B : Type*} {C : Type*} (c : C) (f : A → B) : (λ b : B, c) ∘ f = (λ a : A, c)
  := rfl

@[simp] lemma comp_const {A : Type*} {B : Type*} {C : Type*} (b : B) (f : B → C) : f ∘ (λ a : A, b) = (λ a : A, f b)
  := rfl

lemma test {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
begin
  simp, /- Seems not to work for me without the lemmas above -/
  exact continuous_const,
end

[Kevin Buzzard]

Lean works best if you keep things simple so Lean has less trouble working out what to unfold and what to leave alone. f \circ g can be expressed as lam x, f(g(x)) and probably the latter is preferred because more primitive notions are involved.

[Reid Barton]

The easier way is just to eliminate function composition, like Kevin suggests

import topology.basic

lemma test {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
begin
  simp [(∘)],
  exact continuous_const,
end

[Sebastien Gouezel]

lemma test {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
begin
  dsimp,
  exact continuous_const,
end

[Nicolò Cavalleri]

Sebastien Gouezel said:

lemma test {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
begin
  dsimp,
  exact continuous_const,
end

I tried dsimp before and it does not work for me! Are you including any import other than topology.basic?

[Patrick Massot]

One option here would be to get lazy people to PR their stuff, for instance https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/topology.lean#L36-L39

[Patrick Massot]

Another option is to fix some stupid binders in mathlib

[Patrick Massot]

In the mean time you can use the proof term @continuous_const _ _ _ _ b, (without any tactic)

[Patrick Massot]

A priori having b implicit in continuous_const goes against all rules. But indeed it is tempting since it's almost always clear from context.

[Reid Barton]

I feel like it would actually be easy to improve the unifier to handle this problem

[Patrick Massot]

Of course improving elaboration could also solve this issue, but it's a different game

[Patrick Massot]

In case my messages are unclear, I mean:

import topology.basic

lemma continuous_of_const {α : Type*} {β : Type*}
  [topological_space α] [topological_space β]
  {f : α → β} (h : ∀a b, f a = f b) :
  continuous f :=
λ s _, by convert @is_open_const _ _ (∃ a, f a ∈ s); exact
  set.ext (λ a, ⟨λ fa, ⟨_, fa⟩,
    λ ⟨b, fb⟩, show f a ∈ s, from h b a ▸ fb⟩)

example {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
@continuous_const _ _ _ _ b

example {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
continuous_of_const (by simp)

[Nicolò Cavalleri]

Reid Barton said:

The easier way is just to eliminate function composition, like Kevin suggests

import topology.basic

lemma test {X : Type*} [topological_space X] (a :X)
{Y : Type*} [topological_space Y] (b : Y)
(f : X → Y) : continuous ((λ y : Y, b) ∘ f ∘ (λ x : X, a)) :=
begin
  simp [(∘)],
  exact continuous_const,
end

Ok thanks this makes sense! I mean sometimes compositions (as \circ) just appear in proofs themselves alone without me ever defining something with them (meaning something is defined in terms of them in Mathlib), so I was really looking for a method that works when compositions appear and I guess this would be a standard way to get rid of \circs

[Patrick Massot]

This is very sad for mathematicians, but Lean doesn't really like composition.

[Nicolò Cavalleri]

Patrick Massot said:

In the mean time you can use the proof term @continuous_const _ _ _ _ b, (without any tactic)

This also works but I feel like simp [(∘)] is more scalable (for example in my original proof I did not have a tactic that could close the goal immediately and I just needed to simplify a very complicated expression)

[Patrick Massot]

Nicolò Cavalleri said:

Patrick Massot said:

We can only help you if you provide an actual #mwe.

Well my question was a general question about rfl lemmas, I am not interested specifically in this example, but if you want to try this case any toy example should work (I do not include my original proof because it is exagerately complicated to illustrate this example), for instance:

Did you notice the effect of posting a #mwe?

[Sebastien Gouezel]

Nicolò Cavalleri said:

I tried dsimp before and it does not work for me! Are you including any import other than topology.basic?

I am not able to reproduce what I did. And indeed it doesn't work!

[Reid Barton]

Note the effect of not posting a #mwe...

[Nicolò Cavalleri]

Reid Barton said:

Note the effect of not posting a #mwe...

I am confused! Why is what I posted not a mwe?

[Jalex Stark]

did you read the definition at the #mwe link? Ah I see you eventually posted working code

[Reid Barton]

Was replying to Sebastien.

[Nicolò Cavalleri]

Reid Barton said:

Was replying to Sebastien.

Oh ok sorry!

[Nicolò Cavalleri]

Jalex Stark said:

did you read the definition at the #mwe link?

Yes I did! I believe it was a mwe...

[Anatole Dedecker]

Less interesting that the working example with simp, but in this case you can simply replace it with unfold function.comp

[Nicolò Cavalleri]

Sebastien Gouezel said:

Nicolò Cavalleri said:

I tried dsimp before and it does not work for me! Are you including any import other than topology.basic?

I am not able to reproduce what I did. And indeed it doesn't work!

Maybe it was because you did not comment out the two simp lemmas I wrote and dsimp used them!

[Jalex Stark]

Nicolò Cavalleri said:

Jalex Stark said:

did you read the definition at the #mwe link?

Yes I did! I believe it was a mwe...

patrick was trying to point out that your first post didn't have working code, so you got imprecise answers, and then when you eventually posted working code, ou got more precise answers. I think patrick was trying to suggest that you should start with a working example in the future

[Anatole Dedecker]

I actually tend to unfold function.comp really often because composition really blocks things sometimes

[Anatole Dedecker]

Jalex Stark said:

Nicolò Cavalleri said:

Jalex Stark said:

did you read the definition at the #mwe link?

Yes I did! I believe it was a mwe...

patrick was trying to point out that your first post didn't have working code, so you got imprecise answers, and then when you eventually posted working code, ou got more precise answers. I think patrick was trying to suggest that you should start with a working example in the future

He wasn't replying to Patrick's post I think

[Nicolò Cavalleri]

Anatole Dedecker said:

I actually tend to unfold function.comp really often because composition really blocks things sometimes

Ok thanks I will keep this in mind!

[Kevin Buzzard]

It's surprising -- function.comp seems like a really natural thing, but it's just adding some "extra step" which Lean then has to unravel. This sort of phenomenon shows up everywhere. We like to package things up because it makes stuff neater, but not too much because how does Lean know what to unpack? It's not so obvious. Say Lean has a question about the real numbers. Should it unfold the definition of the real numbers and consider the equivalence class of Cauchy sequences? Almost certainly not! But should it unfold function composition? Maybe, maybe not. Humans are so good at this sort of thing. Machines are quite dumb. A lot of effort has gone into giving users access to various ways to give Lean hints about what to unfold when but it's still a hard problem.

[Nicolò Cavalleri]

Kevin Buzzard said:

It's surprising -- function.comp seems like a really natural thing, but it's just adding some "extra step" which Lean then has to unravel. This sort of phenomenon shows up everywhere. We like to package things up because it makes stuff neater, but not too much because how does Lean know what to unpack? It's not so obvious. Say Lean has a question about the real numbers. Should it unfold the definition of the real numbers and consider the equivalence class of Cauchy sequences? Almost certainly not! But should it unfold function composition? Maybe, maybe not. Humans are so good at this sort of thing. Machines are quite dumb. A lot of effort has gone into giving users access to various ways to give Lean hints about what to unfold when but it's still a hard problem.

Is it not possible to modify simp so that it always unfolds composition when it sees it?

[Reid Barton]

It is possible but is it a good idea?

[Reid Barton]

If you always want to unfold composition in simp then why not just write the unfolded version in the first place?

[Reid Barton]

then you also handle situations where you don't use simp

[Nicolò Cavalleri]

Reid Barton said:

If you always want to unfold composition in simp then why not just write the unfolded version in the first place?

Because it's much harder to read long statement full of lambda expressions for a mathematician when it is easier to read it with compositions!

[Nicolò Cavalleri]

II mean composition is easier to process instantaneously for humans

[Nicolò Cavalleri]

And it makes statements more elegant and more symmetric being similar to a group operation as far as notation is concerned

[Kevin Buzzard]

If you want to put \circ into results because you think it adds to readability, then just start your proofs with simp only [(\circ)].

[Jalex Stark]

at some point you have to bridge the gap between what a human can read and what a computer can read

[Kevin Buzzard]

The whole simp theory is very well-understood by computer scientists, it goes under the name of confluent rewriting systems. One idea is that things should be in some kind of normal form. Normal forms are decided, perhaps by computer scientists. At some point it was decided that function.comp wasn't part of the story. From a mathematician's perspective some of these decisions can be difficult to understand, especially if you're focussed on human-readability (and if you've looked at some of mathlib you'll know that not everyone here is). But simp is an amazing tool, and as someone who doesn't understand it I just accept how it's set up and learn how to use it. Perhaps an even better approach would be to understand it properly and then try and figure out how to add function.comp to the picture.

[Nicolò Cavalleri]

Kevin Buzzard said:

The difference between simp and dsimp is that dsimp will only apply simp lemmas whose proof is rfl, so it preserves definitional equality, whereas simp is just a general confluent rewriting system; it will know add_zero and zero_add, even though (at least on nat) only one of these is definitional.

Do you know if there is a way to get the output of dsimp as with squeeze_simp for simp?

[Nicolò Cavalleri]

(I would guess squeeze_simp should produce it but it happened to me in the past that dsimp did something when simp could not do anything: I cannot easily ricreate a mwe of this right now but I can try to do it if you have no idea about what I am talking about)

[Kevin Buzzard]

I don't think there's a squeeze_dsimp. Note however that if dsimp changes your goal to X then you can replace the call to dsimp with change X or show X (they are the same), because change and show will change a goal from Y to X if Y and X are definitionally equivalent.

[Bhavik Mehta]

You could also use the trace output for simplify to get this, but I also do what Kevin suggests here

[Nicolò Cavalleri]

Bhavik Mehta said:

You could also use the trace output for simplify to get this, but I also do what Kevin suggests here

Thanks! What is the syntax for this?

[Bryan Gin-ge Chen]

set_option trace.simplify true or set_option trace.simplify.rewrite true for just the successful rewrites. See https://leanprover-community.github.io/extras/simp.html