Isabelle中trev(trev t)=t的证明难题求助

问题描述 #

我正在做《高阶逻辑证明助手》第42页的Exercise 3.4.3习题，要求定义递归反转项中所有函数符号参数顺序的函数trev（类型为('v, 'f) Nested.term ⇒ ('v, 'f) Nested.term），并证明trev(trev t) = t。

给定的term数据类型定义：

datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"

我定义的trev函数：

primrec trev :: "('v,'f)term ⇒ ('v,'f)term"
where
"trev (Var x) = Var x" |
"trev (App f ts) = App f (rev (map trev ts))"

尝试过程 #

1. 提出核心引理并启动归纳证明：

lemma "trev (trev t) = (t::('v,'f)term)"
  apply(induct_tac t)
   apply(simp_all)

得到目标：

1. ⋀x2. (⋀x2a. x2a ∈ set x2 ⟹ trev (trev x2a) = x2a) ⟹ rev (map trev (rev (map trev x2))) = x2

2. 证明辅助引理map_rev_map处理列表反转与映射的交换律：

lemma map_rev_map : "map f (rev (l:: 'a list)) = rev (map f l)"
  apply(induct_tac l)
   apply(simp_all)
  done

将其加入原引理化简后，目标变为：

1. ⋀x2. (⋀x2a. x2a ∈ set x2 ⟹ trev (trev x2a) = x2a) ⟹ map (trev ∘ trev) x2 = x2

3. 尝试证明辅助引理map_trev_trev，但无法完成替换：

lemma map_trev_trev : "⟦∀ t. trev (trev t) = t ⟧ ⟹ map (trev ∘ trev) ts = ts"

展开函数复合后得到：

1. ∀t. trev (trev t) = t ⟹ map (λx. trev (trev x)) ts = ts

尝试用drule spec或erule ssubst将trev(trev x)替换为x，但未成功。

解决方案 #

不需要单独证明第二个辅助引理，直接在原引理的证明流程中，利用归纳假设结合列表映射的性质即可完成证明：

完整证明代码 #

datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"

primrec trev :: "('v,'f)term ⇒ ('v,'f)term"
where
"trev (Var x) = Var x" |
"trev (App f ts) = App f (rev (map trev ts))"

lemma map_rev_map : "map f (rev (l:: 'a list)) = rev (map f l)"
  apply(induct_tac l)
   apply(simp_all)
  done

lemma "trev (trev t) = (t::('v,'f)term)"
  apply(induct_tac t)
   apply(simp_all add: map_rev_map)
  apply(simp add: comp_def)  (* 展开函数复合 *)
  apply(rule map_eq_idI)     (* 利用映射等于恒等函数的判定规则 *)
  apply(erule meta_spec)     (* 实例化归纳假设中的元素 *)
  apply(assumption)          (* 应用归纳假设 *)
  done

关键步骤解释 #

• comp_def：展开trev ∘ trev为λx. trev (trev x)，让simp能识别函数复合的具体形式。
• map_eq_idI：这条规则的内容是(∀x∈set xs. f x = x) ⟹ map f xs = xs，正好匹配我们的场景——归纳假设已经保证了x2中所有元素都满足trev(trev x2a)=x2a，应用这条规则后只需验证每个元素的性质。
• erule meta_spec和assumption：将归纳假设中的全称量词实例化为当前元素，再直接应用假设完成证明。

也可以用更简洁的方式，直接依赖simp的自动化简能力，将上述步骤合并为：

lemma "trev (trev t) = (t::('v,'f)term)"
  apply(induct_tac t)
   apply(simp_all add: map_rev_map comp_def map_eq_idI)
  done

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