我想使用 Coq 中的
不幸的是,此时我有一个证明义务:
类似地,如果使用
有没有一种方法可以不重构函数定义来实现这一点?(例如,我知道需要在此处内联
Isabelle 为了证明这个期望,让我展示一下在Isabelle中执行相同操作时会发生什么,使用的是
在终止证明中,我得到假设
请注意,Isabelle 在这里不需要手动终止证明,以下定义也可以正常工作:
这是因为
“function”命令使用的是“set ts”集合中的“t”,以确定终止证明只需要考虑这个部分。如果没有这样的引理可用,例如因为我定义了…
“并在`mapTree`中使用它,我得到了与Coq中相同的无法证明的证明义务。我可以通过声明`map'`的同余引理来使其再次工作,例如使用…”
Program Fixpoint
或 Function
来定义以下函数:Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.
Inductive Tree := Node : nat -> list Tree -> Tree.
Fixpoint height (t : Tree) : nat :=
match t with
| Node x ts => S (fold_right Nat.max 0 (map height ts))
end.
Program Fixpoint mapTree (f : nat -> nat) (t : Tree) {measure (height t)} : Tree :=
match t with
Node x ts => Node (f x) (map (fun t => mapTree f t) ts)
end.
Next Obligation.
不幸的是,此时我有一个证明义务:
height t < height (Node x ts)
,但不知道t
是否是ts
的成员。类似地,如果使用
Function
而不是Program Fixpoint
,只是Function
会检测到问题并中止定义:
Error:
the term fun t : Tree => mapTree f t can not contain a recursive call to mapTree
我期望得到一个证明义务,其形式为In t ts → height t < height (Node x ts)
。有没有一种方法可以不重构函数定义来实现这一点?(例如,我知道需要在此处内联
map
的定义的解决方法 - 我想避免这种情况。)Isabelle 为了证明这个期望,让我展示一下在Isabelle中执行相同操作时会发生什么,使用的是
function
命令,它与Coq的Function
命令相关(据我所知)。theory Tree imports Main begin
datatype Tree = Node nat "Tree list"
fun height where
"height (Node _ ts) = Suc (foldr max (map height ts) 0)"
function mapTree where
"mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"
by pat_completeness auto
termination
proof (relation "measure (λ(f,t). height t)")
show "wf (measure (λ(f, t). height t))" by auto
next
fix f :: "nat ⇒ nat" and x :: nat and ts :: "Tree list" and t
assume "t ∈ set ts"
thus "((f, t), (f, Node x ts)) ∈ measure (λ(f, t). height t)"
by (induction ts) auto
qed
在终止证明中,我得到假设
t ∈ set ts
。请注意,Isabelle 在这里不需要手动终止证明,以下定义也可以正常工作:
fun mapTree where
"mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"
这是因为
map
函数具有形式为“同余引理”的特性。xs = ys ⟹ (⋀x. x ∈ set ys ⟹ f x = g x) ⟹ map f xs = map g ys
“function”命令使用的是“set ts”集合中的“t”,以确定终止证明只需要考虑这个部分。如果没有这样的引理可用,例如因为我定义了…
definition "map' = map"
“并在`mapTree`中使用它,我得到了与Coq中相同的无法证明的证明义务。我可以通过声明`map'`的同余引理来使其再次工作,例如使用…”
declare map_cong[folded map'_def,fundef_cong]
map
使用本地不动点进行了精确定义,并且终止检查器可以穿透其内部。如果我在不那么规范的情况下递归,而我确实需要良好基础的递归,该怎么办? - Joachim Breitner