iterate.comm

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I think that this lemma is not part of logic/function/iterate. If it is not there, do you think that it would be a good idea to add it?

Thanks!

lemma comm {m n : ℕ} : f^[n]^[m] = (f^[m]^[n] : α → α) :=
begin
  rw [← iterate_mul, nat.mul_comm, iterate_mul],
end

[Alex J. Best]

Seems reasonable, I wonder if we should establish a simp-normal form for these sorts of things though, I see there is docs#function.iterate_add and docs#function.iterate_mul both of which insert more iteration symbols rather than arithmetic operations on nats neither of which is @[simp] though, so I would think adding the symm of those lemmas as simp lemmas would help when working with an expression like this.

[Yakov Pechersky]

I don't agree that the symm of those is the right direction for simp. There are basically no lemmas about f^[2], for example. But if you splat it out, you're more likely to have lemmas about application or composition

[Damiano Testa]

PR #7121

[Bryan Gin-ge Chen]

Just noticed docs#function.commute.iterate_iterate_self which seems related.

[Damiano Testa]

I do not know much about what the best for formalization would be, but my instinct would be to transfer everything to the "exponents" and then act there. So, I would have formulated iterate_add and iterate_mul in reverse order to the current one. Since Yuri made this choice, I am probably wrong!

[Damiano Testa]

Bryan, the statement that you mention seems indeed very close, but I am failing to use it...

[Bryan Gin-ge Chen]

Right, I'm not sure how commute is supposed to be used, but it looks like there's some useful API around it.

[Damiano Testa]

I've gotten to having to prove f^[n]^[m] x = f^[n] (f^[m] x), but I am struggling to make progress.

[Damiano Testa]

Wait, that is equivalent to f^[n * m] x = f^[n + m] x: this is not what I want! No wonder I was not making progress!

Bryan, I think that the one that you mention is addition of exponents, not multiplication!

[Bryan Gin-ge Chen]

Ah, sorry about that!

[Yakov Pechersky]

It's commutativity of multiplication in the group of endos

[Damiano Testa]

No worries! I find it somewhat confusing myself.

[Yakov Pechersky]

function.commute is missing a helper lemma about application

[Damiano Testa]

Yakov, I would like to understand better your last statement: would you mind expanding a bit and giving me a hint as to what kind of lemma you are thinking of?

[Damiano Testa]

I would be happy to add it to my "one-lemma PR"!

[Yakov Pechersky]

You have, via function.comm that the composition of f and g is the same as composing g and f. congr_fun with that equality gives you that for all x, (f o g) x = (g o f) x

[Yakov Pechersky]

So you have the tools now to make the proof you need. You can use apply congr_fun to generalize over whatever you're applying on. The helper lemma would just state that directly, something like

[Yakov Pechersky]

function.commute.apply (h : function.commute f g) (x : a) : g (f x) = f (g x) := congr_fun h x

[Yakov Pechersky]

Or something

[Yakov Pechersky]

Then your proof becomes (function.commute.iterate_iterate_self f m n).apply x

[Damiano Testa]

Ok, let me try! Thanks a lot!

[Yakov Pechersky]

And there, you're using that projection notation

[Yakov Pechersky]

Does that make sense? We're constructing a proposition and right away using a lemma about it. And because of namespaces, we can use the projection

[Yakov Pechersky]

Ah hold on, your original lemma is about exponentiation. I misunderstood

[Damiano Testa]

Yakov, it turns out, that the proof is your lemma even easier! Maybe this is why Yuri did not add it:

lemma function.commute.apply (h : function.commute f g) (x : α) :
  g (f x) = f (g x) :=
(h _).symm

[Yakov Pechersky]

Yes, you're using the defeq of h there

[Damiano Testa]

Yes, I think that the one that I want is not the one that Bryan mentioned, but I still took some time to figure out that it wasn't, so I would like to understand how to better get this things!

[Damiano Testa]

Indeed, I unfolded twice before I removed them.

[Yakov Pechersky]

The defeq is via the definition of semiconj

[Damiano Testa]

here is the non-minimal proof:

lemma function.commute.apply (h : function.commute f g) (x : α) :
  g (f x) = f (g x) :=
begin
  apply congr_fun _ x,
  unfold function.commute at h,
  unfold semiconj at h,
  ext,
  exact (h _).symm,
end

[Yakov Pechersky]

Right. I think it's still nice to provide the API that wraps the defeq operations, just in case someone wants to generalize the definition in a way that defeq no longer works. Others might disagree

[Damiano Testa]

Ok, so you are saying that it is better to have the explicit unfold steps?

[Damiano Testa]

I can see why this proof is probably the "other" candidate:

lemma function.commute.apply (h : function.commute f g) (x : α) :
  g (f x) = f (g x) :=
begin
  unfold function.commute at h,
  unfold semiconj at h,  -- at this stage, h : ∀ (x : α), f (g x) = g (f x)
  exact (h _).symm,
end

[Yakov Pechersky]

Of course, maybe the lemma should be the symm of that. It's not clear a priori which is the "inside" function in commute f g

[Yakov Pechersky]

Ah, I meant for users of the API. In the making of the actual API, it's fine to use defeq

[Yakov Pechersky]

(in my opinion)

[Damiano Testa]

I can add this lemma to the PR, even if it is about "addition" instead of "multiplication".

[Damiano Testa]

(If you think that it would be useful to have: adding "unused" lemmas is rarely an issue with CI building.)

[Yakov Pechersky]

Right. Regarding reduction of exponents: since we're operating solely in the nat monoid, any reduction would lead solely to a growth of the exponent. So it'd be harder to deal with a f^3 than f^2 o f

[Damiano Testa]

I see, so this is why the direction of these lemmas goes in the direction that feels "wrong" to me: thanks for the explanation!

[Yakov Pechersky]

So while the expression is "simpler" with a reduced exponent, it's harder to prove things about it.

[Damiano Testa]

Yakov, I added your function.commute.apply lemma as well!

[Alex J. Best]

Yakov Pechersky said:

Right. Regarding reduction of exponents: since we're operating solely in the nat monoid, any reduction would lead solely to a growth of the exponent. So it'd be harder to deal with a f^3 than f^2 o f

I think this is the key point I was missing here, the example I had in my head of things "cancelling out" when you combine the exponents really can't happen with nat-indexing. So maybe the best form is the version currently there, having a simp-normal form still seems useful though?

[Yakov Pechersky]

Is simp a tactic for proving things or simplifying expressions? If the former, you might want to make the proof you use break the monoidal term by 2s or by 3s, that will lead to fewer rewrites.

[Yakov Pechersky]

We break off by ones because of the nat.succ structure. But execution of a function that has been raised to a nat power is more efficient if you execute by twos, and even more so by threes. But it's harder to write the method to do that.

[Eric Wieser]

Are you sure function.commutes.apply is a useful lemma? Does docs#function.commute really unfold to composition?

[Eric Wieser]

Yeah, if you have a term h : function.commutes f g, h x is syntactically f (g x) = g (f x) - the lemma is pointless

[Yakov Pechersky]

variables (f g : α → α)

#reduce (function.commute f g)
/-
∀ (x : α), f (g x) = g (f x)
-/

[Yakov Pechersky]

When I'm working with a new prop, I don't always know what it reduces to. And to find out here that (h : function.commute f g) x would mean f (g x) = g (f x) would require going down some search path.

[Eric Wieser]

Or just #check

[Yakov Pechersky]

It's not indicated in the docs anywhere. One way to explicitly indicate is just to have a lemma that says exactly what it means.

[Yakov Pechersky]

#check (function.commute f g)
/-
function.commute f g : Prop
-/

[Eric Wieser]

I mean, add an x in that check

[Yakov Pechersky]

Right, one needed to know that that was a valid thing to say in the first place

[Eric Wieser]

To be clear, I meant

variables (h : commute f g) (x)
#check h x

[Eric Wieser]

That's basically a problem for any definition that expands to a function type - eg docs#matrix

[Eric Wieser]

So maybe a doc-gen solution is needed here?

[Yakov Pechersky]

Yes I understand what you meant. This example works because of how commute is defined, and how semiconj is defined. In #7118, I redefine perm.disjoint to be disjoint f.support g.support instead of def disjoint (f g : perm α) := ∀ x, f x = x ∨ g x = x. So previous proofs that used cases (h : disjoint f g) x with hfx hgx won't work straight out of the box. But if there was a disjoint.apply or whatever, it would be stable to the definitional change.

[Eric Wieser]

What does h x now produce?

[Eric Wieser]

(for perm.disjoint)

[Yakov Pechersky]

An error, _root_.disjoint expects a set membership prop

[Damiano Testa]

My experience with the commute issue has been that it took me a while to realise that

variables (h : commute f g) (x)
#check h x

that is, applying h to x, was even a thing. Of course, I did in the end, but I would have liked that this information had been more prominent. As a not so experienced user, I still struggle with seeing through the definitions.

Maybe just a pointer in a doc-string would be enough.

[Yury G. Kudryashov]

Feel free to improve docstrings. About LHS vs RHS in iterate_add etc, AFAIR it was not me who made the choice. I moved these lemmas from nat.iterate_* and did not think about LHS vs RHS.

[Yury G. Kudryashov]

I don't know which direction is better.

[Damiano Testa]

I will not change the direction of the lemmas, but I will make an attempt at doc strings!

[Damiano Testa]

For those interested, I added the second line to the doc string of commute:

/-- Two maps `f g : α → α` commute if `f ∘ g = g ∘ f`.
Given `h : function.commute f g` and `a : α`, the term `h a` has Type `h a : f (g a) = g (f a)`. -/
def commute (f g : α → α) : Prop := semiconj f g g

Any comments are more than welcome! I personally find it very helpful when doc strings give "expected usages", since often definitions are a little opaque.

[Damiano Testa]

Ok, the doc string appears to have generated lots of support!

At the moment, the lemma directly below the definition of commute is

lemma commute.apply {f g : α → α} (h : function.commute f g) (x : α) :
  f (g x) = g (f x) :=
h _

and, given the doc string, I am now leaning towards Eric's idea that this is superfluous: this simply allows to write h.apply x instead of h x.

:thumbs_up: this comment if the lemma should stay. :thumbs_down: this comment if the lemma should go.

[Eric Wieser]

A commute.comp_eq lemma that applies funext might still be a useful addition

[Eric Wieser]

Assuming it doesn't exist already

[Gabriel Ebner]

I believe this lemma (commute.apply) would be useful if you made f (and maybe also g) explicit and put h at the end. Then you could do rw commute.apply f x and get a subgoal for function.commute f g.

[Damiano Testa]

As far as I can see, commute.comp_eq does not exist, but there is a similar one for semiconj (see code below and recall
def commute (f g : α → α) : Prop := semiconj f g g).

Thus, I am tempted to will not introduce commute.comp_eq , but may revive the commute.apply with explicit function(s), if people agree that this is wanted. I personally have not worked much with this API, so I am in no position of judging whether it is useful or not.

/-- We say that `f : α → β` semiconjugates `ga : α → α` to `gb : β → β` if `f ∘ ga = gb ∘ f`. -/
def semiconj (f : α → β) (ga : α → α) (gb : β → β) : Prop := ∀ x, f (ga x) = gb (f x)

namespace semiconj

variables {f fab : α → β} {fbc : β → γ} {ga ga' : α → α} {gb gb' : β → β} {gc gc' : γ → γ}

protected lemma comp_eq (h : semiconj f ga gb) : f ∘ ga = gb ∘ f := funext h

[Yury G. Kudryashov]

If you have h : commute f g, then you have h.comp_eq. It unfolds commute to semiconj, then applies semiconj.comp_eq.