Coq深层公理应用方法：MT1A证明遇合一失败问题

让我们一步步拆解你的问题，先理清楚当前的困境和可用的工具：

首先，你尝试直接apply MT1时遇到合一失败，原因很简单：MT1的结论和你的目标结构不匹配。MT1是从z = c(x,y)推出a(z) = x /\ b(z) = y，但你的目标是要证明x = example /\ a x <> x /\ b x <> x，而且x被定义为a(c(example, b example))——Coq没法自动把这两个结构对齐，需要我们手动引导证明步骤。

用MT1公理的解决方案 #

MT1虽然是单向的，但足够完成证明，关键是先把目标拆分成可匹配的子项，步骤如下：

Lemma MT1A : forall x: MT, x = a (c(example, b example)) -> x = example /\ a x <> x /\ b x <> x.
Proof.
  unfold example.  (* 先展开example，让内部结构清晰可见 *)
  intros x H.      (* 引入变量x和假设H: x = a(c(c(NIL,e NIL), b(c(NIL,e NIL)))) *)
  rewrite H.       (* 把目标里的x全部替换成a(c(...))，简化目标 *)
  split.           (* 拆分合取式，分三个子目标证明 *)
  
  - (* 第一个子目标：证明a(c(c(NIL,e NIL), b(c(NIL,e NIL)))) = c(NIL,e NIL) *)
    apply MT1.      (* 应用MT1，此时需要提供前提z = c(x,y) *)
    reflexivity.    (* 这里z就是c(c(NIL,e NIL), b(c(NIL,e NIL)))，x是c(NIL,e NIL)，y是b(c(NIL,e NIL))，等式自成立 *)
  
  - split.          (* 拆分剩下的两个不等式子目标 *)
    + (* 证明a(c(NIL,e NIL)) <> c(NIL,e NIL) *)
      (* 先证明example满足MT3的前提：example = c(a(example), b(example)) *)
      assert (example = c(a(example), b(example))).
      { unfold example. rewrite (MT1 _ _ example (eq_refl example)). reflexivity. }
      (* 应用MT3的正向推导，从前提得到a(example) <> example *)
      apply (proj1 (MT3 example)).
      assumption.
    
    + (* 证明b(c(NIL,e NIL)) <> c(NIL,e NIL) *)
      (* 复用刚才的断言，或者重新证明一次 *)
      assert (example = c(a(example), b(example))).
      { unfold example. rewrite (MT1 _ _ example (eq_refl example)). reflexivity. }
      apply (proj2 (MT3 example)).
      assumption.
Qed.

用MT1bis公理的简化方案 #

MT1bis是双向等价（<->），比MT1更灵活——它既可以从z=c(x,y)推a(z)=x /\ b(z)=y，也可以反过来从a(z)=x /\ b(z)=y推z=c(x,y)。在这个证明里，MT1bis能让步骤更简洁，比如在证明example = c(a(example), b(example))时，我们可以直接用MT1bis的反向方向：

Lemma MT1A_bis : forall x: MT, x = a (c(example, b example)) -> x = example /\ a x <> x /\ b x <> x.
Proof.
  unfold example.
  intros x H.
  rewrite H.
  split.
  
  - apply MT1. reflexivity.  (* 和MT1的步骤一样，因为这里还是用正向推导 *)
  
  - split.
    + (* 用MT1bis简化断言 *)
      assert (example = c(a(example), b(example))).
      { apply (proj2 (MT1bis _ _ example)). split.
        apply (proj1 (MT1 _ _ example (eq_refl example))).
        apply (proj2 (MT1 _ _ example (eq_refl example))). }
      apply (proj1 (MT3 example)). assumption.
    
    + assert (example = c(a(example), b(example))).
      { apply (proj2 (MT1bis _ _ example)). split.
        apply (proj1 (MT1 _ _ example (eq_refl example))).
        apply (proj2 (MT1 _ _ example (eq_refl example))). }
      apply (proj2 (MT3 example)). assumption.
Qed.

为什么之前的rewrite没成功？ #

你尝试rewrite失败，大概率是因为没有先把目标中的x替换成a(c(...))，或者没有拆分合取式——Coq的rewrite需要明确的等式方向和匹配的结构，直接在原始目标上rewrite很难对齐MT1的结论。

内容的提问来源于stack exchange，提问作者Roman Susi