Coq多态多分支归纳树高度计算错误 证明树高为3得6的问题

练习目标 #

• 完成Coq练习：证明自定义树结构的高度为3

遇到的阻碍 #

• 前期查找的Coq参考实现多为二叉树场景，本次自定义的树节点可挂载任意数量的子节点，和二叉树的实现逻辑不匹配
• 编写完代码运行后，在证明步骤执行simpl化简，得到的证明目标为6 = 3，和预期的树高3完全不符
• 无法定位现有定义中的错误点，也不清楚错误产生的根本原因
• 不清楚练习给出的let表达式内嵌递归的提示写法如何应用在当前树高计算的场景中

相关代码片段 #

自定义树的归纳类型定义 #

Inductive tree (X:Type) : Type :=
  | empty : tree X
  | branch : X -> list (tree X) -> tree X.

Arguments tree {X}.
Arguments empty {X}.
Arguments branch {X}.

测试用树实例定义 #

Definition mytree :=
  branch 1 [ branch 5 [ branch 2 [empty] ] ;  branch 8 [empty] ;
          branch 7 [ branch 3 [empty];branch 4 [empty] ] ].

当前编写的高度计算函数 #

Fixpoint height {X: Type} (node: @tree X) : nat :=
  match node with
  | empty => 0
  | branch _ l => S (match l with 
                        | [] => 0
                        | h::t => S (height h)
                       end)
  end.

待证明的单元测试目标 #

Example test_height:
  height mytree = 3.
Proof.
  simpl. (* 执行化简后，目标变为 6 = 3，与预期完全不符 *)

练习给出的参考提示 #

• 可使用let表达式定义递归或相互递归函数，示例写法如下：

Definition a := let fix f (x:nat) := match x with
| O => O
| S y => f y
end
in f 2.

目前对这类let内嵌递归的写法如何适配当前练习需求没有清晰思路

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