relations.v 9.74 KB
 Robbert Krebbers committed Mar 15, 2017 1 ``````(* Copyright (c) 2012-2017, Coq-std++ developers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 3 4 5 6 ``````(* This file is distributed under the terms of the BSD license. *) (** This file collects definitions and theorems on abstract rewriting systems. These are particularly useful as we define the operational semantics as a small step semantics. This file defines a hint database [ars] containing some theorems on abstract rewriting systems. *) `````` Robbert Krebbers committed Feb 13, 2016 7 8 ``````From Coq Require Import Wf_nat. From stdpp Require Export tactics base. `````` Ralf Jung committed Jan 31, 2017 9 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Aug 29, 2012 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 `````` (** * 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. (** 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 36 37 38 39 40 41 42 43 44 45 `````` (** 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. (** Reduction of at most [n] steps. *) 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 Jan 12, 2018 57 58 59 ``````(* Strongly normalizing elements *) Notation sn R := (Acc (flip R)). `````` Robbert Krebbers committed Oct 09, 2014 60 61 ``````Hint Unfold nf red. `````` Robbert Krebbers committed Aug 29, 2012 62 63 64 65 ``````(** * General theorems *) Section rtc. Context `{R : relation A}. `````` Robbert Krebbers committed Sep 06, 2014 66 67 `````` Hint Constructors rtc nsteps bsteps tc. `````` Ralf Jung committed Jun 25, 2018 68 69 70 71 72 73 74 75 `````` (* 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]. See Coq bug https://github.com/coq/coq/issues/7916. *) Global Instance rtc_reflexive: Reflexive (rtc R) | 10. `````` Robbert Krebbers committed Sep 06, 2014 76 77 78 79 80 `````` Proof. exact (@rtc_refl A R). Qed. Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z. Proof. induction 1; eauto. Qed. Global Instance: Transitive (rtc R). Proof. exact rtc_transitive. Qed. `````` Robbert Krebbers committed Aug 29, 2012 81 `````` Lemma rtc_once x y : R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 82 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 83 `````` Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z. `````` Ralf Jung committed Feb 20, 2016 84 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 85 86 `````` 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 87 88 89 90 `````` 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 91 92 `````` 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 93 `````` ∀ x z, rtc R x z → P x z. `````` Robbert Krebbers committed Aug 29, 2012 94 95 96 97 98 `````` 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 99 100 101 102 103 104 `````` 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 105 `````` 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 106 `````` Proof. revert z. apply rtc_ind_r; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 107 108 `````` Lemma nsteps_once x y : R x y → nsteps R 1 x y. `````` Robbert Krebbers committed Sep 06, 2014 109 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 110 111 `````` 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 112 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 113 `````` 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 114 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 115 `````` Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 116 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 117 `````` Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 118 `````` Proof. induction 1; firstorder eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 119 120 `````` Lemma bsteps_once n x y : R x y → bsteps R (S n) x y. `````` Robbert Krebbers committed Sep 06, 2014 121 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 122 123 `````` 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 124 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 125 126 127 128 129 130 131 132 133 `````` 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 134 `````` Proof. apply bsteps_weaken. lia. Qed. `````` Robbert Krebbers committed Aug 29, 2012 135 136 `````` 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 137 `````` Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed. `````` Robbert Krebbers committed Aug 29, 2012 138 `````` 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 139 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 140 `````` Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 141 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 142 `````` Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 143 `````` Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 144 145 146 147 148 149 `````` 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 150 151 `````` 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 152 153 154 `````` 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 155 `````` intros [|m'] [??]; [lia |]. apply Pstep with x'. `````` Robbert Krebbers committed Feb 17, 2016 156 157 158 `````` - apply bsteps_weaken with n; intuition lia. - done. - apply H; intuition lia. `````` Robbert Krebbers committed Jan 09, 2013 159 `````` Qed. `````` Robbert Krebbers committed Aug 29, 2012 160 `````` `````` Robbert Krebbers committed Sep 06, 2014 161 162 163 164 `````` Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z. Proof. induction 1; eauto. Qed. Global Instance: Transitive (tc R). Proof. exact tc_transitive. Qed. `````` Robbert Krebbers committed Aug 29, 2012 165 `````` Lemma tc_r x y z : tc R x y → R y z → tc R x z. `````` Ralf Jung committed Feb 20, 2016 166 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 167 168 169 170 `````` 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 171 `````` Lemma tc_rtc x y : tc R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 172 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 173 `````` `````` Robbert Krebbers committed Sep 06, 2014 174 `````` Lemma all_loop_red x : all_loop R x → red R x. `````` Robbert Krebbers committed Aug 29, 2012 175 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 176 `````` Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y. `````` Robbert Krebbers committed Aug 29, 2012 177 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 178 179 180 181 `````` 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 182 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2014 183 184 185 `````` 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 186 187 188 `````` Qed. End rtc. `````` Robbert Krebbers committed Sep 06, 2014 189 190 191 ``````Hint Constructors rtc nsteps bsteps tc : ars. Hint Resolve rtc_once rtc_r tc_r rtc_transitive tc_rtc_l tc_rtc_r tc_rtc bsteps_once bsteps_r bsteps_refl bsteps_trans : ars. `````` Robbert Krebbers committed Aug 29, 2012 192 193 194 `````` (** * Theorems on sub relations *) Section subrel. `````` Robbert Krebbers committed Apr 22, 2015 195 196 197 198 199 200 `````` 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 201 202 `````` 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 203 ``````End subrel. `````` Robbert Krebbers committed Jan 09, 2013 204 `````` `````` Robbert Krebbers committed Apr 22, 2015 205 ``````(** * Theorems on well founded relations *) `````` Robbert Krebbers committed Jan 09, 2013 206 ``````Notation wf := well_founded. `````` Robbert Krebbers committed Nov 09, 2017 207 208 ``````Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R := Acc_intro_generator n wfR. `````` Robbert Krebbers committed Jan 09, 2013 209 210 211 212 213 214 `````` (* 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 215 `````` `````` Robbert Krebbers committed Nov 09, 2017 216 217 218 219 220 221 222 223 224 225 226 ``````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 227 ``````Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)) `````` Robbert Krebbers committed Nov 17, 2016 228 229 230 231 232 `````` (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 233 ``````Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed. `````` Johannes Kloos committed Nov 01, 2017 234 235 236 237 238 239 240 241 242 243 244 245 246 `````` 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): E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)). Proof. unfold Fix. destruct (wfR x); cbn. apply HF; intros. apply Fix_F_proper; auto. Qed.``````