Access previous structure fields

Stream: general

[Yaël Dillies]

I feel like I keep stumbling onto this limitation. Is there really no way for an auto-param tactic to fill in Prop structure fields using previous Prop fields?

meta def the_tactic_i_want : command :=
`[exact foo.bar_zero _]

structure foo :=
(bar : ℕ → ℕ)
(bar_zero : bar 0 = 37)
(baz : ℕ → ℕ := bar)
(baz_zero : baz 0 = 37 . the_tactic_i_want)

example : foo :=
{ bar := λ _, 37,
  bar_zero := rfl,
  baz_zero := rfl }

example : foo :=
{ bar := λ _, 37,
  bar_zero := rfl }
/-
invalid type ascription, term has type
  ?m_1.bar 0 = 37
but is expected to have type
  37 = 37
state:
⊢ 37 = 37
-/

Context is #17826

[Yaël Dillies]

The obvious alternative would have been

structure foo :=
(bar : ℕ → ℕ)
(bar_zero : bar 0 = 37)
(baz : ℕ → ℕ := bar)
(baz_zero : baz 0 = 37 := bar_zero)
/-
invalid let-expression, term
  bar_zero
has type
  bar 0 = 37
but is expected to have type
  baz 0 = 37
-/

but it doesn't work because bar_zero gets evaluated directly.

[Eric Wieser]

This works:

def maybe_default {α β : Sort*} (a : α) (b : β) : α := a

meta def try_maybe_default : command :=
do
  `(maybe_default %%a %%b) ← tactic.target,
  tactic.exact b

structure foo :=
(bar : ℕ → ℕ)
(bar_zero : bar 0 = 37)
(baz : ℕ → ℕ := bar)
(baz_zero :  maybe_default (baz 0 = 37) bar_zero . try_maybe_default)

example : foo :=
{ bar := λ _, 37,
  bar_zero := rfl,
  baz_zero := rfl }

example : foo :=
{ bar := λ _, 37,
  bar_zero := rfl }

[Jireh Loreaux]

Isn't this the kind of thing you can do with the sneaky by syntax? That is, baz_zero := by exact bar_zero (untested)?

[Mario Carneiro]

I think there are limitations on use of identifiers in auto params in both lean 3 and lean 4

[Yaël Dillies]

Would people be happy with me using Eric's hack, then?

[Mario Carneiro]

maybe_default seems to be another name for opt_param

[Eric Wieser]

opt_param requires the types to agree

[Eric Wieser]

But maybe that should inform a better name

[Mario Carneiro]

hopt_param :)

[Yaël Dillies]

I unironically like it.

[Eric Wieser]

Probably it's reasonable to constrain the universe arguments a bit more than I did

[Scott Morrison]

Might be worth planning and documenting how you will migrate to lean 4 before using any such tricks.

[Yaël Dillies]

This is to be used in algebra.group.defs, so it would be forward-ported immediately anyway ;)