Turn "Make Definition" into a tactic

[yforster]

Hi,

while the quote_term tactic corresponds to "Quote Definition" (or quote_term in OCaml source), it would be great to have a tactic denote_term corresponding to "Make Definition" (or denote_term in the source).

To make it more clear, see the following code:

Make Definition tPlus := (Ast.tVar "plus").
(* binds tPlus to plus *)

Goal True.
Proof.
  let t := constr:(Ast.tVar "plus") in
  let k x := pose x in
  denote_term t k.
  (* I want this to bind x to plus in the context *)
  auto.
Qed.

So, i looked into reify.ml4 and tried to define the following:

TACTIC EXTEND get_goal2
    | [ "denote_term" constr(c) tactic(tac) ] ->
      [ 
  Proofview.Goal.nf_enter begin fun gl ->
      let c = TermReify.denote_term c in
      ltac_apply tac (List.map to_ltac_val [c])
  end ]
END;;

This works only partially. The example above is not working and fails with Error: Cannot reinterpret "plus" in the current environment.. In contrast, the following is working:

Goal forall (X : Type), True.
Proof.
  intros X.
  let t := constr:(Ast.tVar "X") in
  let k x := pose x in
  denote_term t k.
  auto.
Qed.

Denoting constructors and types with the tactic works.

Any idea how to fix this? I tried playing with Lemma.get_current_context as follows, but that still doesn't work (to be honest I was kind of brute forcing and had no real clue what I'm doing):

TACTIC EXTEND get_goal2
    | [ "denote_term" constr(c) tactic(tac) ] ->
      [ 
        Proofview.Goal.nf_enter begin fun gl ->
         let (evm,env) = Lemmas.get_current_context () in
         let def' = Constrextern.extern_constr true env evm c in
         let def = Constrintern.interp_constr env evm def' in
         let c = TermReify.denote_term (fst def) in
      ltac_apply tac (List.map to_ltac_val [c])
  end ]
END;;

I'd appreciate any help. Many thanks in advance

Yannick

[gmalecha]

Hello, Yannick --

The tVar constructor is only used for local variables, not definitions. To reference definitions you need to use tConst The easiest way to see what you want is to do:

Quote Definition qfoo := plus.
Print qfoo.

The reason that converting syntax to terms is not yet supported is due to universes. I don't have an obvious way to convert tSort into a Coq value when the sort is Type due to the representation of universes.

[yforster]

I already tried this, but tConst raises an error in denote_term. Using tVar (and, under the hood, unquote_ident) it works in the vernacular version, but not in the LTac version. So you'd say there's no (easy) way to replay what "Make Definition" can do in a tactic?

In general, what I'm looking for is a way to get a term out of it's name (so plus out of "plus", for instance), and denote_term seemed very promising.

[yforster]

Ok, I was able to solve the problem. The following works now:

Goal True.
Proof.
  let t := constr:(Ast.tVar "plus") in
  let k x := pose x in
  denote_term t k.
  (* this poses (n := Init.Nat.add : nat -> nat -> nat) to the context *)
  auto.
Qed.

The tactic implementation looks as follows:

TACTIC EXTEND get_goal2
    | [ "denote_term" constr(c) tactic(tac) ] ->
      [ 
        Proofview.Goal.nf_enter begin fun gl ->
         let (evm,env) = Lemmas.get_current_context() in
         let c = TermReify.denote_term c in
         let def' = Constrextern.extern_constr true env evm c in
         let def = Constrintern.interp_constr env evm def' in
      ltac_apply tac (List.map to_ltac_val [fst def])
  end ]
END;;

[gmalecha]

Thanks!

closed in c6de18e0ba00980e82f61c98e2348c292f86faa5