如何在 Coq 中引发异常？（在比赛中......结束）

Question

我需要定义递归定义，但我还不知道如何正确地做它()。所以我想要部分定义的函数，它会说明何时需要编写额外的递归级别。

Context (qsigT: forall (A : Type) (P : forall a : A, Type), Type).
Context (qpr1: forall (A : Type) (P : forall a : A, Type), (@qsigT A P) -> A ).
Record Category :={
 ty:>Type
}.
Context (uc:Category).
Context (mO mS: uc -> Type).

 Definition ur0:= (@qsigT uc  (fun x => mO (x)                       ) ).
 Definition ur1:= (@qsigT ur0 (fun x => mS (qpr1 _ _ x)                   ) ).
 Definition ur2:= (@qsigT ur1 (fun x => mS (qpr1 _ _ (qpr1  _ _ x))             ) ).
 Definition ur3:= (@qsigT ur2 (fun x => mS (qpr1 _ _ (qpr1  _ _ (qpr1 _ _ x)))       ) ).
 (*and so on ...*)

 Definition ur (n: nat) := (match n with
  |0 => ur0
  |1 => ur1
  |2 => ur2
  |_ => ur3
  (*|_ => error*)
 end).

1)是否可以对所有大于3的自然数创建异常？（模式匹配期间）

2)有没有低级乐器不会强制我使用monades？

3)是否可以在 Coq 中对所有自然数定义我的函数 'ur'？

4)是否有某种组合器可以应用函数 'pr1' n 次？

5)我应该创建 5 个不同的问题（元上有一个 :-)）还是正确的提问方式？

Answer 1

1) Is it possibly to create exception on all natural numbers greater than 3? (during the pattern matching)

没有。 Coq 是一种完整的语言。标准模式是让你的函数成为 return option T 类型 T，所以你在 partiality monad 中工作。示例：

Definition ur (n: nat) := (match n with
  | 0 => Some ur0
  | 1 => Some ur1
  | 2 => Some ur2
  | 3 => Some ur3
  | _ => None
 end).

2) Is there a low level instrument which will not coerce me to use monads?

见上文。是否要称呼它 "monad" 由您决定。

另一种方法是在 "fail" 模式匹配时让 return 具有 "default" 值 urF。在很多情况下，这种方法比选项类型更方便。

3) Is it possibly to define my function 'ur' on all natural numbers in Coq?

我也这么认为。请提供缺少的定义，我们可能会尝试。

4) Is there some kind of combinator that will apply function 'pr1' n times?

原则上是的，但这取决于您想要的确切类型。

5) Shall I create 5 different question (with one on the meta :-) ) or it is right way to ask?

也许吧。这道题最大的问题是代码没有独立。

如何在 Coq 中引发异常？（在比赛中......结束）

How to raise exception in Coq?(in match ... end)

coq