在 Isabelle 中证明函数定义的正确性答案

【问题标题】：proving function definition correctness in Isabelle在 Isabelle 中证明函数定义的正确性
【发布时间】：2014-01-27 14:20:00
【问题描述】：

我想使用function 关键字定义来证明函数定义的正确性。下面是对自然数的通常归纳定义的加法函数的定义：

theory FunctionDefinition
imports Main

begin

datatype natural = Zero | Succ natural

function add :: "natural => natural => natural"
where 
  "add Zero     m = m"
| "add (Succ n) m = Succ (add n m)"

Isabelle/JEdit 向我展示了以下子目标：

goal (4 subgoals):
 1. ⋀P x. (⋀m. x = (Zero, m) ⟹ P) ⟹ (⋀n m. x = (Succ n, m) ⟹ P) ⟹ P
 2. ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma
 3. ⋀m n ma. (Zero, m) = (Succ n, ma) ⟹ m = Succ (add_sumC (n, ma))
 4. ⋀n m na ma. (Succ n, m) = (Succ na, ma) ⟹ Succ (add_sumC (n, m)) = Succ (add_sumC (na, ma)) 
Auto solve_direct: ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma can be solved directly with
  Product_Type.Pair_inject: (?a, ?b) = (?a', ?b') ⟹ (?a = ?a' ⟹ ?b = ?b' ⟹ ?R) ⟹ ?R

使用

apply (auto simp add: Product_Type.Pair_inject)

我明白了

goal (1 subgoal):
 1. ⋀P a b. (⋀m. a = Zero ∧ b = m ⟹ P) ⟹ (⋀n m. a = Succ n ∧ b = m ⟹ P) ⟹ P

目前尚不清楚如何进行。到底，这是解决这个问题的正确方法吗？

我知道如果我使用 fun 定义，Isabelle 会自动执行此操作 -- 我想了解如何手动执行此操作。

【问题讨论】：

标签： function isabelle

【解决方案1】：

tutorial on the function package 在第 3 节中提到 fun f where ... 缩写

function (sequential) f where ...
by pat_completeness auto
termination by lexicographic_order

这里的pat_completeness 是function 包中的一种证明方法，它自动证明数据类型构造函数模式的完整性。这是您必须证明的第一个子目标。建议在auto之前应用pat_completeness，因为auto改变了目标的句法结构，pat_completeness在auto之后可能不起作用。

如果您想在没有pat_completeness 的情况下证明模式完整性，您应该尝试对所有函数参数进行案例分析，即您的示例中的case_tac a。

【讨论】：

另外，如果你想手动证明终止，apply (relation R) 非常有用，其中R 是函数参数的一个有根据的关系，它表示两个参数中的哪一个是smaller另一个。通常，您会希望使用measure f 作为这种关系，其中f 是从函数参数类型到nat 的函数，并且基本上将函数参数映射到它们的size。

【解决方案2】：

Manuel 已经在他的评论中提到了它，但我认为更详细的示例可能会有所帮助。以下是您可以手动执行的操作：

首先你像往常一样指定你的函数

function add :: "natural => natural => natural"
where 
  "add Zero     m = m" |
  "add (Succ n) m = Succ (add n m)"

然后你证明给定的模式涵盖了所有情况

  by (pat_completeness) auto

然后你处理终止。例如，每个datatype 都带有一个size 函数，您可能会注意到add 的第一个参数在每次递归调用时都会严格减小大小。默认情况下，function 会将函数的所有参数捆绑到一个元组中作为终止证明，即，在您使用单对(n, m)。因此，如果你想告诉系统它应该使用 first 参数的大小，你可以这样做：

termination add
  apply (relation "measure (size o fst)")

这将产生剩余的目标：

goal (2 subgoals):
 1. wf (measure (size o fst))
 2. !!n m. ((n, m), Succ n, m) : measure (size o fst)

也就是说，你必须证明给定的关系是有根据的（这对于measures 来说是微不足道的，因为它们总是有根据的，因为它们是通过将参数映射到自然数然后使用 less-比自然的关系）和，对于每个递归调用，参数实际上都在给定的关系中。 simp 很容易分派这两个目标。

  apply simp
  apply simp
done

【讨论】：