Coq: apply the f_equal tactic only when f is an inductive constructor

The f_equal tactic is unconditionally useful for equality proofs involving inductive constructors. a :: s = a' :: s would be such a goal, reducing to a = a'.

Using it with arbitrary functions is a different story. 4 mod 2 = 2 mod 2 would reduce to 4 = 2, which is clearly absurd.

I'm wondering if there's a way to automatically apply f_equal (or similar) only in cases where it doesn't lose information, e.g. inductive constructors.

Solution

Here is an alternative, non-hackish way, using Ltac2 (with help from Ltac2's author Pierre-Marie Pédrot):

From Ltac2 Require Import Ltac2.

Ltac2 is_constructor c := match Constr.Unsafe.kind c with
| Constr.Unsafe.Constructor _ _ => true
| _ => false
end.

Ltac2 not_a_constructor f :=
  let msg :=
    Message.concat (Message.of_constr f) (Message.of_string " is not a constructor")
  in
  Control.zero (Tactic_failure (Some msg)).

Ltac2 dest_app c := match Constr.Unsafe.kind c with
| Constr.Unsafe.App f args => (f, args)
| _ => (c, Ltac2.Array.make 0 constr:(Type))
end.

Ltac2 f_equal_ind () :=
  lazy_match! goal with
  | [ |- ?lhs = _ ] =>
    let (f, _) := dest_app lhs in
    match is_constructor f with
    | true => f_equal
    | false => Control.zero (not_a_constructor f)
    end
  | [ |- _ ] =>
    Control.zero (Tactic_failure (Some (Message.of_string "Goal is not an equality")))
  end.

Ltac2 Notation "f_equal_ind" := f_equal_ind ().

(* Tests *)

Require Import List.
Import ListNotations.
Require Import Arith.

Goal forall (a a' : nat) s, a :: s = a' :: s.
intros.
f_equal_ind. (* a = a' *)
Abort.

Goal True.
Fail f_equal_ind.
(* 
The command has indeed failed with message:
Uncaught Ltac2 exception: Tactic_failure (Some (message:(Goal is not an equality)))
*)
Abort.

Goal 1 mod 2 = 3 mod 4.
Fail f_equal_ind.
(*
The command has indeed failed with message:
Uncaught Ltac2 exception: Tactic_failure (Some (message:(Nat.modulo is not a constructor)))
*)
Abort.

You can find Ltac2 documentation at https://coq.github.io/doc/master/refman/proof-engine/ltac2.html. It will be released with Coq 8.11, but sources compatible with the previous versions of Coq can be found in the various branches of https://github.com/coq/ltac2/branches/all.