lean - 什么是 Coq 的“修复”关键字在精益中创建固定点的等价物

Question

我正在尝试将 Coq 术语的字面翻译成精益术语，但意识到我不知道如何翻译 Coq 原语fix，如下所示：

Definition Fac : nat -> nat :=
    fix f (n:nat) : nat :=
        match n with
        | 0     => 1
        | S p   => S p * f p
        end.

我不是在问如何在精益文档中很好地解释的归纳类型上定义递归函数，而是如何定义“递归让”，即其主体调用自身的 lambda 抽象。我假设精益中存在等效的原语。

谢谢你。

Answer 1

有一个关于这个here的讨论。据我所知，它没有很好的符号。

您可以获得的最接近的是nat直接或well_founded.fix直接使用递归器。

例如

def fact (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, nat.rec_on n 1 (λ n fact, (n + 1) * fact) in
f n

或者

def fact' (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, well_founded.fix nat.lt_wf 
  (λ n fact, show ℕ, from nat.cases_on n (λ _, 1)
    (λ n fact, (n + 1) * fact n n.lt_succ_self) fact) 
  n in
f n