coq --函数幂定义

Question

我感兴趣的是如何在Coq中将f定义为n：

​

​

基本上，作为练习，我想编写这个定义，然后确认我的算法实现了这个规范。在这里，Inductive定义似乎是合适的，但我无法像上面那样使它变得干净。什么是干净的Coq实现上面的？

Answer 1

使用gallais定义的pow_func函数，您可以将您的规范声明为引理，例如：

Lemma pow_func0: forall (A:Type) (f: A -> A) (x: A), pow_fun f O x = f x.

和

Lemma pow_funcS: forall (n:nat) (A: Type) (f: A->A) (x:A), pow_fun f (S n) x = f (pow_fun f n x).

通过展开定义，证明应该是微不足道的。

Answer 2

Inductive用于定义在某些操作下关闭的类型；这不是您在这里寻找的。您要构建的是在n上迭代的递归函数。这可以使用Fixpoint关键字来完成：

Fixpoint pow_func {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
 match n with
  | O   => f a
  | S n => f (pow_func f n a)
end.

如果您希望这个函数有一个更好的语法，您可以引入一个Notation。

Notation "f ^ n" := (pow_func f n).

但是，请注意，这并不是权力概念的一个行为良好的定义:如果您组合了f ^ m和f ^ n，那么您将得到的不是f ^ (m + n)，而是f ^ (1 + m + n)。要解决这个问题，您应该选择大小写f ^ 0作为组合id的中性元素，而不是f本身。这会让你：

Fixpoint pow_func' {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
 match n with
  | O   => a
  | S n => f (pow_func' f n a)
end.