Stream: Coq users

Topic: let-expressions in Ltac

view this post on Zulip João Mendes (Apr 29 2024 at 00:09):

I am having trouble in understanding how let-expressions work in Ltac. Here are my questions:

  1. In the example below, foo1 doesn't work without the let-expression, while foo2 does:
Ltac foo1 :=
  let H := fresh "H" in
  intro H; clear H.

Ltac foo2 :=
  assert (H : True); auto;
  intro H; clear H.

My general question is: when it is necessary to use a let-expression inside an ltac?

  1. In foo1 of the example above, I've attributed "H" to the parameter H. Attributing "H1" wouldn't have changed pretty much anything in this context. I know that in a case like:
Ltac foo3 :=
  let H := fresh "H1" in
  intro H.

A hypothesis "H1" would be added to the proof instead of a hypothesis "H", that is, affecting merely the labels in the proof.

So, why doesn't Coq allow to use the let-expression as let H in, without the need to attribute any expression to it? When can be useful to a let-expression attributin an expression that is a different to the name of the paramater (eg, let H := fresh "H1" in)?

Last updated: Oct 13 2024 at 01:02 UTC