如何在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)所以你可以用归纳假设