Zulip Chat Archive

Stream: general

Topic: noob tactic question(s)


view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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 pexprs to replace_target_side?

view this post on Zulip Rob Lewis (Apr 17 2020 at 18:12):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 17 2020 at 18:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (Apr 17 2020 at 18:26):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Apr 18 2020 at 05:25):

I just pushed stuff to the nth-rewrite branch

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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