blob: 9bfb7e6e1c2fb2faeae9c1de261ace2549c27875 (
plain) (
blame)
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
|
From stdpp Require Import relations.
Definition deterministic {A} (R : relation A) :=
∀ x y1 y2, R x y1 → R x y2 → y1 = y2.
(* As in Baader and Nipkow (1998): *)
(* y is a normal form of x if x -->* y and y is in normal form. *)
Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y.
(** The reflexive closure. *)
Inductive rc {A} (R : relation A) : relation A :=
| rc_refl x : rc R x x
| rc_once x y : R x y → rc R x y.
Hint Constructors rc : core.
(* Baader and Nipkow, Definition 2.7.3. *)
Definition strongly_confluent {A} (R : relation A) :=
∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z.
(* Baader and Nipkow, Definition 2.1.4. *)
Definition semi_confluent {A} (R : relation A) :=
∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z.
(* Lemma 2.7.4 from Baader and Nipkow *)
Lemma strong__semi_confluence {A} (R : relation A) :
strongly_confluent R → semi_confluent R.
Proof.
intros Hstrc.
unfold strongly_confluent in Hstrc.
unfold semi_confluent.
intros x1 y1 xn Hxy1 [steps Hsteps] % rtc_nsteps.
revert x1 y1 xn Hxy1 Hsteps.
induction steps; intros x1 y1 xn Hxy1 Hsteps.
- inv Hsteps. exists y1.
split.
+ apply rtc_refl.
+ by apply rtc_once.
- inv Hsteps as [|? ? x2 ? Hx1x2 Hsteps'].
destruct (Hstrc x1 y1 x2 Hxy1 Hx1x2) as [y2 [Hy21 Hy22]].
inv Hy22.
+ exists xn. split; [|done].
apply rtc_transitive with (y := y2); [done|].
rewrite rtc_nsteps. by exists steps.
+ destruct (IHsteps x2 y2 xn H Hsteps') as [yn [Hy2yn Hxnyn]].
exists yn. split; [|done].
by apply rtc_transitive with (y := y2).
Qed.
(* Copied from stdpp, originates from Baader and Nipkow (1998) *)
Definition cr {A} (R : relation A) :=
∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z.
(* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *)
Lemma semi_confluence__cr {A} (R : relation A) :
semi_confluent R → cr R.
Proof.
intros Hsc.
unfold semi_confluent in Hsc.
unfold cr.
intros x y [steps Hsteps] % rtc_nsteps.
revert x y Hsteps.
induction steps; intros x y Hsteps.
- inv Hsteps. by exists y.
- inv Hsteps. rename x into y', y into x, y0 into y.
apply IHsteps in H1 as H1'. destruct H1' as [z [Hz1 Hz2]].
destruct H0.
+ exists z. split; [|done].
by apply rtc_l with (y := y).
+ destruct (Hsc y y' z H Hz1) as [z' [Hz'1 Hz'2]].
exists z'. split; [done|].
by apply rtc_transitive with (y := z).
Qed.
|
