coq - 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的各个分支中找到。

Answer 2

这是一种f_equal仅使用一点 Ltac 专门针对归纳构造函数的方法：

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期望否定的原始相等性来处理原始相等性。嵌套tryif是因为该assert (~ G); [ injection |]部分仅用于测试，但我们不想保留它创建的子目标。