-
Notifications
You must be signed in to change notification settings - Fork 1
/
fillia_orig.v
153 lines (123 loc) · 4.57 KB
/
fillia_orig.v
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
(* author: Jean-Christophe Filli�tre *)
(**
Correctness proof of Floyd's cycle-finding algorithm, also known as
the "tortoise and the hare"-algorithm
(see http://en.wikipedia.org/wiki/Floyd's_cycle-finding_algorithm)
If $f:A\rightarrow A$ is a function over a finite set $A$,
then the iterations of $f$ from $x_0\in A$ will ultimately cycle.
The following code finds out an integer $m$ such that
$f^m(x_0)=f^{2m}(x_0)$ :
<<
let rec race m x y = if x = y then m else race (m+1) (f x) (f (f y))
in race 1 (f x0) (f (f x0))
>>
The difficulty is to prove $f$'s termination.
*)
Require Export Arith.
Require Export Omega.
Open Scope nat_scope.
(** Let [f] be a function over a set [A] *)
Parameter A : Set.
Parameter eq_A_dec : forall (x y:A), {x=y}+{~x=y}.
Parameter f : A -> A.
Parameter x0 : A.
(** We consider the sequence $x_i = f^i(x_0)$ *)
Fixpoint x (i:nat) { struct i } : A := match i with
| O => x0
| S j => f (x j)
end.
(** We assume this sequence cycles after [lambda+mu] iterations, [mu]
being the length of the cycle (we actually don't require [lambda] and
[mu] to be minimal, because it is not needed for the remaining of the
proof *)
Parameter lambda : nat.
Parameter mu : nat.
Axiom mu_positive : mu > 0.
Axiom lambda_mu : forall i j, x (lambda+i) = x (lambda+i+j*mu).
(** Hilbert's epsilon operator. *)
Parameter epsilon : (nat -> Prop) -> nat.
Axiom epsilon_spec : forall P, ex P -> P (epsilon P).
(** The distance between [x (2m)] and [x m] defined using [epsilon] *)
Definition sep_x2m_xm m i := x (2*m+i) = x m.
Definition min P i := P i /\ forall j, P j -> i <= j.
Definition dist_x2m_xm m := epsilon (min (sep_x2m_xm m)).
(** Existence of this distance whenever [lambda <= m] *)
Axiom ex_min_P : forall P, (forall x, {P x}+{~(P x)}) -> ex P -> ex (min P).
Axiom div : forall a, a > 0 -> forall b, exists k, k*a >= b.
Lemma ex_dist_x2m_xm : forall m, lambda <= m -> ex (min (sep_x2m_xm m)).
Proof.
intros m hm; apply ex_min_P.
intro i; unfold sep_x2m_xm.
case (eq_A_dec (x (2 * m + i)) (x m)); auto.
generalize (div mu mu_positive m); intros (k,hk).
exists (k*mu - m); unfold sep_x2m_xm.
replace (2 * m + (k * mu - m)) with (lambda + (m-lambda)+k*mu) by omega.
rewrite <- lambda_mu.
replace (lambda+(m-lambda)) with m by omega; auto.
Qed.
(** Variant to prove the termination of Floyd's algorithm:
- either [x m] has not entered the loop yet and [lambda-m] is decreasing
- or bot [x m] and [x (2m)] are inside the loop and the distance between
[x (2m)] and [x m] is decreasing
Thus we use a lexicographic order. *)
Definition variant m := (lambda - m, dist_x2m_xm m).
Definition lex x y := fst x < fst y \/ (fst x = fst y /\ snd x < snd y).
(** Correctness proof *)
Theorem rec_call_is_wf :
forall m, x m <> x (2*m) -> lex (variant (S m)) (variant m).
Proof.
unfold lex,variant; simpl.
intros.
assert (h: m < lambda \/ m >= lambda) by omega.
destruct h.
left; omega.
right.
split; auto with *.
unfold dist_x2m_xm.
assert (exd1: ex (min (sep_x2m_xm (S m)))).
apply ex_dist_x2m_xm; auto with *.
generalize (epsilon_spec (min (sep_x2m_xm (S m))) exd1).
assert (exd0: ex (min (sep_x2m_xm m))).
apply ex_dist_x2m_xm; auto with *.
generalize (epsilon_spec (min (sep_x2m_xm m)) exd0).
generalize (epsilon (min (sep_x2m_xm m))).
generalize (epsilon (min (sep_x2m_xm (S m)))).
intros d1 d0.
unfold min,sep_x2m_xm.
intros (h1,h2) (h3,h4).
assert (x (S(2*m+d0)) = x (S m)).
simpl; simpl in h1; congruence.
assert (d0 > 0).
assert (h: d0=0 \/ d0>0) by omega. destruct h; auto.
subst d0; absurd (x (2*m)=x m); auto.
replace (2*m+0) with (2*m) in h1; auto.
assert (d1 <= d0-1).
apply h4.
replace (2 * (S m) + (d0 - 1)) with (S (2 * m + d0)) by omega.
auto.
omega.
Qed.
Definition R x y := lex (variant x) (variant y).
Axiom R_wf : well_founded R.
Definition find_cycle_rec :
forall (m:nat) (xm x2m:A), m > 0 -> xm=x m -> x2m=x (2*m) ->
{ m:nat | m > 0 /\ x m = x (2*m) }.
Proof.
induction m using (well_founded_induction R_wf).
intros xm x2m h hm h2m.
destruct (eq_A_dec xm x2m).
exists m; subst xm x2m; auto.
apply (H (S m)) with (f xm) (f (f x2m)); subst xm x2m; auto with *.
unfold R; apply rec_call_is_wf; auto.
replace (2*(S m)) with (S (S (2*m))) by omega; auto.
Defined.
Definition find_cycle : { m:nat | m > 0 /\ x m = x (2*m) }.
Proof.
apply (find_cycle_rec (S O) (f x0) (f (f x0))); auto with *.
Defined.
(** This lines were added by DLW to display the pre-conditions of find_cycle *)
Check find_cycle.
Print Assumptions find_cycle.
(*
Recursive Extraction find_cycle.
*)