Coq中证明二叉树两次翻转等于原树的归纳步骤求助

你额外对节点的左右子树t1、t2做了不必要的嵌套归纳，导致原本可以一步处理的通用节点场景被拆成了4个分支，除了你已经完成的Leaf-Leaf分支外，剩下3个就是你当前看到的待证子目标。
对树这类递归结构的归纳证明，只需要对整个树结构做一次结构归纳，就能自动获得左右子树的归纳假设，不需要额外嵌套归纳。

当你对参数t做归纳后，节点分支的上下文会自动给出两个归纳假设：

• IHt1 : invertTree (invertTree t1) = t1（左子树翻转两次等于自身）
• IHt2 : invertTree (invertTree t2) = t2（右子树翻转两次等于自身）
  你的证明目标是invertTree (invertTree (Node t1 t2)) = Node t1 t2，步骤如下：

1. 用simpl/compute展开invertTree的定义：两次翻转Node t1 t2后，结果会变成Node (invertTree (invertTree t1)) (invertTree (invertTree t2))
2. 用IHt1、IHt2两个归纳假设重写目标，就能得到等号右侧的Node t1 t2
3. 用reflexivity完成证明即可

Proof.
  induction t.
  - (* 处理叶节点基础情况 *)
    compute. reflexivity.
  - (* 处理节点归纳情况 *)
    simpl.
    rewrite IHt1.
    rewrite IHt2.
    reflexivity.
Qed.

即使你保留了嵌套归纳的写法，3个子目标的处理逻辑是统一的：对每个子目标先执行simpl展开定义，再依次rewrite IHt1、rewrite IHt2，最后reflexivity就能全部证明完成，只是这种写法有大量冗余步骤，不推荐。

内容的提问来源于stack exchange，提问作者Felipe Balbi