Ltac2: Function to match a variable with a type

Developing plugins
1

Dear Coq community,

I have been trying to write a function in Ltac2 that takes two arguments:

  1. a constr ‘x’ that can be of any type
  2. a constr ‘t’ that is a Type

I want this function to give different output if ‘x’ belongs to the Type of ‘t’ than in the case in which it does not.

The following is a minimal example of the best I managed to produce so far.
However, it does not work as intended. &t does not seem to substitute the value stored in t here.

From Ltac2 Require Import Ltac2.
From Ltac2 Require Option.
From Ltac2 Require Import Message.
Require Import Bool.

Ltac2 match_type (x:constr) (t:constr) :=
    match! x with
    | &t => concat (concat (of_constr x) (of_string " is of type ")) (of_constr t)
    | _ => concat (concat (of_constr x) (of_string " is not of type ")) (of_constr t)
    end.

Goal True.
    print (match_type (constr:(2)) (constr:(nat))).
    print (match_type (constr:(1)) (constr:(bool))).

It produces the following output:

2 is of type nat
1 is of type bool

which is clearly not desirable!

I know there is a function of type in Ltac1 that would probably make this possible.
However, my question is, is there also a Ltac2-native way to build the function I specified?

1 Like
2

The trick is to use a gallina function to extract the type and then use Constr.equal. It might be required to also evaluate t.

From Ltac2 Require Import Ltac2.
Require Import Bool.

Definition type_of {T : Type} (x : T) := T.

Ltac2 match_type (x:constr) (t:constr) :=
  let tx:=eval cbv in (type_of $x) in
  Constr.equal tx t.

Ltac2 Eval match_type constr:(2) constr:(nat).
Ltac2 Eval match_type constr:(2) constr:(bool).
Ltac2 Eval match_type constr:(true) constr:(bool).
1 Like
3

Thank you very much, it does what I was looking for :slight_smile:

4

You are welcome! Please note that Constr.equal compares literal equality of constr terms without any computation or unification. So if the type you give as t is not a fully evaluated ground term (like nat or list bool) but e.g. a function which computes a type, you need to eval cbv $t as well. Production code should better include both evals, unless it can be excluded that t is something computed. With complicated types you might run into the issue that you cannot eval cbv the type. In that case you would have to check for unifiability of the two types, which is a bit more involved.

2 Likes