simplify field in tactic

Stream: general

[Keeley Hoek]

Trivial question: I've got an instance s of some structure which has a nat-valued field f. In tactic mode I have as a hypothesis v : nat := s.f. What can I do to replace v with with its actual nat value? Sorry for the noise

[Mario Carneiro]

what do you mean? If you are in tactic mode, you aren't proving anything so it doesn't matter

[Mario Carneiro]

or do you mean that v : nat := s.f is in the local context of the proof state?

[Mario Carneiro]

You can use dsimp only [v] {zeta := tt} to zeta expand v

[Keeley Hoek]

Hi Mario, I think that's what I mean. If I understand you right, are you saying something like this:

structure my_struct :=
(f : ℕ)

example : false := begin
  let s : my_struct := ⟨42⟩,
  let v := s.f,
  dsimp only [v] {zeta := tt},
  admit
end

should work? Weirdly, the dsimp line fails with

dsimplify tactic failed to simplify
state:
s : my_struct := {f := 42},
v : ℕ := s.f
⊢ false

:'(

[Simon Hudon]

Does v occur in the goal?

[Keeley Hoek]

No, well secretly I'm trying to write a function which I can pass an expr and get back a "simplified" expr; in this case hopefully s.f will become 42.

[Keeley Hoek]

Is there anything which does something like this? Maybe even just like 1 + 1 -> 2

[Kenny Lau]

from my experience, not many tactics know about definitions (i.e. :=)

[Kenny Lau]

which is quite annoying

[Simon Hudon]

You can have a look at tactic.dsimp_target in init/meta/simp_tactic.lean to do that. But if your variable v does not occur in the expression, it will fail. You may have to enclose it in try

[Kenny Lau]

oh and you'll never change the definition of v using any tactic.

[Kenny Lau]

just literally no tactic can rewrite definition (things to the right of :=) in hypothesis, in my experience

[Kenny Lau]

my workaround:

structure my_struct :=
(f : ℕ)

example : false := begin
  let s : my_struct := ⟨42⟩,
  let v := s.f,
  have hv : v = 42 := rfl,
  admit
end

[Simon Hudon]

No, you can do some manipulation

[Simon Hudon]

in tactic.basic, in mathlib, you can use local_def_value to get the value of a definition. Then you can rewrite that experience, create a new definition and clear the old one

[Keeley Hoek]

Thanks, yeah I was poking around in simp_target and simplify before and was wondering why it was failing. I note that

structure my_struct :=
(f : ℕ)

def s : my_struct := ⟨42⟩

#reduce s.f

(obviously) prints 42. Is there any way to capture the result like this? I see that in the kernel reduce calls normalize(...) which returns an expr, is there away to get it to do that and capture the result myself?

[Simon Hudon]

Are you trying to evaluate the expression? If it's an arithmetic expression, you can use norm_num. Otherwise, whnf should take you part of the way there

[Simon Hudon]

Also, do you mean normalize from ring.lean?

[Keeley Hoek]

Thanks I'll dig in and read about whnf for a bit. I don't think so, there's this file src/library/normalize.cpp which normalizes exprs you give it.

[Keeley Hoek]

Actually, I think:

meta def dme : tactic unit := do
  let no_dflt := ff,
  let attr_names : list name := [],
  let hs : list simp_arg_type := [],
  (s, to_unfold) ← mk_simp_set no_dflt attr_names hs,
  e ← s.dsimplify to_unfold `({ my_struct . f := 42 }.f),
  trace e

#eval dme

might do what I want!