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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** * This module proves the validity of
- well-founded recursion (also known as course of values)
- well-founded induction
from a well-founded ordering on a given set *)
Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
Require Import Datatypes.
(** Well-founded induction principle on [Prop] *)
Section Well_founded.
Variable A : Type.
Variable R : A -> A -> Prop.
(** The accessibility predicate is defined to be non-informative *)
(** (Acc_rect is automatically defined because Acc is a singleton type) *)
Inductive Acc (x: A) : Prop :=
Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
destruct 1; trivial.
Defined.
Global Implicit Arguments Acc_inv [x y] [x].
(** A relation is well-founded if every element is accessible *)
Definition well_founded := forall a:A, Acc a.
(** Well-founded induction on [Set] and [Prop] *)
Hypothesis Rwf : well_founded.
Theorem well_founded_induction_type :
forall P:A -> Type,
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Proof.
intros; apply Acc_rect; auto.
Defined.
Theorem well_founded_induction :
forall P:A -> Set,
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact (fun P:A -> Set => well_founded_induction_type P).
Defined.
Theorem well_founded_ind :
forall P:A -> Prop,
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact (fun P:A -> Prop => well_founded_induction_type P).
Defined.
(** Well-founded fixpoints *)
Section FixPoint.
Variable P : A -> Type.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
Fixpoint Fix_F (x:A) (a:Acc x) : P x :=
F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
Scheme Acc_inv_dep := Induction for Acc Sort Prop.
Lemma Fix_F_eq :
forall (x:A) (r:Acc x),
F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
Proof.
destruct r using Acc_inv_dep; auto.
Qed.
Definition Fix (x:A) := Fix_F (Rwf x).
(** Proof that [well_founded_induction] satisfies the fixpoint equation.
It requires an extra property of the functional *)
Hypothesis
F_ext :
forall (x:A) (f g:forall y:A, R y x -> P y),
(forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
Proof.
intro x; induction (Rwf x); intros.
rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
apply F_ext; auto.
Qed.
Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
Proof.
intro x; unfold Fix.
rewrite <- Fix_F_eq.
apply F_ext; intros.
apply Fix_F_inv.
Qed.
End FixPoint.
End Well_founded.
(** Well-founded fixpoints over pairs *)
Section Well_founded_2.
Variables A B : Type.
Variable R : A * B -> A * B -> Prop.
Variable P : A -> B -> Type.
Section FixPoint_2.
Variable
F :
forall (x:A) (x':B),
(forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) : P x x' :=
F
(fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
End FixPoint_2.
Hypothesis Rwf : well_founded R.
Theorem well_founded_induction_type_2 :
(forall (x:A) (x':B),
(forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
forall (a:A) (b:B), P a b.
Proof.
intros; apply Fix_F_2; auto.
Defined.
End Well_founded_2.
Notation Acc_iter := Fix_F (only parsing). (* compatibility *)
Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *)
|
