forked from uds-psl/base-library
-
Notifications
You must be signed in to change notification settings - Fork 0
/
FCI.v
158 lines (135 loc) · 4.3 KB
/
FCI.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
154
155
156
157
158
Require Import Lists.Cardinality Numbers.
(** ** Finite inductive predicates *)
Section Fip.
Variables (X: eqType) (sigma: list X -> X -> bool) (R: list X).
Inductive fip : X -> Prop :=
| fip_intro A x : (forall x, x el A -> fip x) -> sigma A x -> x el R -> fip x.
Definition fip_monotone := forall A B x, A <<= B -> sigma A x -> sigma B x.
Definition fip_closed A := forall x, x el R -> sigma A x -> x el A.
Lemma fip_least A x :
fip_monotone -> fip_closed A -> fip x -> x el A.
Proof.
intros C D. induction 1 as [B x _ IH F G].
apply (D _ G). revert F. apply C. exact IH.
Qed.
Fixpoint fip_it n A : list X :=
match n, find (fun x => Dec (~ x el A /\ sigma A x)) R with
| S n', Some x => fip_it n' (x::A)
| _, _ => A
end.
Lemma fip_it_sound n A :
inclp A fip -> inclp (fip_it n A) fip.
Proof.
revert A; induction n as [|n IH]; cbn; intros A H.
- exact H.
- destruct (find _ R) as[x|] eqn:E.
(* New: Remember equation, apply find specs to it, elim Dec _ = true *)
+ apply find_some in E as [H1 (H2&H3) % Dec_true].
apply IH. intros z [<-|H4].
* apply fip_intro with (A:= A); auto.
* apply H, H4.
+ apply H.
Qed.
Lemma fip_it_closed n A :
A <<= R -> card R <= n + card A -> fip_closed (fip_it n A).
Proof.
revert A. induction n as [|n IH]; cbn; intros A H H1.
- enough (A === R) as (H2&H3) by (hnf; auto).
apply card_or in H as [H|H]. exact H. omega.
- destruct (find _ R) eqn:E.
+ apply find_some in E as [H2 (H3&H4) % Dec_true]. apply IH. now auto.
rewrite card_cons'. omega. auto.
+ intros x H2 H3. apply dec_DN. now auto.
apply find_none with (x := x) in E; auto.
apply Dec_false in E; auto.
Qed.
Theorem fip_dec x :
fip_monotone -> dec (fip x).
Proof.
intros D.
apply dec_transfer with (P:= x el fip_it (card R) nil); [ | now auto].
split.
- revert x. apply fip_it_sound. hnf. auto.
- apply (fip_least D). apply fip_it_closed. now auto. omega.
Qed.
End Fip.
(** ** Finite closure iteration *)
Module FCI.
Section FCI.
Variables (X: eqType) (sigma: list X -> X -> bool) (R: list X).
Lemma pick (A : list X) :
{ x | x el R /\ sigma A x /\ ~ x el A } + { forall x, x el R -> sigma A x -> x el A }.
Proof.
destruct (cfind R (fun x => sigma A x /\ ~ x el A)) as [E|E].
- auto.
- right. intros x F G.
decide (x el A). assumption. exfalso.
eapply E; eauto.
Qed.
Definition F (A : list X) : list X.
destruct (pick A) as [[x _]|_].
- exact (x::A).
- exact A.
Defined.
Definition C := it F (card R) nil.
Lemma it_incl n :
it F n nil <<= R.
Proof.
apply it_ind. now auto.
intros A E. unfold F.
destruct (pick A) as [[x G]|G]; intuition.
Qed.
Lemma incl :
C <<= R.
Proof.
apply it_incl.
Qed.
Lemma ind p :
(forall A x, inclp A p -> x el R -> sigma A x -> p x) -> inclp C p.
Proof.
intros B. unfold C. apply it_ind.
+ intros x [].
+ intros D G x. unfold F.
destruct (pick D) as [[y E]|E].
* intros [[]|]; intuition; eauto.
* intuition.
Qed.
Lemma fp :
F C = C.
Proof.
pose (size (A : list X) := card R - card A).
replace C with (it F (size nil) nil).
- apply it_fp. intros n. cbn.
set (J:= it F n nil). unfold FP, F.
destruct (pick J) as [[x B]|B].
+ right.
assert (G: card J < card (x :: J)).
{ apply card_lt with (x:=x); intuition. }
assert (H: card (x :: J) <= card R).
{ apply card_le, incl_cons. apply B. apply it_incl. }
unfold size. omega.
+ auto.
- unfold C, size. f_equal. change (card nil) with 0. omega.
Qed.
Lemma closure x :
x el R -> sigma C x -> x el C.
Proof.
assert (A2:= fp).
unfold F in A2.
destruct (pick C) as [[y C]| B].
+ contradiction (list_cycle A2).
+ apply B.
Qed.
Theorem fip_dec x : (* Proof using FCI *)
fip_monotone sigma -> dec (fip sigma R x).
Proof.
intros D.
apply dec_transfer with (P:= x el C). Focus 2. now auto.
split.
- revert x. apply FCI.ind. intros A x IH E F.
apply fip_intro with (A:=A); auto.
- apply (fip_least D). intros z. apply FCI.closure.
Qed.
End FCI.
End FCI.
(* Print Graph. (* prints transitive closure of coercions *) *)