#3. 二叉树镜像证明

来源：First Theorem Proving Competition2 AC / 2 提交 · 100%

题目描述

基于以下定义：

  • 二叉树 tree
  • 二叉树的镜像 mirror
  • 一个二叉树是对称的 (symmetric) 如果它等于自身的镜像

如果直接使用对称性的定义来检查一个二叉树是否对称，需要首先计算二叉树的镜像，然后做相等性比较，效率不高。

我们可以通过以下方式定义更高效的对称性检查：

  • check_mirror 检查两个二叉树是否互为镜像
  • check_symmetric 则检查两个子树是否互为镜像

任务

证明 check_mirror 和 check_symmetric 的正确性：

1. check_mirror_correct (50 分)

theorem check_mirror_correct {A : Type} (t1 t2 : Tree A) :
    check_mirror t1 t2 ↔ t1 = mirror t2

2. check_symmetric_correct (50 分)

theorem check_symmetric_correct {A : Type} (t : Tree A) :
    check_symmetric t ↔ is_symmetric t

分值

  • check_mirror_correct: 50 分
  • check_symmetric_correct: 50 分

总计: 100 分