Coq中如何将等式两边的公共子项泛化为新变量

直接替换t3的逻辑误区 #

你不能直接将目标中的N t1 t2替换为t3并套用性质，原因很简单：size (flatten t3) = size t3正是你当前要证明的flatten_size引理本身，N t1 t2是归纳步的当前节点，你还没有证明它满足这个性质，直接套用属于循环论证，逻辑上不成立。
你现有的归纳假设仅覆盖子节点t1和t2，无法直接作用于父节点N t1 t2，需要借助你已经证明的flatten_aux_size辅助引理来过渡。

最终证明实现 #

你最后采用的方案是完全正确的，完整可运行的证明代码如下：

Require Import Nat.
Require Import Arith.

Inductive bin : Type :=
    L : bin
  | N : bin -> bin -> bin.

Fixpoint flatten_aux (t1 t2 : bin) : bin :=
  match t1 with
    L => N L t2
  | N t'1 t'2 => flatten_aux t'1  (flatten_aux t'2 t2)
  end.

Fixpoint flatten (t : bin) : bin :=
  match t with
    L => L
  | N t1 t2 => flatten_aux t1 (flatten t2)
  end.

Fixpoint size (t : bin) : nat :=
  match t with
    L => 1
  | N t1 t2 => 1 + size t1 + size t2
  end.


Lemma flatten_aux_size :
  forall t1 t2, size (flatten_aux t1 t2) =
    size t1 + size t2 + 1.
  induction t1.
  { intros t2.
    simpl.
    ring.
  }
  { intros t2; simpl.
    rewrite IHt1_1.
    rewrite IHt1_2.
    ring.
  }
Qed.

Lemma flatten_size : forall t, size (flatten t) = size t.
  induction t.
  { trivial.
  }
  { simpl.
    rewrite flatten_aux_size.
    rewrite <- IHt1.
    rewrite <- IHt2.
    rewrite Nat.add_comm.
    simpl.
    reflexivity.
  }
Qed.

证明步骤说明 #

1. 进入归纳步执行simpl后，目标展开为size (flatten_aux t1 (flatten t2)) = 1 + size t1 + size t2
2. 调用rewrite flatten_aux_size将左侧展开为size t1 + size (flatten t2) + 1
3. 用归纳假设IHt1、IHt2将flatten后的子节点大小替换为原节点大小
4. 用自然数加法交换律调整项的顺序，两侧等式即可匹配，最后用reflexivity完成证明

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