## Stream: Is there code for X?

### Topic: iterate.comm

#### Damiano Testa (Apr 08 2021 at 16:14):

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 (Apr 08 2021 at 16:21):

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 (Apr 08 2021 at 16:38):

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

PR #7121

#### Bryan Gin-ge Chen (Apr 08 2021 at 18:33):

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

#### Damiano Testa (Apr 08 2021 at 18:34):

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 (Apr 08 2021 at 18:42):

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

#### Bryan Gin-ge Chen (Apr 08 2021 at 18:47):

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 (Apr 08 2021 at 18:48):

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 (Apr 08 2021 at 18:49):

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!

#### Yakov Pechersky (Apr 08 2021 at 18:50):

It's commutativity of multiplication in the group of endos

#### Damiano Testa (Apr 08 2021 at 18:50):

No worries! I find it somewhat confusing myself.

#### Yakov Pechersky (Apr 08 2021 at 18:51):

function.commute is missing a helper lemma about application

#### Damiano Testa (Apr 08 2021 at 18:52):

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 (Apr 08 2021 at 18:52):

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

#### Yakov Pechersky (Apr 08 2021 at 18:59):

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 (Apr 08 2021 at 19:00):

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 (Apr 08 2021 at 19:02):

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

Or something

#### Yakov Pechersky (Apr 08 2021 at 19:03):

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

#### Damiano Testa (Apr 08 2021 at 19:03):

Ok, let me try! Thanks a lot!

#### Yakov Pechersky (Apr 08 2021 at 19:03):

And there, you're using that projection notation

#### Yakov Pechersky (Apr 08 2021 at 19:04):

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

#### Damiano Testa (Apr 08 2021 at 19:06):

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 (Apr 08 2021 at 19:07):

Yes, you're using the defeq of h there

#### Damiano Testa (Apr 08 2021 at 19:07):

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 (Apr 08 2021 at 19:07):

Indeed, I unfolded twice before I removed them.

#### Yakov Pechersky (Apr 08 2021 at 19:07):

The defeq is via the definition of semiconj

#### Damiano Testa (Apr 08 2021 at 19:08):

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 (Apr 08 2021 at 19:08):

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 (Apr 08 2021 at 19:09):

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

#### Damiano Testa (Apr 08 2021 at 19:10):

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 (Apr 08 2021 at 19:10):

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 (Apr 08 2021 at 19:10):

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

(in my opinion)

#### Damiano Testa (Apr 08 2021 at 19:11):

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

#### Yakov Pechersky (Apr 08 2021 at 19:12):

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 (Apr 08 2021 at 19:14):

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 (Apr 08 2021 at 19:14):

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

#### Alex J. Best (Apr 08 2021 at 21:20):

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 (Apr 08 2021 at 21:31):

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 (Apr 08 2021 at 21:32):

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 (Apr 08 2021 at 22:06):

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

#### Eric Wieser (Apr 08 2021 at 22:08):

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 (Apr 08 2021 at 22:08):

variables (f g : α → α)

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


#### Yakov Pechersky (Apr 08 2021 at 22:09):

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 (Apr 08 2021 at 22:10):

Or just #check

#### Yakov Pechersky (Apr 08 2021 at 22:10):

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 (Apr 08 2021 at 22:10):

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


#### Eric Wieser (Apr 08 2021 at 22:10):

I mean, add an x in that check

#### Yakov Pechersky (Apr 08 2021 at 22:11):

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

#### Eric Wieser (Apr 08 2021 at 22:14):

To be clear, I meant

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


#### Eric Wieser (Apr 08 2021 at 22:14):

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

#### Eric Wieser (Apr 08 2021 at 22:15):

So maybe a doc-gen solution is needed here?

#### Yakov Pechersky (Apr 08 2021 at 22:18):

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 (Apr 08 2021 at 22:41):

What does h x now produce?

#### Eric Wieser (Apr 08 2021 at 22:41):

(for perm.disjoint)

#### Yakov Pechersky (Apr 09 2021 at 00:08):

An error, _root_.disjoint expects a set membership prop

#### Damiano Testa (Apr 09 2021 at 01:36):

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 (Apr 09 2021 at 04:58):

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 (Apr 09 2021 at 04:59):

I don't know which direction is better.

#### Damiano Testa (Apr 09 2021 at 05:01):

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

#### Damiano Testa (Apr 09 2021 at 05:38):

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 (Apr 09 2021 at 06:38):

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 (Apr 09 2021 at 06:49):

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

#### Gabriel Ebner (Apr 09 2021 at 06:51):

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 (Apr 09 2021 at 06:58):

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 (Apr 09 2021 at 07:02):

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

Last updated: May 07 2021 at 23:11 UTC