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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
Require Export NDomain.
Declare Module Export DomainModule : DomainSignature.
Open Local Scope NScope.
Parameter O : N.
Parameter S : N -> N.
Notation "0" := O.
Definition induction :=
forall P : N -> Prop, pred_wd E P ->
P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n.
Definition other_induction :=
forall P : N -> Prop,
(forall n : N, n == 0 -> P n) ->
(forall n : N, P n -> forall m : N, m == S n -> P m) ->
forall n : N, P n.
Theorem other_ind_implies_ind : other_induction -> induction.
Proof.
unfold induction, other_induction; intros OI P P_wd Base Step.
apply OI; unfold pred_wd in P_wd.
intros; now apply -> (P_wd 0).
intros n Pn m EmSn; now apply -> (P_wd (S n)); [apply Step|].
Qed.
Theorem ind_implies_other_ind : induction -> other_induction.
Proof.
intros I P Base Step.
set (Q := fun n => forall m, m == n -> P m).
cut (forall n, Q n).
unfold Q; intros H n; now apply (H n).
apply I.
unfold pred_wd, Q. intros x y Exy.
split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy].
exact Base.
intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |].
Qed.
(* This theorem is not really needed. It shows that if we have
other_induction and we proved the base case and the induction step, we
can in fact show that the predicate in question is well-defined, and
therefore we can turn this other induction into the standard one. *)
Theorem other_ind_implies_pred_wd :
other_induction ->
forall P : N -> Prop,
(forall n : N, n == 0 -> P n) ->
(forall n : N, P n -> forall m : N, m == S n -> P m) ->
pred_wd E P.
Proof.
intros OI P Base Step; unfold pred_wd.
intros x; pattern x; apply OI; clear x.
(* Base case *)
intros x H1 y H2.
assert (y == 0); [rewrite <- H2; now rewrite H1|].
assert (P x); [now apply Base|].
assert (P y); [now apply Base|].
split; now intro.
(* Step *)
intros x IH z H y H1.
rewrite H in H1. symmetry in H1.
split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI.
Qed.
Section Recursion.
Variable A : Set.
Variable EA : relation A.
Hypothesis EA_symm : symmetric A EA.
Hypothesis EA_trans : transitive A EA.
Add Relation A EA
symmetry proved by EA_symm
transitivity proved by EA_trans
as EA_rel.
Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a.
Proof.
intros a a' EAaa'.
apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption].
Qed.
Parameter recursion : A -> (N -> A -> A) -> N -> A.
Axiom recursion_0 :
forall (a : A) (f : N -> A -> A),
EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a.
Axiom recursion_S :
forall (a : A) (f : N -> A -> A),
EA a a -> fun2_wd E EA EA f ->
forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
Theorem recursion_wd : induction ->
forall a a' : A, EA a a' ->
forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
forall x x' : N, x == x' ->
EA (recursion a f x) (recursion a' f' x').
Proof.
intros I a a' Eaa' f f' f_wd f'_wd Eff'.
apply ind_implies_other_ind in I.
intro x; pattern x; apply I; clear x.
intros x Ex0 x' Exx'.
rewrite Ex0 in Exx'; symmetry in Exx'.
(* apply recursion_0 in Ex0. produces
Anomaly: type_of: this is not a well-typed term. Please report. *)
assert (EA (recursion a f x) a).
apply recursion_0. now apply EA_neighbor with (a' := a'). assumption.
assert (EA a' (recursion a' f' x')).
apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption.
apply EA_trans with (y := a). assumption.
now apply EA_trans with (y := a').
intros x IH y H y' H1.
rewrite H in H1; symmetry in H1.
assert (EA (recursion a f y) (f x (recursion a f x))).
apply recursion_S. now apply EA_neighbor with (a' := a').
assumption. now symmetry.
assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')).
symmetry; apply recursion_S. now apply EA_neighbor with (a' := a). assumption.
now symmetry.
assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))).
apply Eff'. reflexivity. apply IH. reflexivity.
apply EA_trans with (y := (f x (recursion a f x))). assumption.
apply EA_trans with (y := (f' x (recursion a' f' x))). assumption.
assumption.
Qed.
Axiom recursion_0' :
forall (a : A) (f : N -> A -> A),
forall x : N, x == 0 -> recursion a f x = a.
Axiom recursion_S' :
forall (a : A) (f : N -> A -> A),
EA a a -> fun2_wd E EA EA f ->
forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
Theorem recursion_wd' : other_induction ->
forall a a' : A, EA a a -> EA a' a' -> EA a a' ->
forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
forall x x' : N, x == x' ->
EA (recursion a f x) (recursion a' f' x').
Proof.
intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'.
intro x; pattern x; apply I; clear x.
intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'.
replace (recursion a f x) with a. replace (recursion a' f' x') with a'.
assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'.
intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'.
apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_S'.
apply EA_trans with (y := (f' x (recursion a' f' x))).
apply Eff'. reflexivity. now apply IH.
symmetry; now apply recursion_S'.
Qed.
End Recursion.
Implicit Arguments recursion [A].
|
