noob tactic question(s)

Stream: general

[Johan Commelin]

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]

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]

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 pexprs to replace_target_side?

[Rob Lewis]

If the answers are "no," you probably want to use the tacticmk_app r [new_lhs, rhs].

[Rob Lewis]

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]

Well I guess I want to support the case where r is either = or \iff.

[Johan Commelin]

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]

But it doesn't like the e in the last line, because it expects a pexpr instead of an expr

[Johan Commelin]

I thought that every expr is also a pexpr? (I.e., I expected a coercion.) But I guess I'm naive (-;

[Johan Commelin]

Ooh wait, isn't that what %% is doing?

[Johan Commelin]

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]

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]

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]

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]

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]

I just pushed stuff to the nth-rewrite branch

[Johan Commelin]

@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]

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

[Johan Commelin]

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]

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