为什么我不能将 f_equal 应用于假设？答案

【问题标题】：Why can I not apply f_equal to a hypothesis?为什么我不能将 f_equal 应用于假设？
【发布时间】：2022-05-03 03:49:24
【问题描述】：

在我的假设列表中，我有：

X : Type
l' : list X
n' : nat
H : S (length l') = S n'

我的目标是length l' = n'。

所以我尝试了f_equal in H。但我收到以下错误：

Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]).

我是否认为我应该能够将f_equal 应用于H 以删除双方的S？

【问题讨论】：

标签： coq

【解决方案1】：

f_equal 是关于平等的一致性。它可以用来从x = y 证明f x = f y。但是，它不能用于从f x = f y 推导出x = y，因为这通常不是真的，只有当f 是单射时。

这是一个特殊情况，因为S 是一个归纳类型的构造函数，而构造函数确实是单射的。例如，您可以使用inversion H 之类的策略来获得所需的平等。

涉及f_equal 的另一个解决方案是应用删除S 之类的函数

Definition removeS n :=
  match n with
  | S m => m
  | 0 => 0
  end.

然后使用

apply (f_equal removeS) in H.

【讨论】：

【解决方案2】：

f_equal 告诉你如果x = y，那么f x = f y。换句话说，当你有x = y 和需要f x = f y，你可以使用f_equal。

你的情况正好相反。你有f x = f y和你需要x = y，所以你不能使用f_equal。

如果您考虑一下您的结论，则仅当S 是注入时才成立。你需要一个不同的策略。

【讨论】：