Stream: Ltac2

Topic: matches_subterm

Patrick Nicodemus (Oct 20 2022 at 06:16):

I have a question about the matches_subterm function.
Does matches_subterm do any kind of unfolding or instantation? I have a weird bug in my code where a metavariable is being matched with a subterm I know isn't in the term.
Maybe somehow the variable is being instantiated through Coq's guesswork or maybe there's some primitive projections stuff going on

Patrick Nicodemus (Oct 20 2022 at 06:20):

I ran the command
set(tempvar1 := obj[D] : Type).

Patrick Nicodemus (Oct 20 2022 at 06:20):

And now I have this in my context.
tempvar1 := obj[D] : Type
When I run Set Printing All I see all the references to obj[D] in my goal are gone and replaced by tempvar1.

Patrick Nicodemus (Oct 20 2022 at 06:22):

and I wrote this Ltac script that searches in the goal for a projection fst ?a onto a first coordinate, and introduces a new variable into the context which is equal to a. However it is supposed to skip all matches where a is unified with a variable. My intention is that the script should fail, but instead it succeeds and introduces a new variable into the context which is also equal to obj[D]. The goal is unchanged.

Patrick Nicodemus (Oct 20 2022 at 06:24):

Here is the script I ran:

ltac2:(  let subterm_stream := fun () => Pattern.matches_subterm pat:(@fst ?a) (Control.goal ()) in
  let rec traverse_thunk' thunk :=
  match Control.case thunk with
  | Init.Val pair =>
      let (a , c_p ) := pair in
      let ( ctx , id_constr_list) := a in
      match id_constr_list with
      | [] => Control.zero Init.No_value (* The list shouldn't be empty, if you put in a
                                       pattern with 1 quantifier you should get a
                                       list with one element. *)
      | x :: xs => let (ident, term) := x in
                   Message.print (Message.of_constr term);
                   if Constr.is_var term then
                     traverse_thunk' (fun () => c_p Init.Not_found)
                   else
                     let h := Fresh.in_goal @tempvar in
                     (Std.set Init.false (fun () => (Init.Some h, term))
                    { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences })
      end
  | Init.Err e => fail
  end in traverse_thunk' subterm_stream).

Patrick Nicodemus (Oct 20 2022 at 06:26):

When I run this it prints out all the attempted matches:

tempvar1
tempvar1
tempvar1
tempvar1
tempvar1
tempvar1
tempvar1
tempvar1
obj[D]

As intended it skips over all the initial matches originally, but then somehow it succeeds by matching the netavariable a with obj[D]. This term isn't in the goal.

Jason Gross (Oct 20 2022 at 08:22):

It could be that set and matches_subterm treat hidden subterms differently. In particular, if @fst obj[D] occurs in

• the parameters of a primitive projection
• the type of the binders of the return clause of a match
• the type of the bound arguments to a constructor in the branches of a match
• an evar substitution
• the type of the binders to an unfolded fix or cofix

it may be that the behavior is different. Some of these will not even be printed with Set Printing All.

Gaëtan Gilbert (Oct 20 2022 at 09:27):

instantiate the context and print it to see where it found something

Patrick Nicodemus (Oct 21 2022 at 02:06):

Yes, it was indeed a primitive projections thing! Thank you. I instantiated the pattern with open_constr:(_) so I could search the missing variable and the term it found was a subterm of a parameter to a record type with primitive projections

Patrick Nicodemus (Oct 21 2022 at 02:08):

Record Setoid@{u u0} (A : Type) : Type := Build_Setoid
  { equiv : crelation A;  setoid_equiv : @Equivalence A equiv }.

Setoid has primitive projections with eta conversion.

Goal before running the tactic :

   forall     _ : @equiv _ s y2 (@compose (Product D C) tempvar1 ...

Pattern found by matches_subterm after instantiating the context with open_constr:(_) :

(forall
  _ : @equiv (prod (@hom D (?y y) (@fst (@obj D) (@obj C) y0)) (@hom C y3 y4)) s  y2   (@compose (Product D C) tempvar1 ...

Patrick Nicodemus (Oct 21 2022 at 03:13):

I was going to use "progress" here to fix this, where I thought "progress" would fail if it did not change the goal. But I tried this and it did not work. Am I misunderstanding things and "progress" succeeds if there is a change to the goal-hypothesis context pair [Gamma |- A] rather than just the individual goal, A?

Patrick Nicodemus (Oct 21 2022 at 03:14):

Because obviously if I run set (H := A) this will change the list of hypotheses and thus make "progress" in the list of hypotheses even if there is no change in the goal proper.

Patrick Nicodemus (Oct 21 2022 at 03:22):

Should I just use this instead?

Ltac2 progress_in_goal tac :=
  let old_goal := Control.goal() in
  ( tac() ;
    if Constr.equal old_goal (Control.goal()) then Control.zero Not_found else () ).

Gaëtan Gilbert (Oct 21 2022 at 08:47):

Not_found is wrong, otherwise sounds reasonable

Last updated: Oct 12 2024 at 12:01 UTC