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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
(************************************************************************)
(* 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*)
(** This file defined the strong (course-of-value, well-founded) recursion
and proves its properties *)
Require Export NSub.
Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NSubPropMod := NSubPropFunct NAxiomsMod.
Open Local Scope NatScope.
Section StrongRecursion.
Variable A : Set.
Variable Aeq : relation A.
Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
Instance Aeq_equiv : Equivalence Aeq.
Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
recursion
(fun _ : N => a)
(fun (m : N) (p : N -> A) (k : N) => f k p)
(S n)
n.
Theorem strong_rec_wd :
Proper (Aeq ==> (Neq ==> (Neq ==>Aeq) ==> Aeq) ==> Neq ==> Aeq) strong_rec.
Proof.
intros a a' Eaa' f f' Eff' n n' Enn'.
(* First we prove that recursion (which is on type N -> A) returns
extensionally equal functions, and then we use the fact that n == n' *)
assert (H : fun_eq Neq Aeq
(recursion
(fun _ : N => a)
(fun (m : N) (p : N -> A) (k : N) => f k p)
(S n))
(recursion
(fun _ : N => a')
(fun (m : N) (p : N -> A) (k : N) => f' k p)
(S n'))).
apply recursion_wd with (Aeq := fun_eq Neq Aeq).
unfold fun_eq; now intros.
unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto.
now rewrite Enn'.
unfold strong_rec.
now apply H.
Qed.
(*Section FixPoint.
Variable a : A.
Variable f : N -> (N -> A) -> A.
Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f.
Let g (n : N) : A := strong_rec a f n.
Add Morphism g with signature Neq ==> Aeq as g_wd.
Proof.
intros n1 n2 H. unfold g. now apply strong_rec_wd.
Qed.
Theorem NtoA_eq_sym : symmetric (N -> A) (fun_eq Neq Aeq).
Proof.
apply fun_eq_sym.
exact (proj2 (proj2 NZeq_equiv)).
exact (proj2 (proj2 Aeq_equiv)).
Qed.
Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq).
Proof.
apply fun_eq_trans.
exact (proj1 NZeq_equiv).
exact (proj1 (proj2 NZeq_equiv)).
exact (proj1 (proj2 Aeq_equiv)).
Qed.
Add Relation (N -> A) (fun_eq Neq Aeq)
symmetry proved by NtoA_eq_sym
transitivity proved by NtoA_eq_trans
as NtoA_eq_rel.
Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph.
Proof.
apply f_wd.
Qed.
(* We need an assumption saying that for every n, the step function (f n h)
calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
coincide on values < n, then (f n h1) coincides with (f n h2) *)
Hypothesis step_good :
forall (n : N) (h1 h2 : N -> A),
(forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2).
(* Todo:
Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g).
Proof.
apply induction.
unfold predicate_wd, fun_wd.
intros x y H. rewrite H. unfold fun_eq; apply g_wd.
reflexivity.
unfold g, strong_rec.
*)
End FixPoint.*)
End StrongRecursion.
Implicit Arguments strong_rec [A].
End NStrongRecPropFunct.
|
