Mercurial > cpdt > repo

annotate src/DeBruijn.v @ 265:dce88a5c170c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import DeBruijn
author Adam Chlipala <adamc@hcoop.net>
date Wed, 30 Dec 2009 13:38:13 -0500
parents
children da9ccc6bf572
rev   line source
adamc@265 1 (* Copyright (c) 2009, 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
adamc@265 15 Require Import DepList Tactics.
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
adamc@265 153 (** Less than a page of tactic code will be sufficient to automate our proof of commuativity. 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
adamc@265 321 ]] *)
adamc@265 322
adamc@265 323
adamc@265 324 (** * Theorems *)
adamc@265 325
adamc@265 326 (** We are now ready to prove our main theorem, by way of a progression of lemmas.
adamc@265 327
adamc@265 328 The first pair of lemmas characterizes the interaction of substitution and lifting at the variable level. *)
adamc@265 329
adamc@265 330 Lemma substVar_unliftVar : forall n (f0 : fin n) f g,
adamc@265 331 match substVar f0 f, substVar (liftVar f0 g) f with
adamc@265 332 | Some f1, Some f2 => exists f', substVar g f1 = Some f'
adamc@265 333 /\ substVar (unliftVar f0 g) f2 = Some f'
adamc@265 334 | Some f1, None => substVar g f1 = None
adamc@265 335 | None, Some f2 => substVar (unliftVar f0 g) f2 = None
adamc@265 336 | None, None => False
adamc@265 337 end.
adamc@265 338 induction f0; dester.
adamc@265 339 Qed.
adamc@265 340
adamc@265 341 Lemma substVar_liftVar : forall n (f0 : fin n) f,
adamc@265 342 substVar f0 (liftVar f0 f) = Some f.
adamc@265 343 induction f0; dester.
adamc@265 344 Qed.
adamc@265 345
adamc@265 346 (** 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 347
adamc@265 348 Inductive fin_ge : forall n1, fin n1 -> forall n2, fin n2 -> Prop :=
adamc@265 349 | GeO : forall n1 (f1 : fin n1) n2,
adamc@265 350 fin_ge f1 (First : fin (S n2))
adamc@265 351 | GeS : forall n1 (f1 : fin n1) n2 (f2 : fin n2),
adamc@265 352 fin_ge f1 f2
adamc@265 353 -> fin_ge (Next f1) (Next f2).
adamc@265 354
adamc@265 355 Hint Constructors fin_ge.
adamc@265 356
adamc@265 357 Lemma fin_ge_inv' : forall n1 n2 (f1 : fin n1) (f2 : fin n2),
adamc@265 358 fin_ge f1 f2
adamc@265 359 -> match f1, f2 with
adamc@265 360 | Next _ f1', Next _ f2' => fin_ge f1' f2'
adamc@265 361 | _, _ => True
adamc@265 362 end.
adamc@265 363 destruct 1; dester.
adamc@265 364 Qed.
adamc@265 365
adamc@265 366 Lemma fin_ge_inv : forall n1 n2 (f1 : fin n1) (f2 : fin n2),
adamc@265 367 fin_ge (Next f1) (Next f2)
adamc@265 368 -> fin_ge f1 f2.
adamc@265 369 intros; generalize (fin_ge_inv' (f1 := Next f1) (f2 := Next f2)); dester.
adamc@265 370 Qed.
adamc@265 371
adamc@265 372 Hint Resolve fin_ge_inv.
adamc@265 373
adamc@265 374 (** A congruence lemma for the [fin] constructor [Next] is similarly useful. *)
adamc@265 375
adamc@265 376 Lemma Next_cong : forall n (f1 f2 : fin n),
adamc@265 377 f1 = f2
adamc@265 378 -> Next f1 = Next f2.
adamc@265 379 dester.
adamc@265 380 Qed.
adamc@265 381
adamc@265 382 Hint Resolve Next_cong.
adamc@265 383
adamc@265 384 (** We prove a crucial lemma about [liftVar] in terms of [fin_ge]. *)
adamc@265 385
adamc@265 386 Lemma liftVar_more : forall n (f : fin n) (f0 : fin (S n)) g,
adamc@265 387 fin_ge g f0
adamc@265 388 -> match liftVar f0 f in fin n'
adamc@265 389 return fin n' -> (fin (pred n') -> fin n') -> fin (S n') with
adamc@265 390 | First n0 => fun _ _ => First
adamc@265 391 | Next n0 y' => fun _ fx' => Next (fx' y')
adamc@265 392 end g (liftVar g) = liftVar (more f0) (liftVar g f).
adamc@265 393 induction f; inversion 1; dester.
adamc@265 394 Qed.
adamc@265 395
adamc@265 396 Hint Resolve liftVar_more.
adamc@265 397
adamc@265 398 (** We suggest a particular way of changing the form of a goal, so that other hints are able to match. *)
adamc@265 399
adamc@265 400 Hint Extern 1 (_ = lift _ (Next (more ?f))) =>
adamc@265 401 change (Next (more f)) with (more (Next f)).
adamc@265 402
adamc@265 403 (** 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 404
adamc@265 405 Hint Extern 1 (eq (A := exp _) _ _) => f_equal.
adamc@265 406
adamc@265 407 (** 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 408
adamc@265 409 Lemma double_lift' : forall n (e : exp n) f g,
adamc@265 410 fin_ge g f
adamc@265 411 -> lift (lift e f) (Next g) = lift (lift e g) (more f).
adamc@265 412 induction e; dester.
adamc@265 413 Qed.
adamc@265 414
adamc@265 415 Lemma double_lift : forall n (e : exp n) g,
adamc@265 416 lift (lift e First) (Next g) = lift (lift e g) First.
adamc@265 417 intros; apply double_lift'; dester.
adamc@265 418 Qed.
adamc@265 419
adamc@265 420 Hint Resolve double_lift.
adamc@265 421
adamc@265 422 (** 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 423
adamc@265 424 Lemma substVar_lift' : forall n (f0 : fin n) f g,
adamc@265 425 substVar [nzf f0 return n, fin (S n) for
adamc@265 426 liftVar (more g) [sym_eq (nzf f0) return n, fin n for f0]]
adamc@265 427 (liftVar (liftVar (Next f0) [nzf f0 return n, fin n for g]) f)
adamc@265 428 = match substVar f0 f with
adamc@265 429 | Some f'' => Some [nzf f0 return n, fin n for liftVar g f'']
adamc@265 430 | None => None
adamc@265 431 end.
adamc@265 432 induction f0; dester.
adamc@265 433 Qed.
adamc@265 434
adamc@265 435 Lemma substVar_lift : forall n (f0 f g : fin (S n)),
adamc@265 436 substVar (liftVar (more g) f0) (liftVar (liftVar (Next f0) g) f)
adamc@265 437 = match substVar f0 f with
adamc@265 438 | Some f'' => Some (liftVar g f'')
adamc@265 439 | None => None
adamc@265 440 end.
adamc@265 441 intros; generalize (substVar_lift' f0 f g); dester.
adamc@265 442 Qed.
adamc@265 443
adamc@265 444 (** We follow a similar decomposition for the expression-level theorem about substitution and lifting. *)
adamc@265 445
adamc@265 446 Lemma lift_subst' : forall n (e1 : exp n) f g e2,
adamc@265 447 lift (subst e1 f e2) g
adamc@265 448 = [sym_eq (nzf f) return n, exp n for
adamc@265 449 subst
adamc@265 450 (lift e1 (liftVar (Next f) [nzf f return n, fin n for g]))
adamc@265 451 [nzf f return n, fin (S n) for
adamc@265 452 liftVar (more g) [sym_eq (nzf f) return n, fin n for f]]
adamc@265 453 [nzf f return n, exp n for lift e2 g]].
adamc@265 454 induction e1; generalize substVar_lift; dester.
adamc@265 455 Qed.
adamc@265 456
adamc@265 457 Lemma lift_subst : forall n g (e2 : exp (S n)) e3,
adamc@265 458 subst (lift e2 First) (Next g) (lift e3 First) = lift (n := n) (subst e2 g e3) First.
adamc@265 459 intros; generalize (lift_subst' e2 g First e3); dester.
adamc@265 460 Qed.
adamc@265 461
adamc@265 462 Hint Resolve lift_subst.
adamc@265 463
adamc@265 464 (** Our last auxiliary lemma characterizes a situation where substitution can undo the effects of lifting. *)
adamc@265 465
adamc@265 466 Lemma undo_lift' : forall n (e1 : exp n) e2 f,
adamc@265 467 subst (lift e1 f) f e2 = e1.
adamc@265 468 induction e1; generalize substVar_liftVar; dester.
adamc@265 469 Qed.
adamc@265 470
adamc@265 471 Lemma undo_lift : forall n e2 e3 (f0 : fin (S (S n))) g,
adamc@265 472 e3 = subst (lift e3 (unliftVar f0 g)) (unliftVar f0 g)
adamc@265 473 (subst (n := S n) e2 g e3).
adamc@265 474 generalize undo_lift'; dester.
adamc@265 475 Qed.
adamc@265 476
adamc@265 477 Hint Resolve undo_lift.
adamc@265 478
adamc@265 479 (** Finally, we arrive at the substitution commutativity theorem. *)
adamc@265 480
adamc@265 481 Lemma subst_comm' : forall n (e1 : exp n) f g e2 e3,
adamc@265 482 subst (subst e1 f e2) g e3
adamc@265 483 = subst
adamc@265 484 (subst e1 (liftVar f g) [nzf g return n, exp n for
adamc@265 485 lift e3 [sym_eq (nzf g) return n, fin n for unliftVar f g]])
adamc@265 486 (unliftVar f g)
adamc@265 487 (subst e2 g e3).
adamc@265 488 induction e1; generalize (substVar_unliftVar (n := n)); dester.
adamc@265 489 Qed.
adamc@265 490
adamc@265 491 Theorem subst_comm : forall (e1 : exp 2) e2 e3,
adamc@265 492 subst (subst e1 First e2) First e3
adamc@265 493 = subst (subst e1 (Next First) (lift e3 First)) First (subst e2 First e3).
adamc@265 494 intros; generalize (subst_comm' e1 First First e2 e3); dester.
adamc@265 495 Qed.
adamc@265 496
adamc@265 497 (** 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 498
adamc@265 499 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]. *)