Zulip Chat Archive

Stream: general

Topic: automatically infer proof argument using tactic

Huỳnh Trần Khanh (Oct 30 2021 at 14:35):

is there a way to make lean infer a proof argument automatically using a tactic? i think i've read about it somewhere but... i can't find that page anymore :cry:

Huỳnh Trần Khanh (Oct 30 2021 at 14:44):

this is what im trying to achieve:

structure some_value_t :=
(value : \N)
(proof : value < 100)

and i want lean to automatically infer the proof field with the norm_num tactic because i mostly instatiate the structure with a literal value, not a variable

Huỳnh Trần Khanh (Oct 30 2021 at 14:44):

thanks in advance as usual

Eric Wieser (Oct 30 2021 at 15:00):

structure some_value_t :=
(value : \N)
(proof : value < 100 . norm_num)

I think

Huỳnh Trần Khanh (Oct 30 2021 at 15:01):

thanks for the answer. but i got invalid auto_param, 'norm_num' must have type (tactic unit)

Chris Hughes (Oct 30 2021 at 15:02):

I think it's a bit more complicated than that. The argument after the . has to be a name corresponding to a definition of type tactic unit. The following works

meta def norm_num2 : tactic unit := `[norm_num]

structure some_value_t :=
(value : nat)
(proof : value < 100 . norm_num2)

Last updated: Dec 20 2023 at 11:08 UTC