Stream: Coq users

Topic: Ltac definition


view this post on Zulip Gergely Buday (Aug 10 2020 at 12:14):

Dear Experts,

what does this ltac definition do?

Ltac rewr_assumption := idtac; match goal with
| [R: _ = _ |- _ ] => first [rewrite R| rewrite <- R]
end.

Can you explain it in plain English?

view this post on Zulip Ali Caglayan (Aug 10 2020 at 12:28):

It checks the context for an equality R and tries to rewrite using it. If rewriting along the equality doesn't work it then tries rewriting back then gives up.

view this post on Zulip Enrico Tassi (Aug 10 2020 at 12:29):

in rewrite R there is an implicit rewrite -> R (from left to right). So it tries to use R both ways.

view this post on Zulip Ali Caglayan (Aug 10 2020 at 12:30):

I'm however not sure why idtac is there. Presumably it does nothing here.

view this post on Zulip Théo Winterhalter (Aug 10 2020 at 12:31):

Also, before giving up, it will look for another equality to rewrite with.

view this post on Zulip Enrico Tassi (Aug 10 2020 at 12:34):

This is probably the "thunk idiom", I'm not an exprert but tac and idtac; tac do, in some context, behave like ML code tac () and fun () -> tac () (in ML these two expressions don't have the same type, but in Ltac1 they do, fixed in Ltac2). I suspect the idtac is there to be sure the match-goal-with is evaluated when you expect it.

view this post on Zulip Paolo Giarrusso (Aug 11 2020 at 08:21):

Re "gives up", that tactic will give up by failing, if there's no equality in context where rewriting succeeds, no?


Last updated: Jan 27 2023 at 01:03 UTC