relations.v 17.2 KB
 Robbert Krebbers committed Aug 29, 2012 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 committed Feb 10, 2019 3 ``````small step semantics. *) `````` Robbert Krebbers committed Feb 13, 2016 4 ``````From Coq Require Import Wf_nat. `````` Robbert Krebbers committed Jul 21, 2020 5 ``````From stdpp Require Export sets. `````` Ralf Jung committed Jan 31, 2017 6 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Aug 29, 2012 7 8 9 10 11 12 13 14 15 16 17 `````` (** * 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. `````` Robbert Krebbers committed Feb 10, 2019 18 19 20 `````` (** The symmetric closure. *) Definition sc : relation A := λ x y, R x y ∨ R y x. `````` Robbert Krebbers committed Aug 29, 2012 21 22 23 24 25 `````` (** 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 committed Feb 03, 2017 26 27 28 29 30 `````` (** 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. `````` Robbert Krebbers committed Aug 29, 2012 31 32 33 34 35 `````` (** 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 committed Jan 29, 2019 36 `````` (** Reductions of at most [n] steps. *) `````` Robbert Krebbers committed Aug 29, 2012 37 38 39 40 41 42 43 44 45 `````` 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 committed Sep 06, 2014 46 47 48 49 50 51 52 53 54 `````` (** 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. `````` Robbert Krebbers committed Aug 29, 2012 55 56 ``````End definitions. `````` Robbert Krebbers committed Feb 10, 2019 57 58 59 ``````(** The reflexive transitive symmetric closure. *) Definition rtsc {A} (R : relation A) := rtc (sc R). `````` 60 61 62 ``````(** Weakly and strongly normalizing elements. *) Definition wn {A} (R : relation A) (x : A) := ∃ y, rtc R x y ∧ nf R y. `````` Robbert Krebbers committed Jan 12, 2018 63 64 ``````Notation sn R := (Acc (flip R)). `````` Robbert Krebbers committed Feb 10, 2019 65 66 67 68 69 70 71 72 73 74 75 76 77 ``````(** 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. `````` Tej Chajed committed Nov 28, 2018 78 ``````Hint Unfold nf red : core. `````` Robbert Krebbers committed Oct 09, 2014 79 `````` `````` Robbert Krebbers committed Aug 29, 2012 80 ``````(** * General theorems *) `````` Robbert Krebbers committed Feb 10, 2019 81 ``````Section closure. `````` Robbert Krebbers committed Aug 29, 2012 82 83 `````` Context `{R : relation A}. `````` Tej Chajed committed Nov 28, 2018 84 `````` Hint Constructors rtc nsteps bsteps tc : core. `````` Robbert Krebbers committed Sep 06, 2014 85 `````` `````` Robbert Krebbers committed Jan 29, 2019 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. `````` Ralf Jung committed Jun 25, 2018 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]. `````` Robbert Krebbers committed Jan 29, 2019 95 96 97 98 99 `````` 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. Proof. split. exact (@rtc_refl A R). exact rtc_transitive. Qed. `````` Robbert Krebbers committed Feb 10, 2019 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. `````` Robbert Krebbers committed Aug 29, 2012 108 `````` Lemma rtc_once x y : R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 109 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 110 `````` Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z. `````` Ralf Jung committed Feb 20, 2016 111 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 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. `````` Robbert Krebbers committed Oct 02, 2014 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. `````` Robbert Krebbers committed Sep 06, 2014 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) : `````` Robbert Krebbers committed Jan 09, 2013 120 `````` ∀ x z, rtc R x z → P x z. `````` Robbert Krebbers committed Aug 29, 2012 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. `````` Robbert Krebbers committed Sep 06, 2014 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. `````` Robbert Krebbers committed Aug 29, 2012 132 `````` Lemma rtc_inv_r x z : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z. `````` Robbert Krebbers committed Sep 06, 2014 133 `````` Proof. revert z. apply rtc_ind_r; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 134 `````` `````` Robbert Krebbers committed Feb 10, 2019 135 136 137 `````` Lemma rtc_nf x y : rtc R x y → nf R x → x = y. Proof. destruct 1 as [x|x y1 y2]. done. intros []; eauto. Qed. `````` Amin Timany committed Nov 01, 2019 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. `````` Robbert Krebbers committed Aug 29, 2012 142 `````` Lemma nsteps_once x y : R x y → nsteps R 1 x y. `````` Robbert Krebbers committed Sep 06, 2014 143 `````` Proof. eauto. Qed. `````` Paolo G. Giarrusso committed Aug 23, 2019 144 145 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 146 147 `````` 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 committed Sep 06, 2014 148 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 149 `````` Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z. `````` Robbert Krebbers committed Sep 06, 2014 150 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 151 `````` Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 152 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 153 `````` Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 154 `````` Proof. induction 1; firstorder eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 155 `````` `````` Amin Timany committed Nov 01, 2019 156 157 158 159 160 161 162 163 164 165 166 167 168 169 `````` 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. `````` Amin Timany committed Nov 01, 2019 170 171 172 173 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 174 `````` Lemma bsteps_once n x y : R x y → bsteps R (S n) x y. `````` Robbert Krebbers committed Sep 06, 2014 175 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 176 177 `````` Lemma bsteps_plus_r n m x y : bsteps R n x y → bsteps R (n + m) x y. `````` Robbert Krebbers committed Sep 06, 2014 178 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 179 180 181 182 183 184 185 186 187 `````` Lemma bsteps_weaken n m x y : n ≤ m → bsteps R n x y → bsteps R m x y. Proof. intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r. 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. `````` Robbert Krebbers committed Jan 09, 2013 188 `````` Proof. apply bsteps_weaken. lia. Qed. `````` Robbert Krebbers committed Aug 29, 2012 189 190 `````` 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 committed Sep 06, 2014 191 `````` Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed. `````` Robbert Krebbers committed Aug 29, 2012 192 `````` Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z. `````` Robbert Krebbers committed Sep 06, 2014 193 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 194 `````` Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 195 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 196 `````` Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 197 `````` Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 198 199 200 201 202 203 `````` 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 committed Sep 06, 2014 204 205 `````` bsteps R n x y → (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y) → P (n + m) z). { intros help ?. change n with (0 + n). eauto. } `````` Robbert Krebbers committed Jan 09, 2013 206 207 208 `````` 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 committed Sep 06, 2014 209 `````` intros [|m'] [??]; [lia |]. apply Pstep with x'. `````` Robbert Krebbers committed Feb 17, 2016 210 211 212 `````` - apply bsteps_weaken with n; intuition lia. - done. - apply H; intuition lia. `````` Robbert Krebbers committed Jan 09, 2013 213 `````` Qed. `````` Robbert Krebbers committed Aug 29, 2012 214 `````` `````` Amin Timany committed Nov 01, 2019 215 216 217 218 `````` 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. `````` Robbert Krebbers committed Sep 06, 2014 219 220 `````` Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z. Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Jan 29, 2019 221 `````` Global Instance tc_transitive' : Transitive (tc R). `````` Robbert Krebbers committed Sep 06, 2014 222 `````` Proof. exact tc_transitive. Qed. `````` Robbert Krebbers committed Aug 29, 2012 223 `````` Lemma tc_r x y z : tc R x y → R y z → tc R x z. `````` Ralf Jung committed Feb 20, 2016 224 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 225 226 227 228 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 229 `````` Lemma tc_rtc x y : tc R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 230 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 231 `````` `````` Amin Timany committed Nov 01, 2019 232 233 234 235 `````` 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. `````` Robbert Krebbers committed Feb 10, 2019 236 237 238 239 240 241 242 `````` 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. `````` Amin Timany committed Nov 01, 2019 243 244 245 246 247 `````` 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. `````` Robbert Krebbers committed Feb 10, 2019 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 ``````End closure. Section more_closure. Context `{R : relation A}. 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. `````` Amin Timany committed Nov 01, 2019 264 265 266 267 268 `````` 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. `````` Robbert Krebbers committed Feb 10, 2019 269 270 271 272 273 274 275 ``````End more_closure. Section properties. Context `{R : relation A}. Hint Constructors rtc nsteps bsteps tc : core. `````` 276 277 278 279 280 281 282 `````` 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. `````` Robbert Krebbers committed Jul 21, 2020 283 284 `````` (** An acyclic relation that can only take finitely many steps (sometimes called "globally finite") is strongly normalizing *) `````` Robbert Krebbers committed Jul 21, 2020 285 286 287 288 289 290 291 292 293 294 295 296 297 298 `````` 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. `````` Robbert Krebbers committed Apr 07, 2020 299 300 301 302 `````` (** 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. *) `````` 303 304 305 306 `````` 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 committed Apr 07, 2020 307 `````` - by apply nf_wn. `````` 308 `````` Qed. `````` Robbert Krebbers committed Nov 30, 2018 309 `````` `````` Robbert Krebbers committed Sep 06, 2014 310 `````` Lemma all_loop_red x : all_loop R x → red R x. `````` Robbert Krebbers committed Aug 29, 2012 311 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 312 `````` Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y. `````` Robbert Krebbers committed Aug 29, 2012 313 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 314 315 316 317 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 318 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2014 319 320 321 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 322 `````` Qed. `````` Robbert Krebbers committed Feb 10, 2019 323 `````` `````` 324 325 326 327 328 `````` 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. `````` Robbert Krebbers committed Feb 10, 2019 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 `````` (** 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. `````` Robbert Krebbers committed Aug 29, 2012 382 383 384 `````` (** * Theorems on sub relations *) Section subrel. `````` Robbert Krebbers committed Apr 22, 2015 385 386 387 388 389 390 `````` 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 committed Mar 14, 2017 391 392 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 393 ``````End subrel. `````` Robbert Krebbers committed Jan 09, 2013 394 `````` `````` Robbert Krebbers committed Apr 22, 2015 395 ``````(** * Theorems on well founded relations *) `````` Robbert Krebbers committed Mar 01, 2019 396 397 398 399 ``````Lemma Acc_impl {A} (R1 R2 : relation A) x : Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x. Proof. induction 1; constructor; naive_solver. Qed. `````` Robbert Krebbers committed Jan 09, 2013 400 ``````Notation wf := well_founded. `````` Robbert Krebbers committed Nov 09, 2017 401 402 ``````Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R := Acc_intro_generator n wfR. `````` Robbert Krebbers committed Jan 09, 2013 403 404 405 406 407 408 `````` (* Generally we do not want [wf_guard] to be expanded (neither by tactics, nor by conversion tests in the kernel), but in some cases we do need it for computation (that is, we cannot make it opaque). We use the [Strategy] command to make its expanding behavior less eager. *) Strategy 100 [wf_guard]. `````` Robbert Krebbers committed Nov 17, 2016 409 `````` `````` Robbert Krebbers committed Nov 09, 2017 410 411 412 413 414 415 416 417 418 419 420 ``````Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) : (∀ x y, R1 x y → R2 (f x) (f y)) → wf R2 → wf R1. Proof. intros Hf Hwf. cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x). { intros aux x. apply (aux (f x)); auto. } induction 1 as [y _ IH]. intros x ?. subst. constructor. intros. apply (IH (f y)); auto. Qed. `````` Robbert Krebbers committed Nov 17, 2016 421 ``````Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)) `````` Robbert Krebbers committed Nov 17, 2016 422 423 424 425 426 `````` (F : ∀ x, (∀ y, R y x → B y) → B x) (HF : ∀ (x : A) (f g : ∀ y, R y x → B y), (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g)) (x : A) (acc1 acc2 : Acc R x) : E _ (Fix_F B F acc1) (Fix_F B F acc2). `````` Robbert Krebbers committed Apr 27, 2018 427 ``````Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed. `````` Johannes Kloos committed Nov 01, 2017 428 `````` `````` Robbert Krebbers committed Jan 29, 2019 429 430 431 432 433 ``````Lemma Fix_unfold_rel `{R : relation A} (wfR : wf R) (B : A → Type) (E : ∀ x, relation (B x)) (F: ∀ x, (∀ y, R y x → B y) → B x) (HF: ∀ (x: A) (f g: ∀ y, R y x → B y), (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g)) (x: A) : `````` Johannes Kloos committed Nov 01, 2017 434 435 436 `````` E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)). Proof. unfold Fix. `````` Robbert Krebbers committed Jan 29, 2019 437 `````` destruct (wfR x); simpl. `````` Johannes Kloos committed Nov 01, 2017 438 439 440 `````` apply HF; intros. apply Fix_F_proper; auto. Qed.``````