Coq 证明了一个错误的列表假设答案

【问题标题】：Coq prove a false list assumptionCoq 证明了一个错误的列表假设
【发布时间】：2026-02-15 02:25:02
【问题描述】：

给定下一个定理。

Theorem rev_injective_helper : forall (l : natlist) (n : nat),
    [] = l ++ [n] -> False.
Proof.
  intros l n H.
  unfold app in H.
  induction l. all: inversion H.
Qed.

如何证明下一个目标？

1 subgoal
n : nat
l2 : natlist
H : [ ] = rev l2 ++ [n]
IHl2 : [ ] = rev l2 -> [ ] = l2
______________________________________(1/1)
[ ] = n :: l2

据我了解，这种情况下的假设是错误的H : [ ] = rev l2 ++ [n]如何完成证明？提前致谢！

更新。 缺少定义：

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil ⇒ l2
  | h :: t ⇒ h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ rev t ++ [h]
  end.

我试图证明这个定理：

Theorem rev_injective : forall (l1 l2 : natlist),
    rev l1 = rev l2 -> l1 = l2.

【问题讨论】：

您能否提供足够的信息来编译您的定义？
@pochinha 问题已更新，感谢您的评论

标签： coq

【解决方案1】：

正如您所说，您在上下文中有一个错误的假设，所以无论您试图证明什么，它都会源于虚假。要利用这一点，您可以使用exfalso 策略，将您当前的目标替换为False。那你应该可以从rev_injective_helper和H得出结论没有？

【讨论】：