Rewrite outside first

Stream: general

[Michael Swan]

If I have a goal of the form:

f x = f (f x)

and I would like to rewrite that outer f on the right-hand side, how can that be done? It seems that whenever I do rw [f] it will only ever perform this operation on either the left-hand side or the inner most function application on the right-hand side but never the outer invocation. nth_rewrite i [f] also doesn't allow me to rewrite that specific use of f for any index I provide.

[Adam Topaz]

You could use conv mode (possibly with the fancy new widget) to select which f to rewrite explicitly

[Michael Swan]

Okay, I’ll experiment with that

[Matt Diamond]

I'm surprised you can't get nth_rewrite to do the job... this seems to work for me:

import Mathlib.Tactic.NthRewrite

example {α : Type} (f g : α → α) (hf : f = g) (x : α): f x = f (f x) := by
  nth_rewrite 2 [hf]
  -- goal is now f x = g (f x)

[Matt Diamond]

maybe there's something about the particulars of your case that are interfering... in that case I suppose conv will do the trick, as Adam said

[Adam Topaz]

If you could give a #mwe that would be great, if you still need help

[Michael Swan]

Yeah nth_rewrite doesn't work for my problem, here is a minimal example:

import Mathlib

inductive code : Type
| seq (c1 c2: code)
| skip
open code

def right_append_seq (c1 c2: code) : code :=
  match c1 with
  | seq c1' c2' => seq c1' (right_append_seq c2' c2)
  | _           => seq c1 c2

def right_assoc_seq : code -> code
| seq (seq c1 c2) c3 => right_append_seq (right_assoc_seq c1) (right_append_seq (right_assoc_seq c2) (right_assoc_seq c3))
| seq c1 c2 => right_append_seq (right_assoc_seq c1) (right_assoc_seq c2)
| c => c

theorem right_assoc_seq_idempotent : ∀ c, right_assoc_seq c = right_assoc_seq (right_assoc_seq c) := by
  intros c
  induction c with
  | seq c1 c2 h1 h2 => nth_rewrite 2 [right_assoc_seq] -- Here is where things fail.

[Michael Swan]

I am trying to expand that outer-most right_assoc_seq but that does not appear to be an option.

[Kim Morrison]

What are you expecting it to expand to? Lean can't see yet which of the branches of the definition of right_assoc_seq applies here.

[Kim Morrison]

(Note that the third branch c => c only applies for c = skip.)

[Michael Swan]

I expect it to expand into separate goals for each possibility of the inner (right_assoc_seq c) expression, which I guess perhaps that means I should do induction/cases on that expression?

[Michael Swan]

I guess I should just expand the inner and then the outer and that might be the only way to do anything with this.

[Kyle Miller]

This seems to unfold the outer one and split into three cases:

theorem right_assoc_seq_idempotent : ∀ c, right_assoc_seq c = right_assoc_seq (right_assoc_seq c) := by
  intros c
  induction c with
  | skip => sorry
  | seq c1 c2 h1 h2 =>
    conv_rhs => unfold right_assoc_seq
    split
    -- three goals

[Michael Swan]

Yeah, I'm going to need to rethink what I'm doing. I think there is a saner way to solve this than what I was attempting to do. Starting this proof with intros c; induction (right_assoc_seq c) seems to get me way farther than intros c; induction c