Lean证明中如何代入flip_mytree定义完成双翻转等价证明

你当前证明卡壳是三个实操误区导致的：

• 递归定义函数的化简规则，不会默认暴露在可重写的上下文里，直接调用rw无法匹配到你书写的分支定义规则
• 仅用cases t拆分归纳变量，没有自动生成branch节点对应的左右子树归纳假设，就算强行完成两次定义展开，最后一步递归替换也没有可用的前置等式
• 调用rw时直接传入函数名flip_mytree本身，但rw的输入要求是等式命题，不存在名为flip_mytree的全局等式定理，自然会出现匹配失败的情况

1. 替换变量拆分战术 #

把原来的cases t替换为induction t。这个战术会自动为归纳类型的每个构造子生成对应的证明分支，同时为branch节点自动生成左右子树的归纳假设：也就是自动给你提供“左子树连续两次翻转等于原左子树”、“右子树连续两次翻转等于原右子树”的可直接重写的等式。如果硬用cases t完成拆分，后续需要手动构造这两个假设，证明过程会非常冗余。

2. 触发flip_mytree定义展开的两种可靠方式 #

你提到的flip_mytree分支规则，是Lean编译def定义时自动生成的等式引理，不需要手动编写，有两种稳定的展开方式：

• 调用simp [flip_mytree]：simp战术会自动加载该def对应的所有化简规则，匹配目标中所有的函数应用表达式做自动替换。
• 手动提取内置等式引理：如果不想用simp，可通过have h_branch := flip_mytree.equations._eqn_2，直接拿到完整的分支展开规则∀ (a : A) (l r : mytree A), flip_mytree (mytree.branch a l r) = mytree.branch a (flip_mytree r) (flip_mytree l)，之后就可以正常用rw h_branch完成替换。

universes u

inductive mytree (A : Type u) : Type u
| leaf : A → mytree
| branch : A → mytree → mytree → mytree

def flip_mytree {A : Type u} : mytree A → mytree A
| t@(mytree.leaf _)     := t
| (mytree.branch a l r) := mytree.branch a (flip_mytree r) (flip_mytree l)


theorem flip_flip {A : Type u} {t : mytree A} : flip_mytree (flip_mytree t) = t :=
begin
  induction t with
  | leaf val =>
    -- 叶子分支：翻转后仍为原叶子，自反性成立
    rfl
  | branch node_val left right ih_left ih_right =>
    -- 展开内层flip的分支定义
    simp [flip_mytree],
    -- 展开后目标等价于：flip_mytree (mytree.branch node_val (flip_mytree right) (flip_mytree left)) = mytree.branch node_val left right
    -- 展开外层flip的分支定义
    simp [flip_mytree],
    -- 展开后目标等价于：mytree.branch node_val (flip_mytree (flip_mytree left)) (flip_mytree (flip_mytree right)) = mytree.branch node_val left right
    -- 用左右子树的归纳假设完成最终替换
    rw [ih_left, ih_right]
end

• 不要尝试手写flip_mytree (mytree.branch a l r) = ...的规则当引理，Lean自动生成的等式是带全量词绑定的，手写表达式因为变量命名、作用域的细微差异，经常会出现模式匹配失败的情况。
• 纯结构等值判断用cases，递归结构的性质证明必须用induction，否则永远拿不到递归成立的前置假设，无法完成嵌套结构的证明。

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