search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
191 stars 26 forks source link

Command for adding arbitrary terms as Aesop rules #107

Closed JLimperg closed 7 months ago

JLimperg commented 7 months ago

When adding a small variation of a theorem (e.g. the forward or backward direction of an Iff lemma) as an Aesop rule, the variation currently has to be written as a separate theorem that is then tagged @[aesop]. It would be nicer if there was an Aesop command that allows us to register the variation directly. Mock syntax:

add_aesop_rules apply 1% [λ args, (your_lemma args).mp, ...]

It would be even nicer if we could leave out the λ args and write (your_lemma _ _).mp.

See Zulip conversation.

JLimperg commented 7 months ago

Fixed by 7c31916e8ba8c356f42d0802a2fe8530ff2a8cdd

For now, the λ args can't be omitted. Supporting this would be somewhat complicated, so it's not going to happen soon.