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

Coq seemingly refuses to recognize a simple substitution of a propositional formula for a propositional variable?

在多次失败后,我发现 Coq 做了一件我不明白的奇怪事情。 抱歉涉及代码,我无法隔离一个更简单的示例。 我有一个公式,我在三个变量 pqr 中调用 trident。 然后我简单地写出这个公式的一个实例,用 a <-> b 代替 pa 代替 qb 代替 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.

a lemma stating that the result is equivalent to the substitution into trident as above

对于 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.