Stream: Ltac2

Topic: Debugging, Std.set, patterns

Patrick Nicodemus (Oct 19 2022 at 20:52):

Hello, I am quite new to Ltac2 so I would appreciate any help in figuring out what I am doing wrong here.

Patrick Nicodemus (Oct 19 2022 at 20:52):

Ltac2 Type pattern_type := [ SetPattern (Init.constr) | SetInPattern (Init.pattern) ].
Ltac2 rec hideme pattern_list tac :=
  match pattern_list with
  | [] => tac
  | head :: tail =>
      match head with
      | SetPattern p =>
          let h := Fresh.in_goal @tempvar in
          Std.set
             Init.false
             (fun () => (Init.Some h, p))
             { Std.on_hyps := Init.None ;
                              Std.on_concl := Std.AllOccurrences }
      | SetInPattern p => tac
      end
  end.

Goal forall (a b c d : nat), a + b + c + d = 5.
Proof.
  intros a b c d.
  (* Std.set Init.false (fun () => (Init.Some @H, open_constr:(_ + _))) *)
  (*                { Std.on_hyps := Init.None ; Std.on_concl := Std.AllOccurrences }. *)
  hideme (SetPattern open_constr:(_ + _) :: []) ().

Patrick Nicodemus (Oct 19 2022 at 20:55):

In the script above, the script "hideme" is supposed to take in a list of (open) constr's and patterns, and it should iterate through the list and run either "set h := p", where p is the open_constr, or do something else if it's a pattern

Patrick Nicodemus (Oct 19 2022 at 20:56):

My problem is that in the body of this loop, Std.set does not successfully patternmatch. I expect the very last line to add tempvar := a + b + c + d : nat to the context. However, it instead adds tempvar := ?n + ?m : nat. This is confusing to me. I also was under the impression that the flag Init.false as the first argument to Std.set should cause the command to fail if it cannot find a match without evars, so even if it could not match I do not understand why it succeeds.

Patrick Nicodemus (Oct 19 2022 at 20:57):

The code that is commented out has the expected behavior, it adds H := a + b + c + d : nat to the context.

Gaëtan Gilbert (Oct 19 2022 at 21:42):

you need to thunk the constr argument
using false makes it fail if there are new evars, and they are new iff they are produced by the thunk argument

Patrick Nicodemus (Oct 19 2022 at 22:27):

Thank you! Can you tell me where this kind of thing is documented?

Patrick Nicodemus (Oct 20 2022 at 00:08):

Also, another documentation question, what is the difference between Some [] and None in the on_hyps field of Std.clause? Where can I read about this?

Last updated: Jan 31 2023 at 11:01 UTC