Stream: Coq users

Topic: use Gallina string with ltac's fresh


view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 07:42):

Hi, I have a constructor C taking a string argument "foo" in my goal, and essentially I want to perform set (foo := "foo"). Naturally I would try something like match goal with | |- context [ C ?foo_string ] => let x := fresh foo_string in set (x := C foo_string) end, but here foo_string is a gallina string, while fresh expects an identifier or an Ltac string (at least that's what the error message makes me think). Is there a conversion function?

view this post on Zulip Michael Soegtrop (May 11 2022 at 10:20):

Ltac2 has a function to convert Ltac2 strings to identifiers here Ltac2-ident and it shouldn't be hard to create an Ltac2 string from a gallina string. I am not aware of an Ltac1 way to do this, but you can mix Ltac2 into Ltac1.

view this post on Zulip Michael Soegtrop (May 11 2022 at 10:24):

For any serious automation I would anyway recommend Ltac2 - it is a bit terse in features especially in documentation, but Ltac2 tactics are much easier to maintain and grow because it is an ML like strictly typed language.

view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 11:50):

cheers Michael, that's what I ended up doing. It just seems like someone must already have written the boilerplate to convert gallina types to their ltac2 equivalent

view this post on Zulip Michael Soegtrop (May 11 2022 at 12:11):

Philipp G. Haselwarter said:

cheers Michael, that's what I ended up doing. It just seems like someone must already have written the boilerplate to convert gallina types to their ltac2 equivalent

I have it for quite a few, but not for strings.

view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 12:32):

@Michael Soegtrop could you give me a pointer to one such, for reference?

view this post on Zulip Michael Soegtrop (May 11 2022 at 12:58):

Nothing you can find online. Here is an example:

Ltac2 rec ltac_int_of_pos (p : constr) : int :=
  let res :=lazy_match! p with
  | xH => 1
  | xO ?p' => Int.mul 2 (ltac_int_of_pos p')
  | xI ?p' => Int.add (Int.mul 2 (ltac_int_of_pos p')) 1
  end in
  if Int.lt res 0
  then throw_invalid_argument_sc "ltac_int_of_pos: value is too large: " p
  else res.

Ltac2 ltac_int_of_Z (z : constr) : int :=
  lazy_match! z with
  | Z0 => 0
  | Zpos ?p => ltac_int_of_pos p
  | Zneg ?p => Int.sub 0 (ltac_int_of_pos p)
  end.

The throw_invalid_argument_scis pre Ltac2-printf and requires a bit of boilerplate - I still need to write throw convenience functions with printf style parameters.

view this post on Zulip Notification Bot (May 11 2022 at 17:58):

This topic was moved to #Ltac2 > use Gallina string with ltac's fresh by Michael Soegtrop.


Last updated: Jan 29 2023 at 01:02 UTC