relations.v 8.58 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
8
From Coq Require Import Wf_nat.
From stdpp Require Export tactics base.
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

(** * 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's avatar
Robbert Krebbers committed
25
26
27
28
29
  (** 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.

30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
  (** 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
45
46
47
48
49
50
51
52
53
  (** 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.
54
55
End definitions.

56
57
Hint Unfold nf red.

58
59
60
61
(** * General theorems *)
Section rtc.
  Context `{R : relation A}.

Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
  Hint Constructors rtc nsteps bsteps tc.

64
  Global Instance rtc_reflexive: Reflexive (rtc R).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
69
  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.
70
  Lemma rtc_once x y : R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  Proof. eauto. Qed.
72
  Lemma rtc_r x y z : rtc R x y  R y z  rtc R x z.
73
  Proof. intros. etrans; eauto. Qed.
74
75
  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.
76
77
78
79
  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.
80
81
  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) :
82
     x z, rtc R x z  P x z.
83
84
85
86
87
  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.
88
89
90
91
92
93
  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.
94
  Lemma rtc_inv_r x z : rtc R x z  x = z   y, rtc R x y  R y z.
95
  Proof. revert z. apply rtc_ind_r; eauto. Qed.
96
97

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

  Lemma bsteps_once n x y : R x y  bsteps R (S n) x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  Proof. eauto. Qed.
111
112
  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
113
  Proof. induction 1; simpl; eauto. Qed.
114
115
116
117
118
119
120
121
122
  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.
123
  Proof. apply bsteps_weaken. lia. Qed.
124
125
  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
126
  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
127
  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
128
  Proof. induction 1; eauto. Qed.
129
  Lemma bsteps_rtc n x y : bsteps R n x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  Proof. induction 1; eauto. Qed.
131
  Lemma rtc_bsteps x y : rtc R x y   n, bsteps R n x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed.
133
134
135
136
137
138
  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
139
140
      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. }
141
142
143
    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
144
    intros [|m'] [??]; [lia |]. apply Pstep with x'.
145
146
147
    - apply bsteps_weaken with n; intuition lia.
    - done.
    - apply H; intuition lia.
148
  Qed.
149

Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
  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.
154
  Lemma tc_r x y z : tc R x y  R y z  tc R x z.
155
  Proof. intros. etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
  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.
160
  Lemma tc_rtc x y : tc R x y  rtc R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  Proof. induction 1; eauto. Qed.
162

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

Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
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.
181
182
183

(** * Theorems on sub relations *)
Section subrel.
184
185
186
187
188
189
  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.
190
End subrel.
191

192
(** * Theorems on well founded relations *)
193
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
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].