The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

The iterator you describe is a particular case of the nat recursor

Print nat_rect

Section iter.

  Variables (X : Type) (f : X -> X) (a : X).

  Definition iter n := nat_rect _ a (fun _ => f) n.

  Fact iter_eq_0 : iter 0 = a.                 Proof. reflexivity. Qed.
  Fact iter_eq_S n : iter (S n) = f (iter n).  Proof. reflexivity. Qed.

End iter.

Best,

D.

---

De: "Cao Qinxiang" <caoqinxiang AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Mardi 27 Février 2018 00:04:26
Objet: [Coq-Club] Power function in Coq standard library?

Is power function like the following one defined in Coq standard library?

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.

I could only find power for natural numbers, Z and ring theory.

Thanks,

Qinxiang