Mercurial > cpdt > repo

annotate src/DeBruijn.v @ 326:f1d390f305d7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adjust toc
author Adam Chlipala <adam@chlipala.net>
date Thu, 22 Sep 2011 11:11:03 -0400
parents d5787b70cf48
children
rev   line source
adam@291 1 (* Copyright (c) 2009-2010, Adam Chlipala
adamc@265 2 *
adamc@265 3 * This work is licensed under a
adamc@265 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@265 5 * Unported License.
adamc@265 6 * The license text is available at:
adamc@265 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@265 8 *)
adamc@265 9
adamc@265 10 (* begin hide *)
adamc@265 11 Set Implicit Arguments.
adamc@265 12
adamc@265 13 Require Import Eqdep.
adamc@265 14
adam@314 15 Require Import DepList CpdtTactics.
adamc@265 16 (* end hide *)
adamc@265 17
adamc@265 18 (** remove printing * *)
adamc@265 19 (** printing || $\mid\mid$ *)
adamc@265 20
adamc@265 21 (** %\chapter{Dependent De Bruijn Indices}% *)
adamc@265 22
adamc@265 23 (** The previous chapter introduced the most common form of de Bruijn indices, without essential use of dependent types. In earlier chapters, we used dependent de Bruijn indices to illustrate tricks for working with dependent types. This chapter presents one complete case study with dependent de Bruijn indices, focusing on producing the most maintainable proof possible of a classic theorem about lambda calculus.
adamc@265 24
adamc@265 25 The proof that follows does not provide a complete guide to all kinds of formalization with de Bruijn indices. Rather, it is intended as an example of some simple design patterns that can make proving standard theorems much easier.
adamc@265 26
adamc@265 27 We will prove commutativity of capture-avoiding substitution for basic untyped lambda calculus:
adamc@265 28
adamc@265 29 %$$x_1 \neq x_2 \Rightarrow [e_1/x_1][e_2/x_2]e = [e_2/x_2][[e_2/x_2]e_1/x_1]e$$%
adamc@265 30 #<tt>x1 <> x2 => [e1/x1][e2/x2]e = [e2/x2][[e2/x2]e1/x1]e</tt>#
adamc@265 31 *)
adamc@265 32
adamc@265 33 (** * Defining Syntax and Its Associated Operations *)
adamc@265 34
adamc@265 35 (** Our definition of expression syntax should be unsurprising. An expression of type [exp n] may refer to [n] different free variables. *)
adamc@265 36
adamc@265 37 Inductive exp : nat -> Type :=
adamc@265 38 | Var : forall n, fin n -> exp n
adamc@265 39 | App : forall n, exp n -> exp n -> exp n
adamc@265 40 | Abs : forall n, exp (S n) -> exp n.
adamc@265 41
adamc@265 42 (** The classic implementation of substitution in de Bruijn terms requires an auxiliary operation, %\emph{%lifting%}%, which increments the indices of all free variables in an expression. We need to lift whenever we %``%#"#go under a binder.#"#%''% It is useful to write an auxiliary function [liftVar] that lifts a variable; that is, [liftVar x y] will return [y + 1] if [y >= x], and it will return [y] otherwise. This simple description uses numbers rather than our dependent [fin] family, so the actual specification is more involved.
adamc@265 43
adamc@265 44 Combining a number of dependent types tricks, we wind up with this concrete realization. *)
adamc@265 45
adamc@265 46 Fixpoint liftVar n (x : fin n) : fin (pred n) -> fin n :=
adamc@265 47 match x with
adamc@265 48 | First _ => fun y => Next y
adamc@265 49 | Next _ x' => fun y =>
adamc@265 50 match y in fin n' return fin n' -> (fin (pred n') -> fin n')
adamc@265 51 -> fin (S n') with
adamc@265 52 | First _ => fun x' _ => First
adamc@265 53 | Next _ y' => fun _ fx' => Next (fx' y')
adamc@265 54 end x' (liftVar x')
adamc@265 55 end.
adamc@265 56
adamc@265 57 (** Now it is easy to implement the main lifting operation. *)
adamc@265 58
adamc@265 59 Fixpoint lift n (e : exp n) : fin (S n) -> exp (S n) :=
adamc@265 60 match e with
adamc@265 61 | Var _ f' => fun f => Var (liftVar f f')
adamc@265 62 | App _ e1 e2 => fun f => App (lift e1 f) (lift e2 f)
adamc@265 63 | Abs _ e1 => fun f => Abs (lift e1 (Next f))
adamc@265 64 end.
adamc@265 65
adamc@265 66 (** To define substitution itself, we will need to apply some explicit type casts, based on equalities between types. A single equality will suffice for all of our casts. Its statement is somewhat strange: it quantifies over a variable [f] of type [fin n], but then never mentions [f]. Rather, quantifying over [f] is useful because [fin] is a dependent type that is inhabited or not depending on its index. The body of the theorem, [S (pred n) = n], is true only for [n] $> 0$, but we can prove it by contradiction when [n = 0], because we have around a value [f] of the uninhabited type [fin 0]. *)
adamc@265 67
adamc@265 68 Theorem nzf : forall n (f : fin n), S (pred n) = n.
adamc@265 69 destruct 1; trivial.
adamc@265 70 Qed.
adamc@265 71
adamc@265 72 (** Now we define a notation to streamline our cast expressions. The code [[f return n, r for e]] denotes a cast of expression [e] whose type can be obtained by substituting some number [n1] for [n] in [r]. [f] should be a proof that [n1 = n2], for any [n2]. In that case, the type of the cast expression is [r] with [n2] substituted for [n]. *)
adamc@265 73
adamc@265 74 Notation "[ f 'return' n , r 'for' e ]" :=
adamc@265 75 match f in _ = n return r with
adamc@265 76 | refl_equal => e
adamc@265 77 end.
adamc@265 78
adamc@265 79 (** This notation is useful in defining a variable substitution operation. The idea is that [substVar x y] returns [None] if [x = y]; otherwise, it returns a %``%#"#squished#"#%''% version of [y] with a smaller [fin] index, reflecting that variable [x] has been substituted away. Without dependent types, this would be a simple definition. With dependency, it is reasonably intricate, and our main task in automating proofs about it will be hiding that intricacy. *)
adamc@265 80
adamc@265 81 Fixpoint substVar n (x : fin n) : fin n -> option (fin (pred n)) :=
adamc@265 82 match x with
adamc@265 83 | First _ => fun y =>
adamc@265 84 match y in fin n' return option (fin (pred n')) with
adamc@265 85 | First _ => None
adamc@265 86 | Next _ f' => Some f'
adamc@265 87 end
adamc@265 88 | Next _ x' => fun y =>
adamc@265 89 match y in fin n'
adamc@265 90 return fin (pred n') -> (fin (pred n') -> option (fin (pred (pred n'))))
adamc@265 91 -> option (fin (pred n')) with
adamc@265 92 | First _ => fun x' _ => Some [nzf x' return n, fin n for First]
adamc@265 93 | Next _ y' => fun _ fx' =>
adamc@265 94 match fx' y' with
adamc@265 95 | None => None
adamc@265 96 | Some f => Some [nzf y' return n, fin n for Next f]
adamc@265 97 end
adamc@265 98 end x' (substVar x')
adamc@265 99 end.
adamc@265 100
adamc@265 101 (** It is now easy to define our final substitution function. The abstraction case involves two casts, where one uses the [sym_eq] function to convert a proof of [n1 = n2] into a proof of [n2 = n1]. *)
adamc@265 102
adamc@265 103 Fixpoint subst n (e : exp n) : fin n -> exp (pred n) -> exp (pred n) :=
adamc@265 104 match e with
adamc@265 105 | Var _ f' => fun f v => match substVar f f' with
adamc@265 106 | None => v
adamc@265 107 | Some f'' => Var f''
adamc@265 108 end
adamc@265 109 | App _ e1 e2 => fun f v => App (subst e1 f v) (subst e2 f v)
adamc@265 110 | Abs _ e1 => fun f v => Abs [sym_eq (nzf f) return n, exp n for
adamc@265 111 subst e1 (Next f) [nzf f return n, exp n for lift v First]]
adamc@265 112 end.
adamc@265 113
adamc@265 114 (** Our final commutativity theorem is about [subst], but our proofs will rely on a few more auxiliary definitions. First, we will want an operation [more] that increments the index of a [fin] while preserving its interpretation as a number. *)
adamc@265 115
adamc@265 116 Fixpoint more n (f : fin n) : fin (S n) :=
adamc@265 117 match f with
adamc@265 118 | First _ => First
adamc@265 119 | Next _ f' => Next (more f')
adamc@265 120 end.
adamc@265 121
adamc@265 122 (** Second, we will want a kind of inverse to [liftVar]. *)
adamc@265 123
adamc@265 124 Fixpoint unliftVar n (f : fin n) : fin (pred n) -> fin (pred n) :=
adamc@265 125 match f with
adamc@265 126 | First _ => fun g => [nzf g return n, fin n for First]
adamc@265 127 | Next _ f' => fun g =>
adamc@265 128 match g in fin n'
adamc@265 129 return fin n' -> (fin (pred n') -> fin (pred n')) -> fin n' with
adamc@265 130 | First _ => fun f' _ => f'
adamc@265 131 | Next _ g' => fun _ unlift => Next (unlift g')
adamc@265 132 end f' (unliftVar f')
adamc@265 133 end.
adamc@265 134
adamc@265 135
adamc@265 136 (** * Custom Tactics *)
adamc@265 137
adamc@265 138 (* begin hide *)
adamc@265 139 Ltac simp := repeat progress (crush; try discriminate;
adamc@265 140 repeat match goal with
adamc@265 141 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf)
adamc@265 142 | [ _ : context[match ?pf with refl_equal => _ end] |- _ ] => rewrite (UIP_refl _ _ pf) in *
adamc@265 143
adamc@265 144 | [ H : Next _ = Next _ |- _ ] => injection H; clear H
adamc@265 145 | [ H : ?E = _, H' : ?E = _ |- _ ] => rewrite H in H'
adamc@265 146 | [ H : ?P |- _ ] => rewrite H in *; [match P with
adamc@265 147 | forall x, _ => clear H
adamc@265 148 | _ => idtac
adamc@265 149 end]
adamc@265 150 end).
adamc@265 151 (* end hide *)
adamc@265 152
adam@291 153 (** Less than a page of tactic code will be sufficient to automate our proof of commutativity. We start by defining a workhorse simplification tactic [simp], which extends [crush] in a few ways.
adamc@265 154
adamc@265 155 [[
adamc@265 156 Ltac simp := repeat progress (crush; try discriminate;
adamc@265 157
adamc@265 158 ]]
adamc@265 159
adamc@265 160 We enter an inner loop of applying hints specific to our domain.
adamc@265 161
adamc@265 162 [[
adamc@265 163 repeat match goal with
adamc@265 164
adamc@265 165 ]]
adamc@265 166
adamc@265 167 Our first two hints find places where equality proofs are pattern-matched on. The first hint matches pattern-matches in the conclusion, while the second hint matches pattern-matches in hypotheses. In each case, we apply the library theorem [UIP_refl], which says that any proof of a fact like [e = e] is itself equal to [refl_equal]. Rewriting with this fact enables reduction of the pattern-match that we found.
adamc@265 168
adamc@265 169 [[
adamc@265 170 | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@265 171 rewrite (UIP_refl _ _ pf)
adamc@265 172 | [ _ : context[match ?pf with refl_equal => _ end] |- _ ] =>
adamc@265 173 rewrite (UIP_refl _ _ pf) in *
adamc@265 174
adamc@265 175 ]]
adamc@265 176
adamc@265 177 The next hint finds an opportunity to invert a [fin] equality hypothesis.
adamc@265 178
adamc@265 179 [[
adamc@265 180 | [ H : Next _ = Next _ |- _ ] => injection H; clear H
adamc@265 181
adamc@265 182 ]]
adamc@265 183
adamc@265 184 If we have two equality hypotheses that share a lefthand side, we can use one to rewrite the other, bringing the hypotheses' righthand sides together in a single equation.
adamc@265 185
adamc@265 186 [[
adamc@265 187 | [ H : ?E = _, H' : ?E = _ |- _ ] => rewrite H in H'
adamc@265 188
adamc@265 189 ]]
adamc@265 190
adamc@265 191 Finally, we would like automatic use of quantified equality hypotheses to perform rewriting. We pattern-match a hypothesis [H] asserting proposition [P]. We try to use [H] to perform rewriting everywhere in our goal. The rewrite succeeds if it generates no additional hypotheses, and, to prevent infinite loops in proof search, we clear [H] if it begins with universal quantification.
adamc@265 192
adamc@265 193 [[
adamc@265 194 | [ H : ?P |- _ ] => rewrite H in *; [match P with
adamc@265 195 | forall x, _ => clear H
adamc@265 196 | _ => idtac
adamc@265 197 end]
adamc@265 198 end).
adamc@265 199
adamc@265 200 ]]
adamc@265 201
adamc@265 202 In implementing another level of automation, it will be useful to mark which free variables we generated with tactics, as opposed to which were present in the original theorem statement. We use a dummy marker predicate [Generated] to record that information. A tactic [not_generated] fails if and only if its argument is a generated variable, and a tactic [generate] records that its argument is generated. *)
adamc@265 203
adamc@265 204 Definition Generated n (_ : fin n) := True.
adamc@265 205
adamc@265 206 Ltac not_generated x :=
adamc@265 207 match goal with
adamc@265 208 | [ _ : Generated x |- _ ] => fail 1
adamc@265 209 | _ => idtac
adamc@265 210 end.
adamc@265 211
adamc@265 212 Ltac generate x := assert (Generated x); [ constructor | ].
adamc@265 213
adamc@265 214 (** A tactic [destructG] performs case analysis on [fin] values. The built-in case analysis tactics are not smart enough to handle all situations, and we also want to mark new variables as generated, to avoid infinite loops of case analysis. Our [destructG] tactic will only proceed if its argument is not generated. *)
adamc@265 215
adamc@265 216 Theorem fin_inv : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adamc@265 217 intros; dep_destruct f; eauto.
adamc@265 218 Qed.
adamc@265 219
adamc@265 220 Ltac destructG E :=
adamc@265 221 not_generated E; let x := fresh "x" in
adamc@265 222 (destruct (fin_inv E) as [ | [x]] || destruct E as [ | ? x]);
adamc@265 223 [ | generate x ].
adamc@265 224
adamc@265 225 (* begin hide *)
adamc@265 226 Ltac dester := simp;
adamc@265 227 repeat (match goal with
adamc@265 228 | [ x : fin _, H : _ = _, IH : forall f : fin _, _ |- _ ] =>
adamc@265 229 generalize (IH x); clear IH; intro IH; rewrite H in IH
adamc@265 230 | [ x : fin _, y : fin _, H : _ = _, IH : forall (f : fin _) (g : fin _), _ |- _ ] =>
adamc@265 231 generalize (IH x y); clear IH; intro IH; rewrite H in IH
adamc@265 232 | [ |- context[match ?E with First _ => _ | Next _ _ => _ end] ] => destructG E
adamc@265 233 | [ _ : context[match ?E with First _ => _ | Next _ _ => _ end] |- _ ] => destructG E
adamc@265 234 | [ |- context[more ?E] ] => destructG E
adamc@265 235 | [ x : fin ?n |- _ ] =>
adamc@265 236 match goal with
adamc@265 237 | [ |- context[nzf x] ] =>
adamc@265 238 destruct n; [ inversion x | ]
adamc@265 239 end
adamc@265 240 | [ x : fin (pred ?n), y : fin ?n |- _ ] =>
adamc@265 241 match goal with
adamc@265 242 | [ |- context[nzf x] ] =>
adamc@265 243 destruct n; [ inversion y | ]
adamc@265 244 end
adamc@265 245 | [ |- context[match ?E with None => _ | Some _ => _ end] ] =>
adamc@265 246 match E with
adamc@265 247 | match _ with None => _ | Some _ => _ end => fail 1
adamc@265 248 | _ => case_eq E; firstorder
adamc@265 249 end
adamc@265 250 end; simp); eauto.
adamc@265 251 (* end hide *)
adamc@265 252
adamc@265 253 (** Our most powerful workhorse tactic will be [dester], which incorporates all of [simp]'s simplifications and adds heuristics for automatic case analysis and automatic quantifier instantiation.
adamc@265 254
adamc@265 255 [[
adamc@265 256 Ltac dester := simp;
adamc@265 257 repeat (match goal with
adamc@265 258
adamc@265 259 ]]
adamc@265 260
adamc@265 261 The first hint expresses our main insight into quantifier instantiation. We identify a hypothesis [IH] that begins with quantification over [fin] values. We also identify a free [fin] variable [x] and an arbitrary equality hypothesis [H]. Given these, we try instantiating [IH] with [x]. We know we chose correctly if the instantiated proposition includes an opportunity to rewrite using [H].
adamc@265 262
adamc@265 263 [[
adamc@265 264 | [ x : fin _, H : _ = _, IH : forall f : fin _, _ |- _ ] =>
adamc@265 265 generalize (IH x); clear IH; intro IH; rewrite H in IH
adamc@265 266
adamc@265 267 ]]
adamc@265 268
adamc@265 269 This basic idea suffices for all of our explicit quantifier instantiation. We add one more variant that handles cases where an opportunity for rewriting is only exposed if two different quantifiers are instantiated at once.
adamc@265 270
adamc@265 271 [[
adamc@265 272 | [ x : fin _, y : fin _, H : _ = _,
adamc@265 273 IH : forall (f : fin _) (g : fin _), _ |- _ ] =>
adamc@265 274 generalize (IH x y); clear IH; intro IH; rewrite H in IH
adamc@265 275
adamc@265 276 ]]
adamc@265 277
adamc@265 278 We want to case-analyze on any [fin] expression that is the discriminee of a [match] expression or an argument to [more].
adamc@265 279
adamc@265 280 [[
adamc@265 281 | [ |- context[match ?E with First _ => _ | Next _ _ => _ end] ] =>
adamc@265 282 destructG E
adamc@265 283 | [ _ : context[match ?E with First _ => _ | Next _ _ => _ end] |- _ ] =>
adamc@265 284 destructG E
adamc@265 285 | [ |- context[more ?E] ] => destructG E
adamc@265 286
adamc@265 287 ]]
adamc@265 288
adamc@265 289 Recall that [simp] will simplify equality proof terms of facts like [e = e]. The proofs in question will either be of [n = S (pred n)] or [S (pred n) = n], for some [n]. These equations do not have syntactically equal sides. We can get to the point where they %\emph{%#<i>#do#</i>#%}% have equal sides by performing case analysis on [n]. Whenever we do so, the [n = 0] case will be contradictory, allowing us to discharge it by finding a free variable of type [fin 0] and performing inversion on it. In the [n = S n'] case, the sides of these equalities will simplify to equal values, as needed. The next two hints identify [n] values that are good candidates for such case analysis.
adamc@265 290
adamc@265 291 [[
adamc@265 292 | [ x : fin ?n |- _ ] =>
adamc@265 293 match goal with
adamc@265 294 | [ |- context[nzf x] ] =>
adamc@265 295 destruct n; [ inversion x | ]
adamc@265 296 end
adamc@265 297 | [ x : fin (pred ?n), y : fin ?n |- _ ] =>
adamc@265 298 match goal with
adamc@265 299 | [ |- context[nzf x] ] =>
adamc@265 300 destruct n; [ inversion y | ]
adamc@265 301 end
adamc@265 302
adamc@265 303 ]]
adamc@265 304
adamc@265 305 Finally, we find [match] discriminees of [option] type, enforcing that we do not destruct any discriminees that are themselves [match] expressions. Crucially, we do these case analyses with [case_eq] instead of [destruct]. The former adds equality hypotheses to record the relationships between old variables and their new deduced forms. These equalities will be used by our quantifier instantiation heuristic.
adamc@265 306
adamc@265 307 [[
adamc@265 308 | [ |- context[match ?E with None => _ | Some _ => _ end] ] =>
adamc@265 309 match E with
adamc@265 310 | match _ with None => _ | Some _ => _ end => fail 1
adamc@265 311 | _ => case_eq E; firstorder
adamc@265 312 end
adamc@265 313
adamc@265 314 ]]
adamc@265 315
adamc@265 316 Each iteration of the loop ends by calling [simp] again, and, after no more progress can be made, we finish by calling [eauto].
adamc@265 317
adamc@265 318 [[
adamc@265 319 end; simp); eauto.
adamc@265 320
adam@302 321 ]]
adam@302 322 *)
adamc@265 323
adamc@265 324
adamc@265 325 (** * Theorems *)
adamc@265 326
adamc@265 327 (** We are now ready to prove our main theorem, by way of a progression of lemmas.
adamc@265 328
adamc@265 329 The first pair of lemmas characterizes the interaction of substitution and lifting at the variable level. *)
adamc@265 330
adamc@265 331 Lemma substVar_unliftVar : forall n (f0 : fin n) f g,
adamc@265 332 match substVar f0 f, substVar (liftVar f0 g) f with
adamc@265 333 | Some f1, Some f2 => exists f', substVar g f1 = Some f'
adamc@265 334 /\ substVar (unliftVar f0 g) f2 = Some f'
adamc@265 335 | Some f1, None => substVar g f1 = None
adamc@265 336 | None, Some f2 => substVar (unliftVar f0 g) f2 = None
adamc@265 337 | None, None => False
adamc@265 338 end.
adamc@265 339 induction f0; dester.
adamc@265 340 Qed.
adamc@265 341
adamc@265 342 Lemma substVar_liftVar : forall n (f0 : fin n) f,
adamc@265 343 substVar f0 (liftVar f0 f) = Some f.
adamc@265 344 induction f0; dester.
adamc@265 345 Qed.
adamc@265 346
adamc@265 347 (** Next, we define a notion of %``%#"#greater-than-or-equal#"#%''% for [fin] values, prove an inversion theorem for it, and add that theorem as a hint. *)
adamc@265 348
adamc@265 349 Inductive fin_ge : forall n1, fin n1 -> forall n2, fin n2 -> Prop :=
adamc@265 350 | GeO : forall n1 (f1 : fin n1) n2,
adamc@265 351 fin_ge f1 (First : fin (S n2))
adamc@265 352 | GeS : forall n1 (f1 : fin n1) n2 (f2 : fin n2),
adamc@265 353 fin_ge f1 f2
adamc@265 354 -> fin_ge (Next f1) (Next f2).
adamc@265 355
adamc@265 356 Hint Constructors fin_ge.
adamc@265 357
adamc@265 358 Lemma fin_ge_inv' : forall n1 n2 (f1 : fin n1) (f2 : fin n2),
adamc@265 359 fin_ge f1 f2
adamc@265 360 -> match f1, f2 with
adamc@265 361 | Next _ f1', Next _ f2' => fin_ge f1' f2'
adamc@265 362 | _, _ => True
adamc@265 363 end.
adamc@265 364 destruct 1; dester.
adamc@265 365 Qed.
adamc@265 366
adamc@265 367 Lemma fin_ge_inv : forall n1 n2 (f1 : fin n1) (f2 : fin n2),
adamc@265 368 fin_ge (Next f1) (Next f2)
adamc@265 369 -> fin_ge f1 f2.
adamc@265 370 intros; generalize (fin_ge_inv' (f1 := Next f1) (f2 := Next f2)); dester.
adamc@265 371 Qed.
adamc@265 372
adamc@265 373 Hint Resolve fin_ge_inv.
adamc@265 374
adamc@265 375 (** A congruence lemma for the [fin] constructor [Next] is similarly useful. *)
adamc@265 376
adamc@265 377 Lemma Next_cong : forall n (f1 f2 : fin n),
adamc@265 378 f1 = f2
adamc@265 379 -> Next f1 = Next f2.
adamc@265 380 dester.
adamc@265 381 Qed.
adamc@265 382
adamc@265 383 Hint Resolve Next_cong.
adamc@265 384
adamc@265 385 (** We prove a crucial lemma about [liftVar] in terms of [fin_ge]. *)
adamc@265 386
adamc@265 387 Lemma liftVar_more : forall n (f : fin n) (f0 : fin (S n)) g,
adamc@265 388 fin_ge g f0
adamc@265 389 -> match liftVar f0 f in fin n'
adamc@265 390 return fin n' -> (fin (pred n') -> fin n') -> fin (S n') with
adamc@265 391 | First n0 => fun _ _ => First
adamc@265 392 | Next n0 y' => fun _ fx' => Next (fx' y')
adamc@265 393 end g (liftVar g) = liftVar (more f0) (liftVar g f).
adamc@265 394 induction f; inversion 1; dester.
adamc@265 395 Qed.
adamc@265 396
adamc@265 397 Hint Resolve liftVar_more.
adamc@265 398
adamc@265 399 (** We suggest a particular way of changing the form of a goal, so that other hints are able to match. *)
adamc@265 400
adamc@265 401 Hint Extern 1 (_ = lift _ (Next (more ?f))) =>
adamc@265 402 change (Next (more f)) with (more (Next f)).
adamc@265 403
adamc@265 404 (** We suggest applying the [f_equal] tactic to simplify equalities over expressions. For instance, this would reduce a goal [App f1 x1 = App f2 x2] to two goals [f1 = f2] and [x1 = x2]. *)
adamc@265 405
adamc@265 406 Hint Extern 1 (eq (A := exp _) _ _) => f_equal.
adamc@265 407
adamc@265 408 (** Our consideration of lifting in isolation finishes with another hint lemma. The auxiliary lemma with a strengthened induction hypothesis is where we put [fin_ge] to use, and we do not need to mention that predicate again afteward. *)
adamc@265 409
adamc@265 410 Lemma double_lift' : forall n (e : exp n) f g,
adamc@265 411 fin_ge g f
adamc@265 412 -> lift (lift e f) (Next g) = lift (lift e g) (more f).
adamc@265 413 induction e; dester.
adamc@265 414 Qed.
adamc@265 415
adamc@265 416 Lemma double_lift : forall n (e : exp n) g,
adamc@265 417 lift (lift e First) (Next g) = lift (lift e g) First.
adamc@265 418 intros; apply double_lift'; dester.
adamc@265 419 Qed.
adamc@265 420
adamc@265 421 Hint Resolve double_lift.
adamc@265 422
adamc@265 423 (** Now we characterize the interaction of substitution and lifting on variables. We start with a more general form [substVar_lift'] of the final lemma [substVar_lift], with the latter proved as a direct corollary of the former. *)
adamc@265 424
adamc@265 425 Lemma substVar_lift' : forall n (f0 : fin n) f g,
adamc@265 426 substVar [nzf f0 return n, fin (S n) for
adamc@265 427 liftVar (more g) [sym_eq (nzf f0) return n, fin n for f0]]
adamc@265 428 (liftVar (liftVar (Next f0) [nzf f0 return n, fin n for g]) f)
adamc@265 429 = match substVar f0 f with
adamc@265 430 | Some f'' => Some [nzf f0 return n, fin n for liftVar g f'']
adamc@265 431 | None => None
adamc@265 432 end.
adamc@265 433 induction f0; dester.
adamc@265 434 Qed.
adamc@265 435
adamc@265 436 Lemma substVar_lift : forall n (f0 f g : fin (S n)),
adamc@265 437 substVar (liftVar (more g) f0) (liftVar (liftVar (Next f0) g) f)
adamc@265 438 = match substVar f0 f with
adamc@265 439 | Some f'' => Some (liftVar g f'')
adamc@265 440 | None => None
adamc@265 441 end.
adamc@265 442 intros; generalize (substVar_lift' f0 f g); dester.
adamc@265 443 Qed.
adamc@265 444
adamc@265 445 (** We follow a similar decomposition for the expression-level theorem about substitution and lifting. *)
adamc@265 446
adamc@265 447 Lemma lift_subst' : forall n (e1 : exp n) f g e2,
adamc@265 448 lift (subst e1 f e2) g
adamc@265 449 = [sym_eq (nzf f) return n, exp n for
adamc@265 450 subst
adamc@265 451 (lift e1 (liftVar (Next f) [nzf f return n, fin n for g]))
adamc@265 452 [nzf f return n, fin (S n) for
adamc@265 453 liftVar (more g) [sym_eq (nzf f) return n, fin n for f]]
adamc@265 454 [nzf f return n, exp n for lift e2 g]].
adamc@265 455 induction e1; generalize substVar_lift; dester.
adamc@265 456 Qed.
adamc@265 457
adamc@265 458 Lemma lift_subst : forall n g (e2 : exp (S n)) e3,
adamc@265 459 subst (lift e2 First) (Next g) (lift e3 First) = lift (n := n) (subst e2 g e3) First.
adamc@265 460 intros; generalize (lift_subst' e2 g First e3); dester.
adamc@265 461 Qed.
adamc@265 462
adamc@265 463 Hint Resolve lift_subst.
adamc@265 464
adamc@265 465 (** Our last auxiliary lemma characterizes a situation where substitution can undo the effects of lifting. *)
adamc@265 466
adamc@265 467 Lemma undo_lift' : forall n (e1 : exp n) e2 f,
adamc@265 468 subst (lift e1 f) f e2 = e1.
adamc@265 469 induction e1; generalize substVar_liftVar; dester.
adamc@265 470 Qed.
adamc@265 471
adamc@265 472 Lemma undo_lift : forall n e2 e3 (f0 : fin (S (S n))) g,
adamc@265 473 e3 = subst (lift e3 (unliftVar f0 g)) (unliftVar f0 g)
adamc@265 474 (subst (n := S n) e2 g e3).
adamc@265 475 generalize undo_lift'; dester.
adamc@265 476 Qed.
adamc@265 477
adamc@265 478 Hint Resolve undo_lift.
adamc@265 479
adamc@265 480 (** Finally, we arrive at the substitution commutativity theorem. *)
adamc@265 481
adamc@265 482 Lemma subst_comm' : forall n (e1 : exp n) f g e2 e3,
adamc@265 483 subst (subst e1 f e2) g e3
adamc@265 484 = subst
adamc@265 485 (subst e1 (liftVar f g) [nzf g return n, exp n for
adamc@265 486 lift e3 [sym_eq (nzf g) return n, fin n for unliftVar f g]])
adamc@265 487 (unliftVar f g)
adamc@265 488 (subst e2 g e3).
adamc@265 489 induction e1; generalize (substVar_unliftVar (n := n)); dester.
adamc@265 490 Qed.
adamc@265 491
adamc@265 492 Theorem subst_comm : forall (e1 : exp 2) e2 e3,
adamc@265 493 subst (subst e1 First e2) First e3
adamc@265 494 = subst (subst e1 (Next First) (lift e3 First)) First (subst e2 First e3).
adamc@265 495 intros; generalize (subst_comm' e1 First First e2 e3); dester.
adamc@265 496 Qed.
adamc@265 497
adamc@265 498 (** The final theorem is specialized to the case of substituting in an expression with exactly two free variables, which yields a statement that is readable enough, as statements about de Bruijn indices go.
adamc@265 499
adamc@265 500 This proof script is resilient to specification changes. It is easy to add new constructors to the language being treated. The proofs adapt automatically to the addition of any constructor whose subterms each involve zero or one new bound variables. That is, to add such a constructor, we only need to add it to the definition of [exp] and add (quite obvious) cases for it in the definitions of [lift] and [subst]. *)