Add is_ind, is_constructor, is_proj

[JasonGross]

No description provided.

[jonleivent]

Are those the only kind_of_term left that Ltac can't distinguish via syntax or existing predicates?

I wonder if it would be better to have a Coq inductive that mirrors kind_of_term (maybe just with argless constructors?), and just have a "kind of" tactic (in the spirit of "type of") that returns one of those constructors. One could then write "match kind of x with" in Ltac. Of course, one does "match x with" now and picks out distinguishing syntactic structure - but some kinds don't have any.

[JasonGross]

We have

  | Rel       of int
  | Var       of Id.t
  | Meta      of metavariable
  | Evar      of 'constr pexistential
  | Sort      of sorts
  | Cast      of 'constr * cast_kind * 'types
  | Prod      of Name.t * 'types * 'types
  | Lambda    of Name.t * 'types * 'constr
  | LetIn     of Name.t * 'constr * 'types * 'constr
  | App       of 'constr * 'constr array
  | Const     of constant puniverses
  | Ind       of inductive puniverses
  | Construct of constructor puniverses
  | Case      of case_info * 'constr * 'constr * 'constr array
  | Fix       of ('constr, 'types) pfixpoint
  | CoFix     of ('constr, 'types) pcofixpoint
  | Proj      of projection * 'constr

We have is_fix, is_cofix, is_evar, is_var. I believe Rel and Meta are not supposed to be visible at any point (someone correct me if I'm wrong). Cast is very fragile (most reduction tactics remove them), it handles things like (x : T) : U, x <: T, x <+ T for casts, vm_casts, native_casts. Sort is:

Ltac is_sort x :=
  lazymatch x with
  | Type => idtac
  | Set => idtac
  | Prop => idtac
  | _ => fail 0 "not a sort"
  end.

You can get Prod by matching against forall x, _; Lambda by matching against (fun x => _); LetIn by matching against let x := _ in _; App by matching against ?f ?x, Case by matching against match _ with _ => _ end. This PR gives Ind, Construct, Proj.

You might be able to get Const as:

Tactic Notation "is_const" ref(x) := idtac.

in 8.6, but I'm not sure.

This leaves the following

• Rel, Meta - probably inaccessible
• Cast - probably irrelevant to most tactic code
• Const - probably fine as a default case, possibly doable in Ltac

[jonleivent]

Yes - it seems like:
Tactic Notation "is_const" reference(x) := idtac.
works in 8.5. It's a bit ugly, but may be a useful idiom for other predicates as well (is_integer, is_uconst, etc.).

[JasonGross]

It will not work for is_uconst; there are implicit casts that are automatically inserted there.

[maximedenes]

So would it make sense to provide is_constant, to avoid fragile implementations of it?

[JasonGross]

Probably. I've added a commit to provide is_const, and another to update CHANGES. (Someone should document is_evar, has_evars, is_proj, etc..., but that can be done after the merge window closes)