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
|
(** * powerfix: bounded fixpoint operator *)
(** we define a fixpoint operator which recursively unfolds an
open-recursive function with recursive depth at most [2^n], for
arbitrary [n]. This allows us to define arbitrary recursive
functions, without needing to prove their termination. The operator
is defined in a computationally efficient way. (We already used
such a trick in ATBR ; it's simplified here thanks to the
introduction of eta in Coq v8.4 *)
Require Import common.
Set Implicit Arguments.
Section powerfix.
Variables A B: Type.
Notation Fun := (A -> B).
(** the three following functions "iterate" their [f] argument lazily:
iteration stops whenever [f] no longer makes recursive calls.
- [powerfix' n f k] iterates [f] at most [(2^n-1)] times and then yields to [k]
- [powerfix n f k] iterates [f] at most [(2^n)] times and then yields to [k]
- [linearfix n f k] iterates [f] at most [n] times and then yields to [k]
*)
Fixpoint powerfix' n (f: Fun -> Fun) (k: Fun): Fun :=
fun a => match n with O => k a | S n => f (powerfix' n f (powerfix' n f k)) a end.
Definition powerfix n f k a := f (powerfix' n f k) a.
Fixpoint linearfix n (f: Fun -> Fun) (k: Fun): Fun :=
fun a => match n with O => k a | S n => f (linearfix n f k) a end.
(** simple lemmas about [2^n] *)
Lemma pow2_S n: pow2 n = S (pred (pow2 n)).
Proof. induction n. reflexivity. simpl. now rewrite IHn. Qed.
Lemma pred_pow2_Sn n: pred (pow2 (S n)) = S (double (pred (pow2 n))).
Proof. simpl. now rewrite pow2_S. Qed.
(** characterisation of [powerfix] with [linearfix] *)
Section linear_carac.
Variable f: Fun -> Fun.
Lemma linearfix_S: forall n k,
f (linearfix n f k) = linearfix n f (f k).
Proof. induction n; intros k; simpl. reflexivity. now rewrite IHn. Qed.
Lemma linearfix_double: forall n k,
linearfix n f (linearfix n f k) = linearfix (double n) f k.
Proof.
induction n; intros k. reflexivity. simpl linearfix.
now rewrite <-IHn, <-linearfix_S.
Qed.
Lemma powerfix'_linearfix: forall n k,
powerfix' n f k = linearfix (pred (pow2 n)) f k.
Proof.
induction n; intros. reflexivity.
rewrite pred_pow2_Sn. simpl.
now rewrite <-linearfix_double, 2IHn.
Qed.
Theorem powerfix_linearfix: forall n k,
powerfix n f k = linearfix (pow2 n) f k.
Proof. intros. unfold powerfix. now rewrite powerfix'_linearfix, pow2_S. Qed.
End linear_carac.
(** [powerfix_invariant] gives an induction principle for [powerfix],
that does not care about the number of iterations -- in particular,
the trivial "emptyfix" function : ([fun f k a => k a]) satisfies
the same induction principle, so that this can only be used to
reason about partial correctness. *)
Section invariant.
Variable P: Fun -> Prop.
Lemma powerfix_invariant: forall n f g,
(forall k, P k -> P (f k)) -> P g -> P (powerfix n f g).
Proof.
intros n f g Hf Hg. apply Hf.
revert g Hg. induction n; intros g Hg; simpl; auto.
Qed.
End invariant.
End powerfix.
|
