relations.v 9 KB
Newer Older
 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 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 Oct 09, 2014 57 58 ``````Hint Unfold nf red. `````` Robbert Krebbers committed Aug 29, 2012 59 60 61 62 ``````(** * General theorems *) Section rtc. Context `{R : relation A}. `````` Robbert Krebbers committed Sep 06, 2014 63 64 `````` Hint Constructors rtc nsteps bsteps tc. `````` Robbert Krebbers committed Jan 09, 2013 65 `````` Global Instance rtc_reflexive: Reflexive (rtc R). `````` Robbert Krebbers committed Sep 06, 2014 66 67 68 69 70 `````` 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 71 `````` Lemma rtc_once x y : R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 72 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 73 `````` Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z. `````` Ralf Jung committed Feb 20, 2016 74 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 75 76 `````` 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 77 78 79 80 `````` 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 81 82 `````` 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 83 `````` ∀ x z, rtc R x z → P x z. `````` Robbert Krebbers committed Aug 29, 2012 84 85 86 87 88 `````` 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 89 90 91 92 93 94 `````` 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 95 `````` 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 96 `````` Proof. revert z. apply rtc_ind_r; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 97 98 `````` Lemma nsteps_once x y : R x y → nsteps R 1 x y. `````` Robbert Krebbers committed Sep 06, 2014 99 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 100 101 `````` 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 102 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 103 `````` 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 104 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 105 `````` Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 106 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 107 `````` Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 108 `````` Proof. induction 1; firstorder eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 109 110 `````` Lemma bsteps_once n x y : R x y → bsteps R (S n) x y. `````` Robbert Krebbers committed Sep 06, 2014 111 `````` Proof. eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 112 113 `````` 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 114 `````` Proof. induction 1; simpl; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 115 116 117 118 119 120 121 122 123 `````` 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 124 `````` Proof. apply bsteps_weaken. lia. Qed. `````` Robbert Krebbers committed Aug 29, 2012 125 126 `````` 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 127 `````` Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed. `````` Robbert Krebbers committed Aug 29, 2012 128 `````` 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 129 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 130 `````` Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 131 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 132 `````` Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y. `````` Robbert Krebbers committed Sep 06, 2014 133 `````` Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed. `````` Robbert Krebbers committed Jan 09, 2013 134 135 136 137 138 139 `````` 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 140 141 `````` 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 142 143 144 `````` 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 145 `````` intros [|m'] [??]; [lia |]. apply Pstep with x'. `````` Robbert Krebbers committed Feb 17, 2016 146 147 148 `````` - apply bsteps_weaken with n; intuition lia. - done. - apply H; intuition lia. `````` Robbert Krebbers committed Jan 09, 2013 149 `````` Qed. `````` Robbert Krebbers committed Aug 29, 2012 150 `````` `````` Robbert Krebbers committed Sep 06, 2014 151 152 153 154 `````` 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 155 `````` Lemma tc_r x y z : tc R x y → R y z → tc R x z. `````` Ralf Jung committed Feb 20, 2016 156 `````` Proof. intros. etrans; eauto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 157 158 159 160 `````` 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 161 `````` Lemma tc_rtc x y : tc R x y → rtc R x y. `````` Robbert Krebbers committed Sep 06, 2014 162 `````` Proof. induction 1; eauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 163 `````` `````` Robbert Krebbers committed Sep 06, 2014 164 `````` Lemma all_loop_red x : all_loop R x → red R x. `````` Robbert Krebbers committed Aug 29, 2012 165 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 166 `````` Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y. `````` Robbert Krebbers committed Aug 29, 2012 167 `````` Proof. destruct 1; auto. Qed. `````` Robbert Krebbers committed Sep 06, 2014 168 169 170 171 `````` 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 172 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2014 173 174 175 `````` 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 176 177 178 `````` Qed. End rtc. `````` Robbert Krebbers committed Sep 06, 2014 179 180 181 ``````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 182 183 184 `````` (** * Theorems on sub relations *) Section subrel. `````` Robbert Krebbers committed Apr 22, 2015 185 186 187 188 189 190 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 191 ``````End subrel. `````` Robbert Krebbers committed Jan 09, 2013 192 `````` `````` Robbert Krebbers committed Apr 22, 2015 193 ``````(** * Theorems on well founded relations *) `````` Robbert Krebbers committed Jan 09, 2013 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 ``````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]. `````` Robbert Krebbers committed Nov 17, 2016 225 `````` `````` Robbert Krebbers committed Nov 17, 2016 226 ``````Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)) `````` Robbert Krebbers committed Nov 17, 2016 227 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). Proof. revert x acc1 acc2. fix 2. intros x [acc1] [acc2]; simpl; auto. Qed.``````