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
|
Require Import Wf.
Require Import Coq.subtac.Utils.
Section Well_founded.
Variable A : Type.
Variable R : A -> A -> Prop.
Hypothesis Rwf : well_founded R.
Section Acc.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y)
(Acc_inv r (proj1_sig y) (proj2_sig y))).
Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
End Acc.
Section FixPoint.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *)
Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x).
Hypothesis
F_ext :
forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
(forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
Lemma Fix_F_eq :
forall (x:A) (r:Acc R x),
F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
Proof.
destruct r using Acc_inv_dep; auto.
Qed.
Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
Proof.
intro x; induction (Rwf x); intros.
rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros.
apply F_ext; auto.
intros.
rewrite (proof_irrelevance (Acc R x) r s) ; auto.
Qed.
Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
Proof.
intro x; unfold Fix in |- *.
rewrite <- (Fix_F_eq ).
apply F_ext; intros.
apply Fix_F_inv.
Qed.
Lemma fix_sub_eq :
forall x : A,
Fix_sub P F_sub x =
let f_sub := F_sub in
f_sub x (fun {y : A | R y x}=> Fix (`y)).
exact Fix_eq.
Qed.
End FixPoint.
End Well_founded.
Extraction Inline Fix_F_sub Fix_sub.
Require Import Wf_nat.
Require Import Lt.
Section Well_founded_measure.
Variable A : Type.
Variable f : A -> nat.
Definition R := fun x y => f x < f y.
Section FixPoint.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
F_sub x (fun y: { y : A | f y < f x} => Fix_measure_F_sub (proj1_sig y)
(Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
End FixPoint.
End Well_founded_measure.
Extraction Inline Fix_measure_F_sub Fix_measure_sub.
|
