1

我在归纳类型event上定义了三个相互递归函数，使用两种不同的方式：使用with 和fix关键字，但是，Coq 分别抱怨主要参数和The reference ... was not found in ...。函数的两种实现如下：

Require Import List.

Parameter max: list nat -> nat.
Inductive event : Type := node: list event -> event. 
Parameter eventbool : forall (P:event->Prop) (e:event), {P e} + {~ P e}.
Definition event_sumbool_b (e: event) (p: event -> Prop) : bool :=
  if eventbool p e then true else false.

Fixpoint parentround (e: event) : nat :=
  match e with
 | node l =>  max (rounds l)
 end

 with rounds l := 
   match l with 
   | nil => 0::nil 
   | h::tl => round h:: rounds tl
   end 

 with round e := 
   if event_sumbool_b e roundinc then parentround e + 1 else parentround e

 with roundinc e :=
  exists S:list event, (forall y, List.In y S /\ round y = parentround e).

Coq 抱怨递归调用 round 的主要参数等于“h”而不是“tl”。尽管如此，呼叫回合中的h是e的子项。按照Recursive definitions over an inductive type中的想法，我将parentround替换为以下内容：

Fixpoint parentround (e: event) : nat :=

 let round := 
   ( fix round (e: event) : nat := 
      if event_sumbool_b e roundinc then parentround e + 1 else parentround e
   ) in

 let roundinc := 
   ( fix roundinc (e: event) : Prop :=
     exists S:list event, (forall y, List.In y S /\ round y = parentround e)
   ) in

 match e with
 | node l =>  max (rounds l)
 end

 with rounds l :=
   match l with 
   | nil => 0::nil 
   | h::tl => round h:: rounds tl
   end.

它现在抱怨缺少roundinc的定义。

请帮我定义这三个相互递归的函数parentround、round和roundinc。

编辑定义中有第四个函数轮次，但是到目前为止还没有问题。

4

2 回答 2

2

弄清楚你想要计算什么对我来说有点困难，我会从以下内容开始：

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import bigop.

Definition max_seq l := \max_(x <- l) x.

Inductive event : Type :=
  node : seq event -> event.

Fixpoint round_lvl (e : event) : nat :=
  (* XXX: Missing condition *)
  let cond_inc x := round_lvl x in
  match e with
  | node l => max_seq (map cond_inc l)
  end.

但是我在解析存在条件的含义时遇到了麻烦。我建议您先尝试在没有Coq 代码的情况下表达问题，然后可能会出现解决方案。

于 2016-09-07T18:34:35.560 回答
1

T根据我的经验，在 type和 on 上定义互函数真的很困难list T。我记得 Coq-club 上有一篇关于这个 subjet 的帖子，我必须再次找到它。

event“简单”的解决方案是在您定义的地方同时定义一个互感类型event_list。但是，您将无法使用列表库...

于 2016-09-07T07:05:38.393 回答