Stream: Coq users

Topic: Ltac definition

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?

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.

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.

Ali Caglayan (Aug 10 2020 at 12:30):

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

Théo Winterhalter (Aug 10 2020 at 12:31):

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

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.

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: Sep 30 2023 at 16:01 UTC