ars.v 9.54 KB
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` 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 Jan 09, 2013 7 ``````Require Import Wf_nat. `````` Robbert Krebbers committed Aug 29, 2012 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 ``````Require Export tactics base. (** * 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. (** 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 40 41 42 43 44 45 46 47 48 `````` (** 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 49 50 ``````End definitions. `````` Robbert Krebbers committed Oct 09, 2014 51 52 ``````Hint Unfold nf red. `````` Robbert Krebbers committed Aug 29, 2012 53 54 55 56 ``````(** * General theorems *) Section rtc. Context `{R : relation A}. `````` Robbert Krebbers committed Sep 06, 2014 57 58 `````` Hint Constructors rtc nsteps bsteps tc. `````` Robbert Krebbers committed Jan 09, 2013 59 `````` Global Instance rtc_reflexive: Reflexive (rtc R). `````` Robbert Krebbers committed Sep 06, 2014 60 61 62 63 64 `````` 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 65 `````` Lemma rtc_once x y : R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 66 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 67 `````` Instance rtc_once_subrel: subrelation R (rtc R). `````` Robbert Krebbers committed Aug 29, 2012 68 69 `````` Proof. exact @rtc_once. Qed. Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z. `````` Robbert Krebbers committed Sep 06, 2014 70 `````` Proof. intros. etransitivity; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 71 72 `````` 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 73 74 75 76 `````` 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 77 78 `````` 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 79 `````` ∀ x z, rtc R x z → P x z. `````` Robbert Krebbers committed Aug 29, 2012 80 81 82 83 84 `````` 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 85 86 87 88 89 90 `````` 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 91 `````` 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 92 `````` Proof. revert z. apply rtc_ind_r; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 93 94 `````` Lemma nsteps_once x y : R x y → nsteps R 1 x y. `````` Robbert Krebbers committed Sep 06, 2014 95 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 96 97 `````` 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 98 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 99 `````` 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 100 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 101 `````` Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 102 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 103 `````` Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 104 `````` Proof. induction 1; firstorder eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 105 106 `````` Lemma bsteps_once n x y : R x y → bsteps R (S n) x y. `````` Robbert Krebbers committed Sep 06, 2014 107 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 108 109 `````` 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 110 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 111 112 113 114 115 116 117 118 119 `````` 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 120 `````` Proof. apply bsteps_weaken. lia. Qed. `````` Robbert Krebbers committed Aug 29, 2012 121 122 `````` 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 123 `````` Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed. `````` Robbert Krebbers committed Aug 29, 2012 124 `````` 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 125 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 126 `````` Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 127 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 128 `````` Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 129 `````` Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 130 131 132 133 134 135 `````` 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 136 137 `````` 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 138 139 140 `````` 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 141 `````` intros [|m'] [??]; [lia |]. apply Pstep with x'. `````` Robbert Krebbers committed Jan 09, 2013 142 143 144 145 `````` * apply bsteps_weaken with n; intuition lia. * done. * apply H; intuition lia. Qed. `````` Robbert Krebbers committed Aug 29, 2012 146 `````` `````` Robbert Krebbers committed Sep 06, 2014 147 148 149 150 `````` 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 151 `````` Lemma tc_r x y z : tc R x y → R y z → tc R x z. `````` Robbert Krebbers committed Sep 06, 2014 152 153 154 155 156 `````` Proof. intros. etransitivity; eauto. Qed. 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 157 `````` Lemma tc_rtc x y : tc R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 158 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 159 `````` Instance tc_once_subrel: subrelation (tc R) (rtc R). `````` Robbert Krebbers committed Aug 29, 2012 160 161 `````` Proof. exact @tc_rtc. Qed. `````` Robbert Krebbers committed Sep 06, 2014 162 `````` Lemma all_loop_red x : all_loop R x → red R x. `````` Robbert Krebbers committed Aug 29, 2012 163 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 164 `````` Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y. `````` Robbert Krebbers committed Aug 29, 2012 165 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 166 167 168 169 `````` 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 170 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2014 171 172 173 `````` 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 174 175 176 `````` Qed. End rtc. `````` Robbert Krebbers committed Jan 09, 2013 177 178 179 180 181 182 ``````(* Avoid too eager type class resolution *) Hint Extern 5 (subrelation _ (rtc _)) => eapply @rtc_once_subrel : typeclass_instances. Hint Extern 5 (subrelation _ (tc _)) => eapply @tc_once_subrel : typeclass_instances. `````` Robbert Krebbers committed Sep 06, 2014 183 184 185 ``````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 186 187 188 189 190 191 `````` (** * Theorems on sub relations *) Section subrel. Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2). Lemma red_subrel x : red R1 x → red R2 x. `````` Robbert Krebbers committed Jan 09, 2013 192 `````` Proof. intros [y ?]. exists y. by apply Hsub. Qed. `````` Robbert Krebbers committed Aug 29, 2012 193 `````` Lemma nf_subrel x : nf R2 x → nf R1 x. `````` Robbert Krebbers committed Jan 09, 2013 194 195 196 197 198 199 200 201 202 203 `````` Proof. intros H1 H2. destruct H1. by apply red_subrel. Qed. Instance rtc_subrel: subrelation (rtc R1) (rtc R2). Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed. Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n). Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed. Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n). Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed. Instance tc_subrel: subrelation (tc R1) (tc R2). Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed. `````` Robbert Krebbers committed Aug 29, 2012 204 ``````End subrel. `````` Robbert Krebbers committed Jan 09, 2013 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 `````` Hint Extern 5 (subrelation (rtc _) (rtc _)) => eapply @rtc_subrel : typeclass_instances. Hint Extern 5 (subrelation (nsteps _) (nsteps _)) => eapply @nsteps_subrel : typeclass_instances. Hint Extern 5 (subrelation (bsteps _) (bsteps _)) => eapply @bsteps_subrel : typeclass_instances. Hint Extern 5 (subrelation (tc _) (tc _)) => eapply @tc_subrel : typeclass_instances. Notation wf := well_founded. Section wf. Context `{R : relation A}. (** A trick by Thomas Braibant to compute with well-founded recursions: it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness proof, so that the actual proof is never reached in practise. *) Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R := match n with | 0 => wfR | S n => λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y) end. Lemma wf_projected `(R2 : relation B) (f : A → B) : (∀ x y, R x y → R2 (f x) (f y)) → wf R2 → wf R. Proof. intros Hf Hwf. cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R 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. End wf. (* 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].``````