# Zulip Chat Archive

## Stream: general

### Topic: noob tactic question(s)

#### Johan Commelin (Apr 17 2020 at 17:27):

Without providing a MWE, I hope that the experts can quickly help me back on track.

meta def replace_target_lhs (rw : tracked_rewrite) : tactic unit := do (r, lhs, rhs) ← target_lhs_rhs, (new_lhs, prf) ← rw.eval, replace_target_side ``(r %%new_lhs %%rhs) ``(λ L, %%r L %%rhs) prf

I've decomposed the target into `(r, lhs, rhs)`

where `r`

is the `name`

of a relation. Out of a black box I have procured an expression `new_lhs`

. And now I want to substitute the `new_lhs`

for the old `lhs`

.

My problems is, Lean doesn't seem to like

``(r %%new_lhs %%rhs)

What is the right syntax here?

#### Johan Commelin (Apr 17 2020 at 17:35):

Is there some sort of antiquotation for names?

(I also tried ```(apply %%new_lhs %%rhs)`

but that didn't seem to help either.)

#### Rob Lewis (Apr 17 2020 at 18:12):

What do you know about `r`

? Can you assume it has no universe parameters and no implicit arguments? And do you really want to give `pexpr`

s to `replace_target_side`

?

#### Rob Lewis (Apr 17 2020 at 18:12):

If the answers are "no," you probably want to use the tactic`mk_app r [new_lhs, rhs]`

.

#### Rob Lewis (Apr 17 2020 at 18:15):

Something like ` ``(%%(expr.const r [] : pexpr) %%new_lhs %%rhs)`

will avoid calling the elaborator, but notice that it's returning a pexpr and you're telling it that `r`

takes no universe parameters.

#### Johan Commelin (Apr 17 2020 at 18:21):

Well I guess I want to support the case where `r`

is either `=`

or `\iff`

.

#### Johan Commelin (Apr 17 2020 at 18:21):

So now I'm trying

meta def replace_target_lhs (rw : tracked_rewrite) : tactic unit := do (r, lhs, rhs) ← target_lhs_rhs, (new_lhs, prf) ← rw.eval, e ← mk_app r [new_lhs, rhs], replace_target_side e ``(λ L, %%r L %%rhs) prf

#### Johan Commelin (Apr 17 2020 at 18:21):

But it doesn't like the `e`

in the last line, because it expects a `pexpr`

instead of an `expr`

#### Johan Commelin (Apr 17 2020 at 18:22):

I thought that every `expr`

is also a `pexpr`

? (I.e., I expected a coercion.) But I guess I'm naive (-;

#### Johan Commelin (Apr 17 2020 at 18:26):

Ooh wait, isn't that what `%%`

is doing?

#### Johan Commelin (Apr 17 2020 at 19:00):

I'm completely stuck. @Mario Carneiro would you mind enlightening me?

I've got

r : name -- some relation lhs : expr -- the "old" left hand side rhs : expr -- the right hand side new_lhs : expr -- the "new" left hand side prf : expr -- a proof that lhs = new_lhs

Now I've run

t ← mk_app r [new_lhs, rhs], -- the new target

But now I want to run `tactic.replace target`

, and I need a proof that the new target is equivalent to the old one.

This should be more or less `congr_arg (λ L, r L rhs) prf`

, except that this is not how meta code works. What is the correct variant now? I can't use `mk_app`

here, I think...

#### Johan Commelin (Apr 17 2020 at 19:12):

The version for `rhs`

is easier. This is what I have now

private meta def replace_target_side (new_target : expr) (lam : pexpr) (prf : expr) : tactic unit := do prf' ← to_expr ``(congr_arg %%lam %%prf) tt ff, tactic.replace_target new_target prf' meta def replace_target_lhs (rw : tracked_rewrite) : tactic unit := do (r, lhs, rhs) ← target_lhs_rhs, (new_lhs, prf) ← rw.eval, t ← mk_app r [new_lhs, rhs], replace_target_side t _ prf -- FIXME -- ``(λ L, %%r L %%rhs) meta def replace_target_rhs (rw : tracked_rewrite) : tactic unit := do (r, lhs, rhs) ← target_lhs_rhs, (new_rhs, prf) ← rw.eval, t ← mk_app r [lhs, new_rhs], e ← mk_app r [lhs], replace_target_side t ``(λ R, %%e R) prf

#### Mario Carneiro (Apr 17 2020 at 22:18):

open tactic meta def tracked_rewrite : Type := sorry meta def tracked_rewrite.eval : tracked_rewrite → tactic (expr × expr) := sorry private meta def replace_target_side (new_target : expr) (lam : pexpr) (prf : expr) : tactic unit := do prf' ← to_expr ``(congr_arg %%lam %%prf) tt ff, tactic.replace_target new_target prf' meta def replace_target_lhs (rw : tracked_rewrite) : tactic unit := do expr.app (expr.app r lhs) rhs ← target, (new_lhs, prf) ← rw.eval, replace_target_side (r new_lhs rhs) ``(λ L, %%r L %%rhs) prf meta def replace_target_rhs (rw : tracked_rewrite) : tactic unit := do expr.app (expr.app r lhs) rhs ← target, (new_rhs, prf) ← rw.eval, replace_target_side (r lhs new_rhs) ``(λ R, %%(r lhs) R) prf

#### Johan Commelin (Apr 18 2020 at 05:02):

Aah, nice! So why does `(r, lhs, rhs) ← target_lhs_rhs`

not do the same thing as `expr.app (expr.app r lhs) rhs ← target`

? Is there a reason for this?

#### Johan Commelin (Apr 18 2020 at 05:23):

So now I have compiling code again! :octopus: There is only one minor little problem.... it doesn't do what I want :laughter_tears:

#### Johan Commelin (Apr 18 2020 at 05:25):

I just pushed stuff to the `nth-rewrite`

branch

#### Johan Commelin (Apr 18 2020 at 05:30):

@Mario Carneiro Does

expr.app (expr.app r lhs) rhs ← target

take care of implicit variables etc...?

Suppose I have `a = b`

where `a b : nat`

. Then I would like `r`

to be `@eq nat`

and `lhs`

and `rhs`

to be `a`

and `b`

respectively.

#### Johan Commelin (Apr 18 2020 at 05:33):

My understand is that what you wrote should work the way I want... So maybe the bug is somewhere else

#### Johan Commelin (Apr 18 2020 at 05:36):

Hmmm, it woks with `Prop`

so maybe it's universe issues:

example (x y : Prop) (h₁ : x ↔ y) (h₂ : x ↔ x ∧ x) : x ∧ x ↔ x := begin nth_rewrite_rhs 1 [h₁] at h₂, nth_rewrite_rhs 0 [← h₁] at h₂, nth_rewrite_rhs 0 h₂, end

#### Johan Commelin (Apr 18 2020 at 05:37):

example (x y : ℕ) (h₁ : x = y) (h₂ : x = x + x) : x + x = x := begin nth_rewrite_rhs 1 [h₁] at h₂, -- fails nth_rewrite_rhs 0 [← h₁] at h₂, nth_rewrite_rhs 0 h₂, end

Last updated: May 09 2021 at 18:17 UTC