为什么我不能在假设上应用f_ qual？

Question

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

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

我的目标是长度L'= n'。

因此，我在h 中尝试了f_equal。但是我会收到以下错误：

语法错误：[tatic：ltac_use_default]预期[tatic：tatic]之后（在[vernac：tactic_command]））。

我认为我应该能够应用<我错了代码> f_equal to h以删除双方的s？

Answer 1

f_equal是关于平等的一致性。它可用于证明fx = f y来自x = y。但是，它不能用于从fx = f y中推导x = y，因为这通常不正确，只有当f是注入时。

这是一种特殊的情况，因为s是归纳类型的构造函数，并且构造函数确实是注入性的。例如，您可以使用反转H之类的策略来获得所需的平等。

涉及f_equal的另一个解决方案是应用一个删除s喜欢的函数

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

，然后使用

apply (f_equal removeS) in H.

Answer 2

f_equal告诉您，如果x = y，则fx = f y。换句话说，当您有 x = y和需要 fx = f y时，您可以使用> f_equal。

您的情况是相反的。您有 fx = f y，并且您需要 x = y，因此您不能使用f_equal。

如果您考虑自己的结论，那么只有当s是注射时才正确。您需要其他策略。