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
|
Require Import Coq.Init.Wf.
Require Import Coq.Program.Utils.
Require Import ProofIrrelevance.
Open Local Scope program_scope.
Implicit Arguments Enriching Acc_inv [y].
(** Reformulation of the Wellfounded module using subsets where possible. *)
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 (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 : 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:A|R y x) => Fix_F (`y) (Acc_inv r (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: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 m : A -> nat.
Section Acc.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y
(@Acc_inv _ _ _ r (m y) (proj2_sig y))).
Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
End Acc.
Section FixPoint.
Variable P : A -> Type.
Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
Hypothesis
F_ext :
forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
(forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
Program Lemma Fix_measure_F_eq :
forall (x:A) (r:Acc lt (m x)),
F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
Proof.
intros x.
set (y := m x).
unfold Fix_measure_F_sub.
intros r ; case r ; auto.
Qed.
Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
Proof.
intros x r s.
rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
Qed.
Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
Proof.
intro x; unfold Fix_measure in |- *.
rewrite <- (Fix_measure_F_eq ).
apply F_ext; intros.
apply Fix_measure_F_inv.
Qed.
Lemma fix_measure_sub_eq :
forall x : A,
Fix_measure_sub P F_sub x =
let f_sub := F_sub in
f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
exact Fix_measure_eq.
Qed.
End FixPoint.
End Well_founded_measure.
Extraction Inline Fix_measure_F_sub Fix_measure_sub.
|
