如何在 Coq 中推广方程两边的变量？

Question

我有这个目标

size (flatten (N t1 t2)) = size (N t1 t2)

N 是一个 bin 构造函数，如何用 t3 : bin 替换两边的 N t1 t2？

我的假设是

t1, t2 : bin
IHt1 : size (flatten t1) = size t1
IHt2 : size (flatten t2) = size t2

如果我可以将size (flatten (N t1 t2)) = size (N t1 t2)重写为size (flatten t3) = size t3那么我就可以应用我的假设来完成证明。

这是完整的代码

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.
    (* goal size (flatten (N t1 t2)) = size (N t1 t2) *)

最后我用的是这个方案

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.

Answer 1

为什么要size (flatten t3) = size t3？您的假设并未普遍量化，size (flatten t2) = size t2 对那个特定的 t2 成立（与 t1 相同）。如果没有更多详细信息，我们无法为您提供帮助，但我希望您更愿意根据 flatten t1 和 flatten t2 来展示 flatten 应用于 N t1 t2 时的行为，这将有助于您得出结论.

Answer 2

你使用 simpl 做了正确的事情：它部分评估了 size (flatten (N t1 t2)) 和 size (N t1 t2) 所以你可以使用你的归纳假设。

如何在 Coq 中推广方程两边的变量？

How to generalize a variable on both sides of an equation in Coq?

coq