blob: a97dca9a54ae9c86b00295bd6874fe7170e6a264 (
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
|
Require Import NAxioms.
Module StrongRecProperties (Export NatModule : NatSignature).
Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule.
Section StrongRecursion.
Variable A : Set.
Variable EA : relation A.
Hypothesis EA_equiv : equiv A EA.
Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A :=
(recursion (fun _ : N => a)
(fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
(S x)) x.
Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A,
fun2_wd E (eq_fun E EA) EA f ->
fun2_wd E (eq_fun E EA) (eq_fun E EA)
(fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)).
Proof.
unfold fun2_wd; intros f f_wd.
intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'.
assert (H : e y x = e y' x'). now apply e_wd. rewrite H.
destruct (e y' x'); simpl.
now apply f_wd. now apply Egg'.
Qed.
Theorem strong_rec_wd :
forall a a', EA a a' ->
forall f f', eq_fun2 E (eq_fun E EA) EA f f' ->
forall x x', x == x' ->
EA (strong_rec a f x) (strong_rec a' f' x').
Proof.
intros a a' Eaa' f f' Eff' x x' Exx'.
assert (H : eq_fun E EA
(recursion (fun _ : N => a)
(fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
(S x))
(recursion (fun _ : N => a')
(fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y))
(S x'))).
apply recursion_wd with (EA := eq_fun E EA).
unfold eq_fun; now intros.
unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'.
assert (H: e z y = e z' y'); [now apply e_wd|].
rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp'].
now rewrite Exx'.
unfold strong_rec.
now apply H.
Qed.
(* To do:
Definition step_good (g : N -> (N -> A) -> A) :=
forall (x : N) (h1 h2 : N -> A),
(forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2).
Theorem strong_recursion_fixpoint : forall a g, step_good g ->
let f x := (strong_rec a g x) in forall x, EA (f x) (g x f).
*)
End StrongRecursion.
Implicit Arguments strong_rec [A].
End StrongRecProperties.
|
