The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

I am making some use of 8.5 features, so if the 8.5 version has a cleaner 
result, I would use the 8.5 version. But I am also curious to see how you 
solved it in 8.4.

Regarding context searches: I am interested in proof automation performance 
and context searches with unspecific search patterns and heavy follow up 
tactics have a bad impact on performance. But context searches with 
restrictive patterns or lightweight follow up tactics or properly gated 
heavier tactics are fine. On the other hand everything which leads to good 
search tree pruning or more stable proof search is usually worth the effort. 
What counts is ease of use, stability and the final performance. I am quite 
pragmatic in reaching these goals.

For the time being I think I will go with Ltac as far as possible. Meanwhile 
I am quite happy with it. I try to delay plugin development until sometime 
later when my project grows larger.

Here is the final "IsLiteralTerm" tactic which is based on your is_ctor 
tactic (called IsCtorSym below).

(* Check if the given term is an inductive type *)

Ltac IsInductiveType type :=
  let H:=fresh in
  (* Using type as a precondition allows us to get a value of the type during 
the proof of the assert *)
  assert (type -> True) as H by (
    (* val is a opaque value of type 'type' *)
    intros val; 
    (* See if val can be destructed, if so solve the goal *)
    destruct val; exact I
  );
  (* clear the hypothesis generated by the assert *)
  clear H.

(* Check if a complete term contains only constructors and inductive type 
names like a polymorphic list type argument.
   This includes numbers, lists of numbers, strings, booleans, ... *)

Ltac IsLiteralTerm term := lazymatch term with
| ?H ?A1 => 
    (* Debug idtac "f2" H A1; *) 
    IsLiteralTerm H; 
    IsLiteralTerm A1
| ?H => 
    (* Debug idtac "f1" H; *)
    first [ IsCtorSym H | IsInductiveType H ]
end.

Best regards,

Michael