blob: 42016ab10b4e5035d9892fb6bfdcf162a24a0c2c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Export NZAxioms.
Set Implicit Arguments.
Module Type NAxioms (Import NZ : NZDomainSig').
Axiom pred_0 : P 0 == 0.
Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
Implicit Arguments recursion [A].
Declare Instance recursion_wd (A : Type) (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
Axiom recursion_0 :
forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a.
Axiom recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A),
Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
End NAxioms.
Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms.
Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms.
|
