相关疑难解决方法(0)

我试图在Coq中定义Ackermann-Peters函数,我收到一条我不明白的错误消息.正如你所看到的,我把a, bAckermann 的论据打包成一对ab; 我提供了一个定义参数的排序函数的排序.然后我使用Function表单来定义Ackermann本身,为它提供ab参数的排序函数.

Require Import Recdef.    
Definition ack_ordering (ab1 ab2 : nat * nat) :=
    match (ab1, ab2) with
    |((a1, b1), (a2, b2)) => 
       (a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))   
    end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, …

有喜欢的战术什么simpl的Program FixpointS'

特别是,如何证明以下琐碎的陈述？

Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => 0
| S n' => S (bla n')
end.

Lemma obvious: forall n, bla n = n. 
induction n. reflexivity.
(* I'm stuck here. For a normal fixpoint, I could for instance use 
simpl. rewrite IHn. reflexivity. But here, I couldn't find a tactic 
transforming bla (S n) to S (bla n).*)

显然,Program Fixpoint这个玩具示例没有必要,但我在一个更复杂的设置中面临同样的问题,我需要证明Program Fixpoint手动终止.

我想使用Program Fixpoint或Function在Coq中定义以下函数:

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 …

与许多其他人不同,Coq接受可选的显式参数,该参数可用于指示固定点定义的递减结构.

来自Gallina规范,1.3.4,

Fixpoint ident params {struct ident0 } : type0 := term0

定义语法.但是从中我们已经知道它必须是一个标识符,而不是一般的衡量标准.

然而,一般来说,存在递归函数,终止不是很明显,或者实际上是,但终止检查器很难找到减少的结构.例如,以下程序交错两个列表,

Fixpoint interleave (A : Set) (l1 l2 : list A) : list A :=
  match l1 with
  | [] => []
  | h :: t => h :: interleave l2 t
  end

这个功能明显终止,而Coq无法弄明白.原因既不是也l1没有l2减少每个周期.但是,如果我们考虑一个被定义为的措施length l1 + length l2呢？然后,此度量明显减少每次递归.

所以我的问题是,在复杂的情况下,代码不能直接以终止可检查的方式组织,你如何教育coq并说服它接受修复点定义？