Stream: MetaCoq

Topic: Constructor and backtracking


view this post on Zulip Thomas Lamiaux (Mar 31 2024 at 00:41):

Hi, I am currently learning MetaCoq, and I was looking at the constructor_tac example available on the repo https://github.com/MetaCoq/metacoq/blob/coq-8.16/examples/constructor_tac.v .
The tactic constructor_tac does not behave as the usual constructor, as there is no backtracking, typically, it can not solve the following goal that contructor can :

Goal {x : bool | x = false }.
  unshelve eapply exist.
  Fail all: constructor_tac.
  all: constructor.
Qed.

How could one account for backtracking ?

view this post on Zulip Thomas Lamiaux (Mar 31 2024 at 01:00):

Also, I was trying to modify the tactic to get not the first constructor of an inductive type but the second one.
So I modified the code by changing a 0 to a 1 as bellow

let term := Ast.tApp (Ast.tConstruct ind **1** u) args in

Yet, surprisingly, doing so works only for some types. For instance, in the following, it works on sum but not on nat, and I don't really get why

Goal False + True + nat.
  constructor_tac.
  Fail constructor_tac.
Admitted.

view this post on Zulip Gaëtan Gilbert (Mar 31 2024 at 09:58):

in

      let cstrs := Ast.Env.ind_ctors oib in
      match cstrs with
      | [] => tmFail "no constructor in this inductive type"
      | hd :: _ =>

hd is the data for the 1st constructor, so the code using only works to build the 1st constructor (and sometimes to build other constructors if their data is similar enough, in this case the code only cares about the number of arguments)

view this post on Zulip Thomas Lamiaux (Mar 31 2024 at 11:14):

Ha yes right, I forgot to account for that thanks

view this post on Zulip Thomas Lamiaux (Mar 31 2024 at 12:38):

I have modified the tactic to get the second constructor as follows

      match cstrs with
      | [] => tmFail "no constructor in this inductive type"
      | [qh] => tmFail "not enough constructors in this inductive type"
      | qd :: hd :: _ =>
          let args := cstr_args hd in
          let params := firstn qi.(ind_npars) iargs in
          let args := (params ++ map (fun _ => Ast.hole) args)%list in
          let term := Ast.tApp (Ast.tConstruct ind 1 u) args in
          term' <- tmEval all term ;;
          tmPrint term' ;;
          tmUnquote term'

It works perfectly fine for true + false, bool or list nat but for a reason or another, it still does not work nat where it does nothing. (do not bug or fail, just does nothing)
I have tried to print the terms to inspect them, but I can't notice any issue reading them and comparing them.
For nat I get the following, which is basically what I expected :

(tApp
   (tConstruct
      {|
        inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
        inductive_ind := 0
      |} 1 []) [tEvar fresh_evar_id []])

view this post on Zulip Gaëtan Gilbert (Mar 31 2024 at 12:43):

Are you sure it does nothing? The second constructor of nat is S : nat -> nat so applying it produces the same goal, you can only see the effect with Show Proof or if some other goal depends on the one you're working on

view this post on Zulip Thomas Lamiaux (Mar 31 2024 at 12:48):

yeah you are completely right, I just wasn't thinking about that


Last updated: Jul 23 2024 at 20:01 UTC