blob: 6a34d0f7b69f2ae8479b2c2cadb4743b9670a3e2 (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(************************************************************************)
(* 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 NAxiomsSig.
Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
Delimit Scope NatScope with Nat.
Notation N := NZ.
Notation Neq := NZeq.
Notation N0 := NZ0.
Notation N1 := (NZsucc NZ0).
Notation S := NZsucc.
Notation P := NZpred.
Notation add := NZadd.
Notation mul := NZmul.
Notation sub := NZsub.
Notation lt := NZlt.
Notation le := NZle.
Notation min := NZmin.
Notation max := NZmax.
Notation "x == y" := (Neq x y) (at level 70) : NatScope.
Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope.
Notation "0" := NZ0 : NatScope.
Notation "1" := (NZsucc NZ0) : NatScope.
Notation "x + y" := (NZadd x y) : NatScope.
Notation "x - y" := (NZsub x y) : NatScope.
Notation "x * y" := (NZmul x y) : NatScope.
Notation "x < y" := (NZlt x y) : NatScope.
Notation "x <= y" := (NZle x y) : NatScope.
Notation "x > y" := (NZlt y x) (only parsing) : NatScope.
Notation "x >= y" := (NZle y x) (only parsing) : NatScope.
Open Local Scope NatScope.
Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> A.
Implicit Arguments recursion [A].
Axiom pred_0 : P 0 == 0.
Instance recursion_wd (A : Type) (Aeq : relation A) :
Proper (Aeq ==> (Neq==>Aeq==>Aeq) ==> Neq ==> Aeq) (@recursion A).
Axiom recursion_0 :
forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a.
Axiom recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
Aeq a a -> Proper (Neq==>Aeq==>Aeq) f ->
forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
(*Axiom dep_rec :
forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*)
End NAxiomsSig.
|
