Coq 似乎拒绝承认命题公式对命题变量的简单替换？

Question

经过多次失败后，我发现 Coq 做了一件我不明白的奇怪事情。抱歉涉及的代码，我无法隔离一个更简单的示例。我有一个包含trident三个变量的公式p，q, r。a <-> b然后，我简单地用in place of p、ain place ofq和bin place of写出该公式的一个实例r，并尝试证明一个引理，表明结果相当于trident上面的代入。当试图证明我被第一个子目标困住时，它写着

 a, b : Prop
  H : b
  ============================
  a \/ (a <-> b)

这显然是无法证明的：如果b假设为真，那么就a \/ (a <-> b)变为正义a，并且没有理由它为真。

这是完整的代码：

From Coq Require Import Setoid.

Definition denseover (p q : Prop) := (p -> q) -> q.

Definition trident (p q r : Prop) :=
  (
       (denseover p (q \/ r)) 
    /\ (denseover q (r \/ p))
    /\ (denseover r (p \/ q))
  ) -> (p \/ q \/ r).

Lemma triexpand : forall a b : Prop,
     ((a <-> b) \/ a \/ b)
<-> ((a \/ (a -> b)) /\ (b \/ (b -> a))).

Proof.
tauto.
Qed.

Lemma substritwo : forall a b : Prop,
   (trident (a <-> b) a b)
<->
   (
    (
         (denseover (a <-> b) (a \/ b)) 
      /\ (denseover a (b \/ (a <-> b)))
      /\ (denseover b (a \/ (a <-> b)))
    ) -> ((a <-> b) \/ a \/ b)
   ).

Proof.
  unfold trident, denseover.
  split.
  rewrite triexpand.
  split.
  destruct H.
  destruct H0.
  destruct H.
  destruct H0.
  destruct H.
  destruct H0.
  intuition.

Answer 1

引理表明结果相当于上面替换为三叉戟

对于使用诸如 之类的策略的 Coq 来说，这应该是微不足道的easy。它不起作用的事实让我发现你的引理改变了析取的顺序：第三个语句denseover是

denseover r (p \/ q)

trident在和的定义中

denseover b (a \/ (a <-> b))

在引理中，而不是denseover b ((a <-> b) \/ a).

如果你改变这个，easy就可以了。

但假设您想证明所述引理。那么论证是 是\/可交换的，并且您不应该分解该语句，您应该使用交换引理重写，该引理称为or_comm。有趣的是，以下内容不起作用：

Proof.
  intros a b.
  rewrite (or_comm a (a <-> b)).

它给出了一个看起来很可怕的错误。这就是为什么它不应该工作的原因：就当前目标而言，denseover可以是任何东西，并且我们事先不知道用denseover等效（但不相等！）参数替换参数 会给出相同的结果。据 Coq 所知，在不检查 的定义的情况下denseover，它可以匹配析取，并且在左右分支中表现不同。

在这种情况下，只需展开即可解决问题denseover。由于这是一个简单的含义链，Coq 知道用等效语句重写是可以的：

Proof.
  intros a b.
  unfold trident, denseover.
  now rewrite (or_comm a (a <-> b)).
Qed.