Coq:仅当 f 是归纳构造函数时才应用 f_equal 策略

Question

f_equal 策略对于涉及归纳构造函数的相等性证明无条件有用。 a::s = a'::s 就是这样一个目标，简化为 a = a'。

将它与任意函数一起使用是另一回事。 4 mod 2 = 2 mod 2 将减少为 4 = 2，这显然是荒谬的。

我想知道是否有一种方法可以自动应用f_equal(或类似的)仅在不丢失信息的情况下，例如归纳构造函数。

Answer 1

这是另一种非黑客方式，使用 Ltac2(在 Ltac2 作者 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.

您可以在 https://coq.github.io/doc/master/refman/proof-engine/ltac2.html 找到 Ltac2 文档。它将与 Coq 8.11 一起发布，但与之前版本的 Coq 兼容的源代码可以在 https://github.com/coq/ltac2/branches/all 的各个分支中找到。 .