Coq 中的二叉树反转

Question

我试图证明将二叉树反转两次会产生相同的二叉树。

所以我写了下面的归纳类型：

Inductive tree : Type :=
| Leaf (x : Type)
| Node (t1 : tree) (t2 : tree).

这里是反函数：

Fixpoint invertTree (t : tree) :=
  match t with
  | Leaf x => Leaf x
  | Node l r => Node (invertTree r) (invertTree l)
  end.

定理很简单：

Theorem involution_of_invert : forall t : tree,
    (invertTree (invertTree t)) = t.

基本情况很容易证明，我们从归纳证明开始，只需计算 -> 自反性。我很难理解归纳步骤。据我所知：

Proof.
  induction t.
  compute.
  reflexivity.
  induction t1, t2.
  compute.
  reflexivity.

我的剩余目标：

3 subgoals (ID 57)
  
  x : Type
  t2_1, t2_2 : tree
  IHt1 : invertTree (invertTree (Leaf x)) = Leaf x
  IHt2 : invertTree (invertTree (Node t2_1 t2_2)) = Node t2_1 t2_2
  ============================
  invertTree (invertTree (Node (Leaf x) (Node t2_1 t2_2))) =
  Node (Leaf x) (Node t2_1 t2_2)

subgoal 2 (ID 74) is:
 invertTree (invertTree (Node (Node t1_1 t1_2) (Leaf x))) =
 Node (Node t1_1 t1_2) (Leaf x)
subgoal 3 (ID 81) is:
 invertTree (invertTree (Node (Node t1_1 t1_2) (Node t2_1 t2_2))) =
 Node (Node t1_1 t1_2) (Node t2_1 t2_2)

如能提供任何提示，将不胜感激。我是 Coq 的新手（从这个问题中应该很清楚哈）。

谢谢

Answer 1

找到了解决方法，这里是：

Inductive tree : Type :=
| Leaf (x : Type)
| Node (t1 : tree) (t2 : tree).

Fixpoint invertTree (t : tree) :=
  match t with
  | Leaf x => Leaf x
  | Node l r => Node (invertTree r) (invertTree l)
  end.

Theorem involution_of_invert : forall t : tree,
    (invertTree (invertTree t)) = t.
Proof.
  induction t.
  compute.
  reflexivity.
  simpl.
  rewrite -> IHt1.
  rewrite -> IHt2.
  reflexivity.
Qed.

Coq 中的二叉树反转

Binary tree inversion in Coq

binary-tree

coq

theorem-proving