The Coq mailing list

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

Dear Jonathan,

I have a very special case in that my terms don't contain partially applied 
functions nor opaque definitions. Basically the idea was that only free 
variables, evars, opaque definitions, partially applied functions and 
constructors stop compute from further reducing a term. So in my application 
I just have to check the result of compute for vars and evars. 

But your solution is much cleaner and it likely gives me less pain with 
future extensions (e.g. compute producing really large terms), so I think 
about using it. It is a bit slower in my current application, but it is 
negligible in the overall execution time (<5%).

I would be very interested in your constructor listing tactic. I have a 8.5 
based tactic which creates a list of all constructors for simple enum types, 
but I didn't manage to make this generic.

A measure of term complexity is indeed quite tricky in general, as you say 
especially around the matches, but I can imagine that anonymous fixpoints are 
also tricky. The question is how important this is. In the end this is just 
for heuristics used to direct proof search in the right direction and it 
might be good enough to just give matches and fixpoints a fixed score. If 
not, it is likely a good time for me to try myself on my first Ocaml tactic.

Since for intermediate advanced Coq users like me your is_ctor tactic is not 
easy to understand, I documented it a bit and gave the variables more 
expressive names. I hope I understood it correctly. I would very much 
appreciate if you could have a quick look at my comments.

Thanks & best regards,

Michael

Ltac head_of term :=
lazymatch term with
| (?H _) => head_of H
| _ => term
end.

Ltac get_value H := eval cbv delta [H] in H.

(* Check if a symbol is a constructor of an inductive type.
   A constructor is a function with 2 properties
   1.) The result type is an inductive type
   2.) The function is equal to the head symbol of one of the constructor 
terms produced when destructing the result type
   The below tactic, from a Coq forum post of Jonathan Leivent, checks these 
two properties.
*)

Ltac is_ctor sym :=
  try (
    try (
      (* Get the result type of sym by providing all arguments.
         For this we use (forall T:Type, T), which returns a value for any 
type (including False).
         Although such a function obviously cannot be constructed, using it 
as a precondition as in
         assert( (forall T:Type, T) -> True ) gives temporary access to it 
inside the proof of the assert.
         Although any values derived from this will not survive past the 
proof of the assert,
         we can make a tactic fail descisison based on this, and this 
descision does survive! *)
      assert ((forall T:Type, T) -> True) by (
        (* Introduce (forall T:Type,T) as value_supplier *)
        let value_supplier:=fresh "value_supplier" in 
        intro value_supplier;
        (* Create a copy of sym named sym_result. This also checks if sym is 
valid, e.g. not undefined. *)
        let sym_result:=fresh "sym_result" in 
        first
          [ pose sym as sym_result
          | fail 3 "is_ctor:" sym "is not a valid term"
          ];
        (* Now remove the arguments of sym_result one by one using the 
universal value_supplier *)
        repeat specialize (sym_result (value_supplier _));
        (* Create a copy of sym_result, because destruct clears sym_result.
           The copy sym_result' will be set to one of the constructor terms 
of the result type. *)
        let sym_result':=fresh "sym_result'" in 
        pose sym_result as sym_result';
        (* Destruct sym_result in order to
           1. Check if sym_result is an inducitve type
           2. If so, enumerate all constructors of this type *)
        first
          [ destruct sym_result 
          | fail 3 "is_ctor:" sym "does not produce an inductive type"
          ]; 
        (* Unfold sym_result' and get the constructor term produced by 
destruct.
           This has nothing to do with sym itself, if just unfolds the local 
definition sym_result' *)
        let constr_term:=get_value sym_result' in
        let constr_head:=head_of constr_term in
        idtac sym sym_result' constr_term constr_head;
        (* Compare the head symbol of the constructor term with the input 
symbol *)
        try (constr_eq constr_head sym; fail 2 (*success*)); 
        (* Finish the proof of ((forall T:Type, T) -> True) *)
        exact I
      );
      fail 2 "is_ctor:" sym "is not a constructor"
    );
    fail 1 "is_ctor - problem with tactic"
  ).

(* is_ctor test cases *)

Variable F:nat.
Variable T:Type.
Variable G:T.

Goal True.
Fail is_ctor F.
Fail is_ctor G.
Fail is_ctor X.
is_ctor 0.
Fail is_ctor 1.
is_ctor S.
is_ctor cons.
is_ctor @nil.
is_ctor @eq_refl.
is_ctor true.
is_ctor false.
is_ctor I.
Fail is_ctor (cons 1 nil).
Fail is_ctor True.
Fail is_ctor Type.
Fail is_ctor pred.
exact I.
Qed.