relations.v 20 KB
Newer Older
1
2
(** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a
Robbert Krebbers's avatar
Robbert Krebbers committed
3
small step semantics. *)
4
From stdpp Require Export sets well_founded.
Ralf Jung's avatar
Ralf Jung committed
5
From stdpp Require Import options.
6
7
8
9
10
11
12
13
14
15
16

(** * Definitions *)
Section definitions.
  Context `(R : relation A).

  (** An element is reducible if a step is possible. *)
  Definition red (x : A) :=  y, R x y.

  (** An element is in normal form if no further steps are possible. *)
  Definition nf (x : A) := ¬red x.

17
18
19
  (** The symmetric closure. *)
  Definition sc : relation A := λ x y, R x y  R y x.

20
21
22
23
24
  (** The reflexive transitive closure. *)
  Inductive rtc : relation A :=
    | rtc_refl x : rtc x x
    | rtc_l x y z : R x y  rtc y z  rtc x z.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
28
29
  (** The reflexive transitive closure for setoids. *)
  Inductive rtcS `{Equiv A} : relation A :=
    | rtcS_refl x y : x  y  rtcS x y
    | rtcS_l x y z : R x y  rtcS y z  rtcS x z.

30
31
32
33
34
  (** Reductions of exactly [n] steps. *)
  Inductive nsteps : nat  relation A :=
    | nsteps_O x : nsteps 0 x x
    | nsteps_l n x y z : R x y  nsteps n y z  nsteps (S n) x z.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
  (** Reductions of at most [n] steps. *)
36
37
38
39
40
41
42
43
44
  Inductive bsteps : nat  relation A :=
    | bsteps_refl n x : bsteps n x x
    | bsteps_l n x y z : R x y  bsteps n y z  bsteps (S n) x z.

  (** The transitive closure. *)
  Inductive tc : relation A :=
    | tc_once x y : R x y  tc x y
    | tc_l x y z : R x y  tc y z  tc x z.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
48
49
50
51
52
53
  (** An element [x] is universally looping if all paths starting at [x]
  are infinite. *)
  CoInductive all_loop : A  Prop :=
    | all_loop_do_step x : red x  ( y, R x y  all_loop y)  all_loop x.

  (** An element [x] is existentally looping if some path starting at [x]
  is infinite. *)
  CoInductive ex_loop : A  Prop :=
    | ex_loop_do_step x y : R x y  ex_loop y  ex_loop x.
54
55
End definitions.

56
57
58
(** The reflexive transitive symmetric closure. *)
Definition rtsc {A} (R : relation A) := rtc (sc R).

59
60
61
(** Weakly and strongly normalizing elements. *)
Definition wn {A} (R : relation A) (x : A) :=  y, rtc R x y  nf R y.

62
63
Notation sn R := (Acc (flip R)).

64
65
66
67
68
69
70
71
72
73
74
75
76
(** The various kinds of "confluence" properties. Any relation that has the
diamond property is confluent, and any confluent relation is locally confluent.
The naming convention are taken from "Term Rewriting and All That" by Baader and
Nipkow. *)
Definition diamond {A} (R : relation A) :=
   x y1 y2, R x y1  R x y2   z, R y1 z  R y2 z.

Definition confluent {A} (R : relation A) :=
  diamond (rtc R).

Definition locally_confluent {A} (R : relation A) :=
   x y1 y2, R x y1  R x y2   z, rtc R y1 z  rtc R y2 z.

77
Global Hint Unfold nf red : core.
78

79
(** * General theorems *)
80
Section general.
81
82
  Context `{R : relation A}.

Ralf Jung's avatar
Ralf Jung committed
83
  Local Hint Constructors rtc nsteps bsteps tc : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
84

85
  (** ** Results about the reflexive-transitive closure [rtc] *)
86
87
88
  Lemma rtc_transitive x y z : rtc R x y  rtc R y z  rtc R x z.
  Proof. induction 1; eauto. Qed.

89
90
91
92
93
94
  (* We give this instance a lower-than-usual priority because [setoid_rewrite]
     queries for [@Reflexive Prop ?r] in the hope of [iff_reflexive] getting
     picked as the instance.  [rtc_reflexive] overlaps with that, leading to
     backtracking.  We cannot set [Hint Mode] because that query must not fail,
     but we can at least avoid picking [rtc_reflexive].

95
96
97
     See Coq bug https://github.com/coq/coq/issues/7916 and the test
     [tests.typeclasses.test_setoid_rewrite]. *)
  Global Instance rtc_po : PreOrder (rtc R) | 10.
98
  Proof. split; [exact (@rtc_refl A R) | exact rtc_transitive]. Qed.
99

100
101
102
103
104
105
106
107
  (* Not an instance, related to the issue described above, this sometimes makes
  [setoid_rewrite] queries loop. *)
  Lemma rtc_equivalence : Symmetric R  Equivalence (rtc R).
  Proof.
    split; try apply _.
    intros x y. induction 1 as [|x1 x2 x3]; [done|trans x2; eauto].
  Qed.

108
  Lemma rtc_once x y : R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  Proof. eauto. Qed.
110
  Lemma rtc_r x y z : rtc R x y  R y z  rtc R x z.
111
  Proof. intros. etrans; eauto. Qed.
112
113
  Lemma rtc_inv x z : rtc R x z  x = z   y, R x y  rtc R y z.
  Proof. inversion_clear 1; eauto. Qed.
114
115
116
117
  Lemma rtc_ind_l (P : A  Prop) (z : A)
    (Prefl : P z) (Pstep :  x y, R x y  rtc R y z  P y  P x) :
     x, rtc R x z  P x.
  Proof. induction 1; eauto. Qed.
118
119
  Lemma rtc_ind_r_weak (P : A  A  Prop)
    (Prefl :  x, P x x) (Pstep :  x y z, rtc R x y  R y z  P x y  P x z) :
120
     x z, rtc R x z  P x z.
121
122
123
124
125
  Proof.
    cut ( y z, rtc R y z   x, rtc R x y  P x y  P x z).
    { eauto using rtc_refl. }
    induction 1; eauto using rtc_r.
  Qed.
126
127
128
129
130
131
  Lemma rtc_ind_r (P : A  Prop) (x : A)
    (Prefl : P x) (Pstep :  y z, rtc R x y  R y z  P y  P z) :
     z, rtc R x z  P z.
  Proof.
    intros z p. revert x z p Prefl Pstep. refine (rtc_ind_r_weak _ _ _); eauto.
  Qed.
132
  Lemma rtc_inv_r x z : rtc R x z  x = z   y, rtc R x y  R y z.
133
  Proof. revert z. apply rtc_ind_r; eauto. Qed.
134

135
  Lemma rtc_nf x y : rtc R x y  nf R x  x = y.
136
  Proof. destruct 1 as [x|x y1 y2]; [done|]. intros []; eauto. Qed.
137

138
139
140
141
  Lemma rtc_congruence {B} (f : A  B) (R' : relation B) x y :
    ( x y, R x y  R' (f x) (f y))  rtc R x y  rtc R' (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.

142
  (** ** Results about [nsteps] *)
143
  Lemma nsteps_once x y : R x y  nsteps R 1 x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  Proof. eauto. Qed.
145
146
  Lemma nsteps_once_inv x y : nsteps R 1 x y  R x y.
  Proof. inversion 1 as [|???? Hhead Htail]; inversion Htail; by subst. Qed.
147
148
  Lemma nsteps_trans n m x y z :
    nsteps R n x y  nsteps R m y z  nsteps R (n + m) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  Proof. induction 1; simpl; eauto. Qed.
150
  Lemma nsteps_r n x y z : nsteps R n x y  R y z  nsteps R (S n) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Proof. induction 1; eauto. Qed.
152

Amin Timany's avatar
Amin Timany committed
153
154
155
156
157
158
159
160
161
162
163
164
165
166
  Lemma nsteps_plus_inv n m x z :
    nsteps R (n + m) x z   y, nsteps R n x y  nsteps R m y z.
  Proof.
    revert x.
    induction n as [|n IH]; intros x Hx; simpl; [by eauto|].
    inversion Hx; naive_solver.
  Qed.

  Lemma nsteps_inv_r n x z : nsteps R (S n) x z   y, nsteps R n x y  R y z.
  Proof.
    rewrite <- PeanoNat.Nat.add_1_r.
    intros (?&?&?%nsteps_once_inv)%nsteps_plus_inv; eauto.
  Qed.

167
168
169
170
  Lemma nsteps_congruence {B} (f : A  B) (R' : relation B) n x y :
    ( x y, R x y  R' (f x) (f y))  nsteps R n x y  nsteps R' n (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.

171
  (** ** Results about [bsteps] *)
172
  Lemma bsteps_once n x y : R x y  bsteps R (S n) x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Proof. eauto. Qed.
174
175
  Lemma bsteps_plus_r n m x y :
    bsteps R n x y  bsteps R (n + m) x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  Proof. induction 1; simpl; eauto. Qed.
177
178
179
  Lemma bsteps_weaken n m x y :
    n  m  bsteps R n x y  bsteps R m x y.
  Proof.
180
    intros. replace m with (n + (m - n)) by lia; auto using bsteps_plus_r.
181
182
183
184
185
  Qed.
  Lemma bsteps_plus_l n m x y :
    bsteps R n x y  bsteps R (m + n) x y.
  Proof. apply bsteps_weaken. auto with arith. Qed.
  Lemma bsteps_S n x y :  bsteps R n x y  bsteps R (S n) x y.
186
  Proof. apply bsteps_weaken. lia. Qed.
187
188
  Lemma bsteps_trans n m x y z :
    bsteps R n x y  bsteps R m y z  bsteps R (n + m) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
190
  Lemma bsteps_r n x y z : bsteps R n x y  R y z  bsteps R (S n) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Proof. induction 1; eauto. Qed.
192
193
194
195
196
197
  Lemma bsteps_ind_r (P : nat  A  Prop) (x : A)
    (Prefl :  n, P n x)
    (Pstep :  n y z, bsteps R n x y  R y z  P n y  P (S n) z) :
     n z, bsteps R n x z  P n z.
  Proof.
    cut ( m y z, bsteps R m y z   n,
Robbert Krebbers's avatar
Robbert Krebbers committed
198
      bsteps R n x y  ( m', n  m'  m'  n + m  P m' y)  P (n + m) z).
199
    { intros help n. change n with (0 + n). eauto. }
200
201
202
    induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
    intros n p1 H. rewrite <-plus_n_Sm.
    apply (IH (S n)); [by eauto using bsteps_r |].
Robbert Krebbers's avatar
Robbert Krebbers committed
203
    intros [|m'] [??]; [lia |]. apply Pstep with x'.
204
205
206
    - apply bsteps_weaken with n; intuition lia.
    - done.
    - apply H; intuition lia.
207
  Qed.
208

209
210
211
212
  Lemma bsteps_congruence {B} (f : A  B) (R' : relation B) n x y :
    ( x y, R x y  R' (f x) (f y))  bsteps R n x y  bsteps R' n (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.

213
  (** ** Results about the transitive closure [tc] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
  Lemma tc_transitive x y z : tc R x y  tc R y z  tc R x z.
  Proof. induction 1; eauto. Qed.
216
  Global Instance tc_transitive' : Transitive (tc R).
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  Proof. exact tc_transitive. Qed.
218
  Lemma tc_r x y z : tc R x y  R y z  tc R x z.
219
  Proof. intros. etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
222
223
  Lemma tc_rtc_l x y z : rtc R x y  tc R y z  tc R x z.
  Proof. induction 1; eauto. Qed.
  Lemma tc_rtc_r x y z : tc R x y  rtc R y z  tc R x z.
  Proof. intros Hxy Hyz. revert x Hxy. induction Hyz; eauto using tc_r. Qed.
224
  Lemma tc_rtc x y : tc R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Proof. induction 1; eauto. Qed.
226

Ralf Jung's avatar
Ralf Jung committed
227
228
229
230
231
232
233
  Lemma red_tc x : red (tc R) x  red R x.
  Proof.
    split.
    - intros [y []]; eexists; eauto.
    - intros [y HR]. exists y. by apply tc_once.
  Qed.

234
235
236
237
  Lemma tc_congruence {B} (f : A  B) (R' : relation B) x y :
    ( x y, R x y  R' (f x) (f y))  tc R x y  tc R' (f x) (f y).
  Proof. induction 2; econstructor; by eauto. Qed.

238
  (** ** Results about the symmetric closure [sc] *)
239
240
241
242
243
244
245
  Global Instance sc_symmetric : Symmetric (sc R).
  Proof. unfold Symmetric, sc. naive_solver. Qed.

  Lemma sc_lr x y : R x y  sc R x y.
  Proof. by left. Qed.
  Lemma sc_rl x y : R y x  sc R x y.
  Proof. by right. Qed.
246
247
248
249
250

  Lemma sc_congruence {B} (f : A  B) (R' : relation B) x y :
    ( x y, R x y  R' (f x) (f y))  sc R x y  sc R' (f x) (f y).
  Proof. induction 2; econstructor; by eauto. Qed.

251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
  (** ** Equivalences between closure operators *)
  Lemma bsteps_nsteps n x y : bsteps R n x y   n', n'  n  nsteps R n' x y.
  Proof.
    split.
    - induction 1 as [|n x1 x2 y ?? (n'&?&?)].
      + exists 0; naive_solver eauto with lia.
      + exists (S n'); naive_solver eauto with lia.
    - intros (n'&Hn'&Hsteps). apply bsteps_weaken with n'; [done|].
      clear Hn'. induction Hsteps; eauto.
  Qed.

  Lemma tc_nsteps x y : tc R x y   n, 0 < n  nsteps R n x y.
  Proof.
    split.
    - induction 1 as [|x1 x2 y ?? (n&?&?)].
      { exists 1. eauto using nsteps_once with lia. }
      exists (S n); eauto using nsteps_l.
    - intros (n & ? & Hstep). induction Hstep as [|n x1 x2 y ? Hstep]; [lia|].
      destruct Hstep; eauto with lia.
  Qed.

  Lemma rtc_tc x y : rtc R x y  x = y  tc R x y.
  Proof.
274
275
    split; [|naive_solver eauto using tc_rtc].
    induction 1; naive_solver.
276
  Qed.
277

278
279
280
  Lemma rtc_nsteps x y : rtc R x y   n, nsteps R n x y.
  Proof.
    split.
281
282
    - induction 1; naive_solver.
    - intros [n Hsteps]. induction Hsteps; naive_solver.
283
  Qed.
284
285
286
287
288
  Lemma rtc_nsteps_1 x y : rtc R x y   n, nsteps R n x y.
  Proof. rewrite rtc_nsteps. naive_solver. Qed.
  Lemma rtc_nsteps_2 n x y : nsteps R n x y  rtc R x y.
  Proof. rewrite rtc_nsteps. naive_solver. Qed.

289
290
  Lemma rtc_bsteps x y : rtc R x y   n, bsteps R n x y.
  Proof. rewrite rtc_nsteps. setoid_rewrite bsteps_nsteps. naive_solver. Qed.
291
292
293
294
  Lemma rtc_bsteps_1 x y : rtc R x y   n, bsteps R n x y.
  Proof. rewrite rtc_bsteps. naive_solver. Qed.
  Lemma rtc_bsteps_2 n x y : bsteps R n x y  rtc R x y.
  Proof. rewrite rtc_bsteps. naive_solver. Qed.
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352

  Lemma nsteps_list n x y :
    nsteps R n x y   l,
      length l = S n 
      head l = Some x 
      last l = Some y 
       i a b, l !! i = Some a  l !! S i = Some b  R a b.
  Proof.
    setoid_rewrite head_lookup. split.
    - induction 1 as [x|n' x x' y ?? IH].
      { exists [x]; naive_solver. }
      destruct IH as (l & Hlen & Hfirst & Hlast & Hcons).
      exists (x :: l). simpl. rewrite Hlen, last_cons, Hlast.
      split_and!; [done..|]. intros [|i]; naive_solver.
    - intros ([|x' l]&?&Hfirst&Hlast&Hcons); simplify_eq/=.
      revert x Hlast Hcons.
      induction l as [|x1 l IH]; intros x2 Hlast Hcons; simplify_eq/=; [constructor|].
      econstructor; [by apply (Hcons 0)|].
      apply IH; [done|]. intros i. apply (Hcons (S i)).
  Qed.

  Lemma bsteps_list n x y :
    bsteps R n x y   l,
      length l  S n 
      head l = Some x 
      last l = Some y 
       i a b, l !! i = Some a  l !! S i = Some b  R a b.
  Proof.
    rewrite bsteps_nsteps. split.
    - intros (n'&?&(l&?&?&?&?)%nsteps_list). exists l; eauto with lia.
    - intros (l&?&?&?&?). exists (pred (length l)). split; [lia|].
      apply nsteps_list. exists l. split; [|by eauto]. by destruct l.
  Qed.

  Lemma rtc_list x y :
    rtc R x y   l,
      head l = Some x 
      last l = Some y 
       i a b, l !! i = Some a  l !! S i = Some b  R a b.
  Proof.
    rewrite rtc_bsteps. split.
    - intros (n'&(l&?&?&?&?)%bsteps_list). exists l; eauto with lia.
    - intros (l&?&?&?). exists (pred (length l)).
      apply bsteps_list. exists l. eauto with lia.
  Qed.

  Lemma tc_list x y :
    tc R x y   l,
      1 < length l 
      head l = Some x 
      last l = Some y 
       i a b, l !! i = Some a  l !! S i = Some b  R a b.
  Proof.
    rewrite tc_nsteps. split.
    - intros (n'&?&(l&?&?&?&?)%nsteps_list). exists l; eauto with lia.
    - intros (l&?&?&?&?). exists (pred (length l)).
      split; [lia|]. apply nsteps_list. exists l. eauto with lia.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
353
354
355
356
357
358

  Lemma ex_loop_inv x :
    ex_loop R x 
     x', R x x'  ex_loop R x'.
  Proof. inversion 1; eauto. Qed.

359
End general.
360

361
Section more_general.
362
363
  Context `{R : relation A}.

364
  (** ** Results about the reflexive-transitive-symmetric closure [rtsc] *)
365
366
367
368
369
370
371
372
373
374
375
  Global Instance rtsc_equivalence : Equivalence (rtsc R) | 10.
  Proof. apply rtc_equivalence, _. Qed.

  Lemma rtsc_lr x y : R x y  rtsc R x y.
  Proof. unfold rtsc. eauto using sc_lr, rtc_once. Qed.
  Lemma rtsc_rl x y : R y x  rtsc R x y.
  Proof. unfold rtsc. eauto using sc_rl, rtc_once. Qed.
  Lemma rtc_rtsc_rl x y : rtc R x y  rtsc R x y.
  Proof. induction 1; econstructor; eauto using sc_lr. Qed.
  Lemma rtc_rtsc_lr x y : rtc R y x  rtsc R x y.
  Proof. intros. symmetry. eauto using rtc_rtsc_rl. Qed.
376
377
378
379
380

  Lemma rtsc_congruence {B} (f : A  B) (R' : relation B) x y :
    ( x y, R x y  R' (f x) (f y))  rtsc R x y  rtsc R' (f x) (f y).
  Proof. unfold rtsc; eauto using rtc_congruence, sc_congruence. Qed.

Ralf Jung's avatar
Ralf Jung committed
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
  Lemma ex_loop_tc x :
    ex_loop (tc R) x  ex_loop R x.
  Proof.
    split.
    - revert x; cofix IH.
      intros x (y & Hstep & Hloop')%ex_loop_inv.
      destruct Hstep as [x y Hstep|x y z Hstep Hsteps].
      + econstructor; eauto.
      + econstructor; [by eauto|].
        eapply IH. econstructor; eauto.
    - revert x; cofix IH.
      intros x (y & Hstep & Hloop')%ex_loop_inv.
      econstructor; eauto using tc_once.
  Qed.

396
End more_general.
397
398
399
400

Section properties.
  Context `{R : relation A}.

Ralf Jung's avatar
Ralf Jung committed
401
  Local Hint Constructors rtc nsteps bsteps tc : core.
402

403
404
405
406
407
408
409
  Lemma nf_wn x : nf R x  wn R x.
  Proof. intros. exists x; eauto. Qed.
  Lemma wn_step x y : wn R y  R x y  wn R x.
  Proof. intros (z & ? & ?) ?. exists z; eauto. Qed.
  Lemma wn_step_rtc x y : wn R y  rtc R x y  wn R x.
  Proof. induction 2; eauto using wn_step. Qed.

410
411
412
413
414
415
416
  Lemma nf_sn x : nf R x  sn R x.
  Proof. intros Hnf. constructor; intros y Hxy. destruct Hnf; eauto. Qed.
  Lemma sn_step x y : sn R x  R x y  sn R y.
  Proof. induction 1; eauto. Qed.
  Lemma sn_step_rtc x y : sn R x  rtc R x y  sn R y.
  Proof. induction 2; eauto using sn_step. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
417
418
  (** An acyclic relation that can only take finitely many steps (sometimes
  called "globally finite") is strongly normalizing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
419
420
421
422
423
424
425
426
427
428
429
430
431
432
  Lemma tc_finite_sn x : Irreflexive (tc R)  pred_finite (tc R x)  sn R x.
  Proof.
    intros Hirr [xs Hfin]. remember (length xs) as n eqn:Hn.
    revert x xs Hn Hfin.
    induction (lt_wf n) as [n _ IH]; intros x xs -> Hfin.
    constructor; simpl; intros x' Hxx'.
    assert (x'  xs) as (xs1&xs2&->)%elem_of_list_split by eauto using tc_once.
    refine (IH (length xs1 + length xs2) _ _ (xs1 ++ xs2) _ _);
      [rewrite app_length; simpl; lia..|].
    intros x'' Hx'x''. feed pose proof (Hfin x'') as Hx''; [by econstructor|].
    cut (x'  x''); [set_solver|].
    intros ->. by apply (Hirr x'').
  Qed.

433
434
435
436
  (** The following theorem requires that [red R] is decidable. The intuition
  for this requirement is that [wn R] is a very "positive" statement as it
  points out a particular trace. In contrast, [sn R] just says "this also holds
  for all successors", there is no "data"/"trace" there. *)
437
438
439
440
  Lemma sn_wn `{! y, Decision (red R y)} x : sn R x  wn R x.
  Proof.
    induction 1 as [x _ IH]. destruct (decide (red R x)) as [[x' ?]|?].
    - destruct (IH x') as (y&?&?); eauto using wn_step.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
    - by apply nf_wn.
442
  Qed.
443

Robbert Krebbers's avatar
Robbert Krebbers committed
444
  Lemma all_loop_red x : all_loop R x  red R x.
445
  Proof. destruct 1; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
446
  Lemma all_loop_step x y : all_loop R x  R x y  all_loop R y.
447
  Proof. destruct 1; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
449
450
451
  Lemma all_loop_rtc x y : all_loop R x  rtc R x y  all_loop R y.
  Proof. induction 2; eauto using all_loop_step. Qed.
  Lemma all_loop_alt x :
    all_loop R x   y, rtc R x y  red R y.
452
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
454
455
    split; [eauto using all_loop_red, all_loop_rtc|].
    intros H. cut ( z, rtc R x z  all_loop R z); [eauto|].
    cofix FIX. constructor; eauto using rtc_r.
456
  Qed.
457

458
459
460
461
462
  Lemma wn_not_all_loop x : wn R x  ¬all_loop R x.
  Proof. intros (z&?&?). rewrite all_loop_alt. eauto. Qed.
  Lemma sn_not_ex_loop x : sn R x  ¬ex_loop R x.
  Proof. unfold not. induction 1; destruct 1; eauto. Qed.

463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
  (** An alternative definition of confluence; also known as the Church-Rosser
  property. *)
  Lemma confluent_alt :
    confluent R  ( x y, rtsc R x y   z, rtc R x z  rtc R y z).
  Proof.
    split.
    - intros Hcr. induction 1 as [x|x y1 y1' [Hy1|Hy1] Hy1' (z&IH1&IH2)]; eauto.
      destruct (Hcr y1 x z) as (z'&?&?); eauto using rtc_transitive.
    - intros Hcr x y1 y2 Hy1 Hy2.
      apply Hcr; trans x; eauto using rtc_rtsc_rl, rtc_rtsc_lr.
  Qed.

  Lemma confluent_nf_r x y :
    confluent R  rtsc R x y  nf R y  rtc R x y.
  Proof.
    rewrite confluent_alt. intros Hcr ??. destruct (Hcr x y) as (z&Hx&Hy); auto.
    by apply rtc_nf in Hy as ->.
  Qed.
  Lemma confluent_nf_l x y :
    confluent R  rtsc R x y  nf R x  rtc R y x.
  Proof. intros. by apply (confluent_nf_r y x). Qed.

  Lemma diamond_confluent :
    diamond R  confluent R.
  Proof.
    intros Hdiam. assert ( x y1 y2,
      rtc R x y1  R x y2   z, rtc R y1 z  rtc R y2 z) as Hstrip.
    { intros x y1 y2 Hy1; revert y2.
      induction Hy1 as [x|x y1 y1' Hy1 Hy1' IH]; [by eauto|]; intros y2 Hy2.
      destruct (Hdiam x y1 y2) as (z&Hy1z&Hy2z); auto.
      destruct (IH z) as (z'&?&?); eauto. }
    intros x y1 y2 Hy1; revert y2.
    induction Hy1 as [x|x y1 y1' Hy1 Hy1' IH]; [by eauto|]; intros y2 Hy2.
    destruct (Hstrip x y2 y1) as (z&?&?); eauto.
    destruct (IH z) as (z'&?&?); eauto using rtc_transitive.
  Qed.

  Lemma confluent_locally_confluent :
    confluent R  locally_confluent R.
  Proof. unfold confluent, locally_confluent; eauto. Qed.

  (** The following is also known as Newman's lemma *)
  Lemma locally_confluent_confluent :
    ( x, sn R x)  locally_confluent R  confluent R.
  Proof.
    intros Hsn Hcr x. induction (Hsn x) as [x _ IH].
    intros y1 y2 Hy1 Hy2. destruct Hy1 as [x|x y1 y1' Hy1 Hy1']; [by eauto|].
    destruct Hy2 as [x|x y2 y2' Hy2 Hy2']; [by eauto|].
    destruct (Hcr x y1 y2) as (z&Hy1z&Hy2z); auto.
    destruct (IH _ Hy1 y1' z) as (z1&?&?); auto.
    destruct (IH _ Hy2 y2' z1) as (z2&?&?); eauto using rtc_transitive.
  Qed.
End properties.
516
517
518

(** * Theorems on sub relations *)
Section subrel.
519
520
521
522
523
524
  Context {A} (R1 R2 : relation A).
  Notation subrel := ( x y, R1 x y  R2 x y).
  Lemma red_subrel x : subrel  red R1 x  red R2 x.
  Proof. intros ? [y ?]; eauto. Qed.
  Lemma nf_subrel x : subrel  nf R2 x  nf R1 x.
  Proof. intros ? H1 H2; destruct H1; by apply red_subrel. Qed.
Ralf Jung's avatar
Ralf Jung committed
525
526
  Lemma rtc_subrel x y : subrel  rtc R1 x y  rtc R2 x y.
  Proof. induction 2; [by apply rtc_refl|]. eapply rtc_l; eauto. Qed.
527
End subrel.