ars.v 9.54 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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. *)
7
Require Import Wf_nat.
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's avatar
Robbert Krebbers committed
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.
49 50
End definitions.

51 52
Hint Unfold nf red.

53 54 55 56
(** * General theorems *)
Section rtc.
  Context `{R : relation A}.

Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
  Hint Constructors rtc nsteps bsteps tc.

59
  Global Instance rtc_reflexive: Reflexive (rtc R).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
65
  Lemma rtc_once x y : R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Proof. eauto. Qed.
67
  Instance rtc_once_subrel: subrelation R (rtc R).
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's avatar
Robbert Krebbers committed
70
  Proof. intros. etransitivity; eauto. Qed.
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.
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.
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) :
79
     x z, rtc R x z  P x z.
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.
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.
91
  Lemma rtc_inv_r x z : rtc R x z  x = z   y, rtc R x y  R y z.
92
  Proof. revert z. apply rtc_ind_r; eauto. Qed.
93 94

  Lemma nsteps_once x y : R x y  nsteps R 1 x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  Proof. eauto. Qed.
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's avatar
Robbert Krebbers committed
98
  Proof. induction 1; simpl; eauto. Qed.
99
  Lemma nsteps_r n x y z : nsteps R n x y  R y z  nsteps R (S n) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  Proof. induction 1; eauto. Qed.
101
  Lemma nsteps_rtc n x y : nsteps R n x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  Proof. induction 1; eauto. Qed.
103
  Lemma rtc_nsteps x y : rtc R x y   n, nsteps R n x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Proof. induction 1; firstorder eauto. Qed.
105 106

  Lemma bsteps_once n x y : R x y  bsteps R (S n) x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  Proof. eauto. Qed.
108 109
  Lemma bsteps_plus_r n m x y :
    bsteps R n x y  bsteps R (n + m) x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  Proof. induction 1; simpl; eauto. Qed.
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.
120
  Proof. apply bsteps_weaken. lia. Qed.
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's avatar
Robbert Krebbers committed
123
  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
124
  Lemma bsteps_r n x y z : bsteps R n x y  R y z  bsteps R (S n) x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
  Proof. induction 1; eauto. Qed.
126
  Lemma bsteps_rtc n x y : bsteps R n x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Proof. induction 1; eauto. Qed.
128
  Lemma rtc_bsteps x y : rtc R x y   n, bsteps R n x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed.
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's avatar
Robbert Krebbers committed
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. }
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's avatar
Robbert Krebbers committed
141
    intros [|m'] [??]; [lia |]. apply Pstep with x'.
142 143 144 145
    * apply bsteps_weaken with n; intuition lia.
    * done.
    * apply H; intuition lia.
  Qed.
146

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
151
  Lemma tc_r x y z : tc R x y  R y z  tc R x z.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
157
  Lemma tc_rtc x y : tc R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Proof. induction 1; eauto. Qed.
159
  Instance tc_once_subrel: subrelation (tc R) (rtc R).
160 161
  Proof. exact @tc_rtc. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
162
  Lemma all_loop_red x : all_loop R x  red R x.
163
  Proof. destruct 1; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
  Lemma all_loop_step x y : all_loop R x  R x y  all_loop R y.
165
  Proof. destruct 1; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
170
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
174 175 176
  Qed.
End rtc.

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's avatar
Robbert Krebbers committed
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.
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.
192
  Proof. intros [y ?]. exists y. by apply Hsub. Qed.
193
  Lemma nf_subrel x : nf R2 x  nf R1 x.
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.
204
End subrel.
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].