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

这是一种仅使用一点 Ltac 就可以将 f_equal 专门化为归纳构造函数的方法：

Ltac f_equal_ind :=
  match goal with
  | [ |- ?G ] =>
    tryif
      (tryif assert (~ G); [ injection |]
       then fail else idtac)
    then
      fail "Not an inductive constructor"
    else
      f_equal
  end.

Require Import List.
Import ListNotations.

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

Require Import Arith.

Goal 4 mod 2 = 2 mod 2.
Fail f_equal_ind.

(* The command has indeed failed with message:
   In nested Ltac calls to "f_equal_ind" and "f_equal_ind", last call failed.
   Tactic failure: Not an inductive constructor. *)

我必须说结果特别复杂，如果有更简单的方法我也不会感到惊讶。我的想法是测试我们是否正在使用 injection which expects a negated primitive equality. The nested tryif 进行原始相等性工作，因为 assert (~ G); [ injection |] 部分仅用于测试，但我们不想保留由此创建的子目标。

Answer 2

这里有一个替代方法，non-hackish，使用 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. 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 找到 Ltac2 文档。

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

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

coq

coq-tactic