Mercurial > cpdt > repo

annotate src/Reflection.v @ 439:393b8ed99c2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of improvements to vertical spacing, up through end of InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 13:21:36 -0400
parents 8077352044b2
children 0650420c127b
rev   line source
adam@379 1 (* Copyright (c) 2008-2012, Adam Chlipala
adamc@142 2 *
adamc@142 3 * This work is licensed under a
adamc@142 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@142 5 * Unported License.
adamc@142 6 * The license text is available at:
adamc@142 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@142 8 *)
adamc@142 9
adamc@142 10 (* begin hide *)
adamc@142 11 Require Import List.
adamc@142 12
adam@314 13 Require Import CpdtTactics MoreSpecif.
adamc@142 14
adamc@142 15 Set Implicit Arguments.
adamc@142 16 (* end hide *)
adamc@142 17
adamc@142 18
adamc@142 19 (** %\chapter{Proof by Reflection}% *)
adamc@142 20
adam@412 21 (** The last chapter highlighted a very heuristic approach to proving. In this chapter, we will study an alternative technique,%\index{proof by reflection}% _proof by reflection_ %\cite{reflection}%. We will write, in Gallina, decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs. Such a proof is checked by running the decision procedure. The term _reflection_ applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them, and translating such a term back to the original form is called _reflecting_ it. *)
adamc@142 22
adamc@142 23
adamc@142 24 (** * Proving Evenness *)
adamc@142 25
adamc@142 26 (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *)
adamc@142 27
adamc@142 28 Inductive isEven : nat -> Prop :=
adamc@144 29 | Even_O : isEven O
adamc@144 30 | Even_SS : forall n, isEven n -> isEven (S (S n)).
adamc@142 31
adamc@148 32 (* begin thide *)
adamc@142 33 Ltac prove_even := repeat constructor.
adamc@148 34 (* end thide *)
adamc@142 35
adamc@142 36 Theorem even_256 : isEven 256.
adamc@142 37 prove_even.
adamc@142 38 Qed.
adamc@142 39
adamc@142 40 Print even_256.
adamc@221 41 (** %\vspace{-.15in}% [[
adamc@142 42 even_256 =
adamc@142 43 Even_SS
adamc@142 44 (Even_SS
adamc@142 45 (Even_SS
adamc@142 46 (Even_SS
adamc@221 47
adamc@142 48 ]]
adamc@142 49
adam@360 50 %\noindent%...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length super-linear in the input value. Coq's implicit arguments mechanism is hiding the values given for parameter [n] of [Even_SS], which is why the proof term only appears linear here. Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent. Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough.
adam@360 51
adam@360 52 Superlinear evenness proof terms seem like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed.
adamc@142 53
adamc@142 54 It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.
adamc@142 55
adamc@142 56 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
adamc@142 57
adamc@221 58 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
adamc@142 59
adam@432 60 (* begin hide *)
adam@437 61 (* begin thide *)
adam@432 62 Definition paartial := partial.
adam@437 63 (* end thide *)
adam@432 64 (* end hide *)
adam@432 65
adamc@142 66 Print partial.
adamc@221 67 (** %\vspace{-.15in}% [[
adamc@221 68 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
adamc@221 69
adamc@221 70 ]]
adamc@142 71
adamc@221 72 A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
adamc@142 73
adamc@221 74 Local Open Scope partial_scope.
adamc@142 75
adamc@142 76 (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
adamc@142 77
adamc@148 78 (* begin thide *)
adam@297 79 Definition check_even : forall n : nat, [isEven n].
adamc@142 80 Hint Constructors isEven.
adamc@142 81
adamc@142 82 refine (fix F (n : nat) : [isEven n] :=
adamc@221 83 match n with
adamc@142 84 | 0 => Yes
adamc@142 85 | 1 => No
adamc@142 86 | S (S n') => Reduce (F n')
adamc@142 87 end); auto.
adamc@142 88 Defined.
adamc@142 89
adam@398 90 (** The function [check_even] may be viewed as a _verified decision procedure_, because its type guarantees that it never returns [Yes] for inputs that are not even.
adam@360 91
adam@360 92 Now we can use dependent pattern-matching to write a function that performs a surprising feat. When given a [partial P], this function [partialOut] returns a proof of [P] if the [partial] value contains a proof, and it returns a (useless) proof of [True] otherwise. From the standpoint of ML and Haskell programming, it seems impossible to write such a type, but it is trivial with a [return] annotation. *)
adamc@142 93
adamc@142 94 Definition partialOut (P : Prop) (x : [P]) :=
adamc@142 95 match x return (match x with
adamc@142 96 | Proved _ => P
adamc@142 97 | Uncertain => True
adamc@142 98 end) with
adamc@142 99 | Proved pf => pf
adamc@142 100 | Uncertain => I
adamc@142 101 end.
adamc@142 102
adam@289 103 (** It may seem strange to define a function like this. However, it turns out to be very useful in writing a reflective version of our earlier [prove_even] tactic: *)
adamc@142 104
adamc@142 105 Ltac prove_even_reflective :=
adamc@142 106 match goal with
adamc@142 107 | [ |- isEven ?N] => exact (partialOut (check_even N))
adamc@142 108 end.
adamc@148 109 (* end thide *)
adamc@142 110
adam@432 111 (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. Recall that the %\index{tactics!exact}%[exact] tactic proves a proposition [P] when given a proof term of precisely type [P]. *)
adamc@142 112
adamc@142 113 Theorem even_256' : isEven 256.
adamc@142 114 prove_even_reflective.
adamc@142 115 Qed.
adamc@142 116
adamc@142 117 Print even_256'.
adamc@221 118 (** %\vspace{-.15in}% [[
adamc@142 119 even_256' = partialOut (check_even 256)
adamc@142 120 : isEven 256
adamc@142 121 ]]
adamc@142 122
adam@289 123 We can see a constant wrapper around the object of the proof. For any even number, this form of proof will suffice. The size of the proof term is now linear in the number being checked, containing two repetitions of the unary form of that number, one of which is hidden above within the implicit argument to [partialOut].
adam@289 124
adam@289 125 What happens if we try the tactic with an odd number? *)
adamc@142 126
adamc@142 127 Theorem even_255 : isEven 255.
adam@360 128 (** %\vspace{-.275in}%[[
adamc@142 129 prove_even_reflective.
adam@360 130 ]]
adamc@142 131
adam@360 132 <<
adamc@142 133 User error: No matching clauses for match goal
adam@360 134 >>
adamc@142 135
adamc@142 136 Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the [match].
adamc@142 137
adam@360 138 %\vspace{-.15in}%[[
adamc@142 139 exact (partialOut (check_even 255)).
adam@360 140 ]]
adamc@142 141
adam@360 142 <<
adamc@142 143 Error: The term "partialOut (check_even 255)" has type
adamc@142 144 "match check_even 255 with
adamc@142 145 | Yes => isEven 255
adamc@142 146 | No => True
adamc@142 147 end" while it is expected to have type "isEven 255"
adam@360 148 >>
adamc@142 149
adam@360 150 As usual, the type checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
adamc@221 151
adamc@142 152 Abort.
adamc@143 153
adam@362 154 (** Our tactic [prove_even_reflective] is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of [check_even]. *)
adamc@143 155
adam@360 156
adam@360 157 (** * Reifying the Syntax of a Trivial Tautology Language *)
adamc@143 158
adamc@143 159 (** We might also like to have reflective proofs of trivial tautologies like this one: *)
adamc@143 160
adamc@143 161 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143 162 tauto.
adamc@143 163 Qed.
adamc@143 164
adam@432 165 (* begin hide *)
adam@437 166 (* begin thide *)
adam@432 167 Definition tg := (and_ind, or_introl).
adam@437 168 (* end thide *)
adam@432 169 (* end hide *)
adam@432 170
adamc@143 171 Print true_galore.
adamc@221 172 (** %\vspace{-.15in}% [[
adamc@143 173 true_galore =
adamc@143 174 fun H : True /\ True =>
adamc@143 175 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
adamc@143 176 : True /\ True -> True \/ True /\ (True -> True)
adamc@221 177
adamc@143 178 ]]
adamc@143 179
adamc@143 180 As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules. For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
adamc@143 181
adam@432 182 To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection." It is impossible to case-analyze a [Prop] in any way in Gallina. We must%\index{reification}% _reify_ [Prop] into some type that we _can_ analyze. This inductive type is a good candidate: *)
adamc@143 183
adamc@148 184 (* begin thide *)
adamc@143 185 Inductive taut : Set :=
adamc@143 186 | TautTrue : taut
adamc@143 187 | TautAnd : taut -> taut -> taut
adamc@143 188 | TautOr : taut -> taut -> taut
adamc@143 189 | TautImp : taut -> taut -> taut.
adamc@143 190
adam@432 191 (** We write a recursive function to _reflect_ this syntax back to [Prop]. Such functions are also called%\index{interpretation function}% _interpretation functions_, and we have used them in previous examples to give semantics to small programming languages. *)
adamc@143 192
adamc@143 193 Fixpoint tautDenote (t : taut) : Prop :=
adamc@143 194 match t with
adamc@143 195 | TautTrue => True
adamc@143 196 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
adamc@143 197 | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
adamc@143 198 | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
adamc@143 199 end.
adamc@143 200
adamc@143 201 (** It is easy to prove that every formula in the range of [tautDenote] is true. *)
adamc@143 202
adamc@143 203 Theorem tautTrue : forall t, tautDenote t.
adamc@143 204 induction t; crush.
adamc@143 205 Qed.
adamc@143 206
adam@360 207 (** To use [tautTrue] to prove particular formulas, we need to implement the syntax reification process. A recursive Ltac function does the job. *)
adamc@143 208
adam@360 209 Ltac tautReify P :=
adamc@143 210 match P with
adamc@143 211 | True => TautTrue
adamc@143 212 | ?P1 /\ ?P2 =>
adam@360 213 let t1 := tautReify P1 in
adam@360 214 let t2 := tautReify P2 in
adamc@143 215 constr:(TautAnd t1 t2)
adamc@143 216 | ?P1 \/ ?P2 =>
adam@360 217 let t1 := tautReify P1 in
adam@360 218 let t2 := tautReify P2 in
adamc@143 219 constr:(TautOr t1 t2)
adamc@143 220 | ?P1 -> ?P2 =>
adam@360 221 let t1 := tautReify P1 in
adam@360 222 let t2 := tautReify P2 in
adamc@143 223 constr:(TautImp t1 t2)
adamc@143 224 end.
adamc@143 225
adam@360 226 (** With [tautReify] available, it is easy to finish our reflective tactic. We look at the goal formula, reflect it, and apply [tautTrue] to the reflected formula. *)
adamc@143 227
adamc@143 228 Ltac obvious :=
adamc@143 229 match goal with
adamc@143 230 | [ |- ?P ] =>
adam@360 231 let t := tautReify P in
adamc@143 232 exact (tautTrue t)
adamc@143 233 end.
adamc@143 234
adamc@143 235 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)
adamc@148 236 (* end thide *)
adamc@143 237
adamc@143 238 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143 239 obvious.
adamc@143 240 Qed.
adamc@143 241
adamc@143 242 Print true_galore'.
adamc@143 243
adamc@221 244 (** %\vspace{-.15in}% [[
adamc@143 245 true_galore' =
adamc@143 246 tautTrue
adamc@143 247 (TautImp (TautAnd TautTrue TautTrue)
adamc@143 248 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
adamc@143 249 : True /\ True -> True \/ True /\ (True -> True)
adamc@143 250 ]]
adamc@143 251
adam@432 252 It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reification process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here _is_ on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This is all in addition to the proof-size improvement that we have already seen.
adam@360 253
adam@360 254 It may also be worth pointing out that our previous example of evenness testing used a function [partialOut] for sound handling of input goals that the verified decision procedure fails to prove. Here, we prove that our procedure [tautTrue] (recall that an inductive proof may be viewed as a recursive procedure) is able to prove any goal representable in [taut], so no extra step is necessary. *)
adamc@144 255
adamc@144 256
adamc@145 257 (** * A Monoid Expression Simplifier *)
adamc@145 258
adam@432 259 (** Proof by reflection does not require encoding of all of the syntax in a goal. We can insert "variables" in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them. In this section, we explore that possibility by writing a tactic for normalizing monoid equations. *)
adamc@146 260
adamc@145 261 Section monoid.
adamc@145 262 Variable A : Set.
adamc@145 263 Variable e : A.
adamc@145 264 Variable f : A -> A -> A.
adamc@145 265
adamc@145 266 Infix "+" := f.
adamc@145 267
adamc@145 268 Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
adamc@145 269 Hypothesis identl : forall a, e + a = a.
adamc@145 270 Hypothesis identr : forall a, a + e = a.
adamc@145 271
adamc@146 272 (** We add variables and hypotheses characterizing an arbitrary instance of the algebraic structure of monoids. We have an associative binary operator and an identity element for it.
adamc@146 273
adam@432 274 It is easy to define an expression tree type for monoid expressions. A [Var] constructor is a "catch-all" case for subexpressions that we cannot model. These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand. *)
adamc@146 275
adamc@148 276 (* begin thide *)
adamc@145 277 Inductive mexp : Set :=
adamc@145 278 | Ident : mexp
adamc@145 279 | Var : A -> mexp
adamc@145 280 | Op : mexp -> mexp -> mexp.
adamc@145 281
adam@360 282 (** Next, we write an interpretation function. *)
adamc@146 283
adamc@145 284 Fixpoint mdenote (me : mexp) : A :=
adamc@145 285 match me with
adamc@145 286 | Ident => e
adamc@145 287 | Var v => v
adamc@145 288 | Op me1 me2 => mdenote me1 + mdenote me2
adamc@145 289 end.
adamc@145 290
adamc@146 291 (** We will normalize expressions by flattening them into lists, via associativity, so it is helpful to have a denotation function for lists of monoid values. *)
adamc@146 292
adamc@145 293 Fixpoint mldenote (ls : list A) : A :=
adamc@145 294 match ls with
adamc@145 295 | nil => e
adamc@145 296 | x :: ls' => x + mldenote ls'
adamc@145 297 end.
adamc@145 298
adamc@146 299 (** The flattening function itself is easy to implement. *)
adamc@146 300
adamc@145 301 Fixpoint flatten (me : mexp) : list A :=
adamc@145 302 match me with
adamc@145 303 | Ident => nil
adamc@145 304 | Var x => x :: nil
adamc@145 305 | Op me1 me2 => flatten me1 ++ flatten me2
adamc@145 306 end.
adamc@145 307
adamc@146 308 (** [flatten] has a straightforward correctness proof in terms of our [denote] functions. *)
adamc@146 309
adamc@146 310 Lemma flatten_correct' : forall ml2 ml1,
adamc@146 311 mldenote ml1 + mldenote ml2 = mldenote (ml1 ++ ml2).
adamc@145 312 induction ml1; crush.
adamc@145 313 Qed.
adamc@145 314
adamc@145 315 Theorem flatten_correct : forall me, mdenote me = mldenote (flatten me).
adamc@145 316 Hint Resolve flatten_correct'.
adamc@145 317
adamc@145 318 induction me; crush.
adamc@145 319 Qed.
adamc@145 320
adamc@146 321 (** Now it is easy to prove a theorem that will be the main tool behind our simplification tactic. *)
adamc@146 322
adamc@146 323 Theorem monoid_reflect : forall me1 me2,
adamc@146 324 mldenote (flatten me1) = mldenote (flatten me2)
adamc@146 325 -> mdenote me1 = mdenote me2.
adamc@145 326 intros; repeat rewrite flatten_correct; assumption.
adamc@145 327 Qed.
adamc@145 328
adam@360 329 (** We implement reification into the [mexp] type. *)
adamc@146 330
adam@360 331 Ltac reify me :=
adamc@146 332 match me with
adamc@145 333 | e => Ident
adamc@146 334 | ?me1 + ?me2 =>
adam@360 335 let r1 := reify me1 in
adam@360 336 let r2 := reify me2 in
adamc@145 337 constr:(Op r1 r2)
adamc@146 338 | _ => constr:(Var me)
adamc@145 339 end.
adamc@145 340
adam@360 341 (** The final [monoid] tactic works on goals that equate two monoid terms. We reify each and change the goal to refer to the reified versions, finishing off by applying [monoid_reflect] and simplifying uses of [mldenote]. Recall that the %\index{tactics!change}%[change] tactic replaces a conclusion formula with another that is definitionally equal to it. *)
adamc@146 342
adamc@145 343 Ltac monoid :=
adamc@145 344 match goal with
adamc@146 345 | [ |- ?me1 = ?me2 ] =>
adam@360 346 let r1 := reify me1 in
adam@360 347 let r2 := reify me2 in
adamc@145 348 change (mdenote r1 = mdenote r2);
adam@360 349 apply monoid_reflect; simpl
adamc@145 350 end.
adamc@145 351
adamc@146 352 (** We can make short work of theorems like this one: *)
adamc@146 353
adamc@148 354 (* end thide *)
adamc@148 355
adamc@145 356 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
adamc@146 357 intros; monoid.
adamc@146 358 (** [[
adamc@146 359 ============================
adamc@146 360 a + (b + (c + (d + e))) = a + (b + (c + (d + e)))
adamc@221 361
adamc@146 362 ]]
adamc@146 363
adam@360 364 Our tactic has canonicalized both sides of the equality, such that we can finish the proof by reflexivity. *)
adamc@146 365
adamc@145 366 reflexivity.
adamc@145 367 Qed.
adamc@146 368
adamc@146 369 (** It is interesting to look at the form of the proof. *)
adamc@146 370
adamc@146 371 Print t1.
adamc@221 372 (** %\vspace{-.15in}% [[
adamc@146 373 t1 =
adamc@146 374 fun a b c d : A =>
adamc@146 375 monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d))
adamc@146 376 (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
adam@426 377 (eq_refl (a + (b + (c + (d + e)))))
adamc@146 378 : forall a b c d : A, a + b + c + d = a + (b + c) + d
adamc@146 379 ]]
adamc@146 380
adam@360 381 The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form. *)
adamc@221 382
adamc@145 383 End monoid.
adamc@145 384
adam@360 385 (** Extensions of this basic approach are used in the implementations of the %\index{tactics!ring}%[ring] and %\index{tactics!field}%[field] tactics that come packaged with Coq. *)
adamc@146 386
adamc@145 387
adamc@144 388 (** * A Smarter Tautology Solver *)
adamc@144 389
adam@412 390 (** Now we are ready to revisit our earlier tautology solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality.
adamc@147 391
adam@360 392 To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library. *)
adamc@147 393
adamc@144 394 Require Import Quote.
adamc@144 395
adamc@148 396 (* begin thide *)
adamc@144 397 Inductive formula : Set :=
adamc@144 398 | Atomic : index -> formula
adamc@144 399 | Truth : formula
adamc@144 400 | Falsehood : formula
adamc@144 401 | And : formula -> formula -> formula
adamc@144 402 | Or : formula -> formula -> formula
adamc@144 403 | Imp : formula -> formula -> formula.
adam@362 404 (* end thide *)
adamc@144 405
adam@360 406 (** The type %\index{Gallina terms!index}%[index] comes from the [Quote] library and represents a countable variable type. The rest of [formula]'s definition should be old hat by now.
adamc@147 407
adamc@147 408 The [quote] tactic will implement injection from [Prop] into [formula] for us, but it is not quite as smart as we might like. In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter. *)
adamc@144 409
adamc@144 410 Definition imp (P1 P2 : Prop) := P1 -> P2.
adamc@144 411 Infix "-->" := imp (no associativity, at level 95).
adamc@144 412
adamc@147 413 (** Now we can define our denotation function. *)
adamc@147 414
adamc@147 415 Definition asgn := varmap Prop.
adamc@147 416
adam@362 417 (* begin thide *)
adamc@144 418 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
adamc@144 419 match f with
adamc@144 420 | Atomic v => varmap_find False v atomics
adamc@144 421 | Truth => True
adamc@144 422 | Falsehood => False
adamc@144 423 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
adamc@144 424 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
adamc@144 425 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2
adamc@144 426 end.
adam@362 427 (* end thide *)
adamc@144 428
adam@360 429 (** The %\index{Gallina terms!varmap}%[varmap] type family implements maps from [index] values. In this case, we define an assignment as a map from variables to [Prop]s. Our reifier [formulaDenote] works with an assignment, and we use the [varmap_find] function to consult the assignment in the [Atomic] case. The first argument to [varmap_find] is a default value, in case the variable is not found. *)
adamc@147 430
adamc@144 431 Section my_tauto.
adamc@144 432 Variable atomics : asgn.
adamc@144 433
adamc@144 434 Definition holds (v : index) := varmap_find False v atomics.
adamc@144 435
adamc@147 436 (** We define some shorthand for a particular variable being true, and now we are ready to define some helpful functions based on the [ListSet] module of the standard library, which (unsurprisingly) presents a view of lists as sets. *)
adamc@147 437
adamc@144 438 Require Import ListSet.
adamc@144 439
adamc@144 440 Definition index_eq : forall x y : index, {x = y} + {x <> y}.
adamc@144 441 decide equality.
adamc@144 442 Defined.
adamc@144 443
adamc@144 444 Definition add (s : set index) (v : index) := set_add index_eq v s.
adamc@147 445
adamc@221 446 Definition In_dec : forall v (s : set index), {In v s} + {~ In v s}.
adamc@221 447 Local Open Scope specif_scope.
adamc@144 448
adamc@221 449 intro; refine (fix F (s : set index) : {In v s} + {~ In v s} :=
adamc@221 450 match s with
adamc@144 451 | nil => No
adamc@144 452 | v' :: s' => index_eq v' v || F s'
adamc@144 453 end); crush.
adamc@144 454 Defined.
adamc@144 455
adamc@147 456 (** We define what it means for all members of an index set to represent true propositions, and we prove some lemmas about this notion. *)
adamc@147 457
adamc@144 458 Fixpoint allTrue (s : set index) : Prop :=
adamc@144 459 match s with
adamc@144 460 | nil => True
adamc@144 461 | v :: s' => holds v /\ allTrue s'
adamc@144 462 end.
adamc@144 463
adamc@144 464 Theorem allTrue_add : forall v s,
adamc@144 465 allTrue s
adamc@144 466 -> holds v
adamc@144 467 -> allTrue (add s v).
adamc@144 468 induction s; crush;
adamc@144 469 match goal with
adamc@144 470 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@144 471 end; crush.
adamc@144 472 Qed.
adamc@144 473
adamc@144 474 Theorem allTrue_In : forall v s,
adamc@144 475 allTrue s
adamc@144 476 -> set_In v s
adamc@144 477 -> varmap_find False v atomics.
adamc@144 478 induction s; crush.
adamc@144 479 Qed.
adamc@144 480
adamc@144 481 Hint Resolve allTrue_add allTrue_In.
adamc@144 482
adamc@221 483 Local Open Scope partial_scope.
adamc@144 484
adam@353 485 (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, guaranteeing correctness. The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *)
adamc@147 486
adam@297 487 Definition forward : forall (f : formula) (known : set index) (hyp : formula)
adam@297 488 (cont : forall known', [allTrue known' -> formulaDenote atomics f]),
adam@297 489 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
adamc@144 490 refine (fix F (f : formula) (known : set index) (hyp : formula)
adamc@221 491 (cont : forall known', [allTrue known' -> formulaDenote atomics f])
adamc@144 492 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
adamc@221 493 match hyp with
adamc@144 494 | Atomic v => Reduce (cont (add known v))
adamc@144 495 | Truth => Reduce (cont known)
adamc@144 496 | Falsehood => Yes
adamc@144 497 | And h1 h2 =>
adamc@144 498 Reduce (F (Imp h2 f) known h1 (fun known' =>
adamc@144 499 Reduce (F f known' h2 cont)))
adamc@144 500 | Or h1 h2 => F f known h1 cont && F f known h2 cont
adamc@144 501 | Imp _ _ => Reduce (cont known)
adamc@144 502 end); crush.
adamc@144 503 Defined.
adamc@144 504
adamc@147 505 (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *)
adamc@147 506
adam@362 507 (* begin thide *)
adam@297 508 Definition backward : forall (known : set index) (f : formula),
adam@297 509 [allTrue known -> formulaDenote atomics f].
adamc@221 510 refine (fix F (known : set index) (f : formula)
adamc@221 511 : [allTrue known -> formulaDenote atomics f] :=
adamc@221 512 match f with
adamc@144 513 | Atomic v => Reduce (In_dec v known)
adamc@144 514 | Truth => Yes
adamc@144 515 | Falsehood => No
adamc@144 516 | And f1 f2 => F known f1 && F known f2
adamc@144 517 | Or f1 f2 => F known f1 || F known f2
adamc@144 518 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
adamc@144 519 end); crush; eauto.
adamc@144 520 Defined.
adam@362 521 (* end thide *)
adamc@144 522
adamc@147 523 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *)
adamc@147 524
adam@297 525 Definition my_tauto : forall f : formula, [formulaDenote atomics f].
adam@362 526 (* begin thide *)
adamc@144 527 intro; refine (Reduce (backward nil f)); crush.
adamc@144 528 Defined.
adam@362 529 (* end thide *)
adamc@144 530 End my_tauto.
adamc@144 531
adam@360 532 (** Our final tactic implementation is now fairly straightforward. First, we [intro] all quantifiers that do not bind [Prop]s. Then we call the [quote] tactic, which implements the reification for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *)
adamc@147 533
adamc@144 534 Ltac my_tauto :=
adamc@144 535 repeat match goal with
adamc@144 536 | [ |- forall x : ?P, _ ] =>
adamc@144 537 match type of P with
adamc@144 538 | Prop => fail 1
adamc@144 539 | _ => intro
adamc@144 540 end
adamc@144 541 end;
adamc@144 542 quote formulaDenote;
adamc@144 543 match goal with
adamc@144 544 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
adamc@144 545 end.
adamc@148 546 (* end thide *)
adamc@144 547
adamc@147 548 (** A few examples demonstrate how the tactic works. *)
adamc@147 549
adamc@144 550 Theorem mt1 : True.
adamc@144 551 my_tauto.
adamc@144 552 Qed.
adamc@144 553
adamc@144 554 Print mt1.
adamc@221 555 (** %\vspace{-.15in}% [[
adamc@147 556 mt1 = partialOut (my_tauto (Empty_vm Prop) Truth)
adamc@147 557 : True
adamc@147 558 ]]
adamc@147 559
adamc@147 560 We see [my_tauto] applied with an empty [varmap], since every subformula is handled by [formulaDenote]. *)
adamc@144 561
adamc@144 562 Theorem mt2 : forall x y : nat, x = y --> x = y.
adamc@144 563 my_tauto.
adamc@144 564 Qed.
adamc@144 565
adam@432 566 (* begin hide *)
adam@437 567 (* begin thide *)
adam@432 568 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx).
adam@437 569 (* end thide *)
adam@432 570 (* end hide *)
adam@432 571
adamc@144 572 Print mt2.
adamc@221 573 (** %\vspace{-.15in}% [[
adamc@147 574 mt2 =
adamc@147 575 fun x y : nat =>
adamc@147 576 partialOut
adamc@147 577 (my_tauto (Node_vm (x = y) (Empty_vm Prop) (Empty_vm Prop))
adamc@147 578 (Imp (Atomic End_idx) (Atomic End_idx)))
adamc@147 579 : forall x y : nat, x = y --> x = y
adamc@147 580 ]]
adamc@147 581
adamc@147 582 Crucially, both instances of [x = y] are represented with the same index, [End_idx]. The value of this index only needs to appear once in the [varmap], whose form reveals that [varmap]s are represented as binary trees, where [index] values denote paths from tree roots to leaves. *)
adamc@144 583
adamc@144 584 Theorem mt3 : forall x y z,
adamc@144 585 (x < y /\ y > z) \/ (y > z /\ x < S y)
adamc@144 586 --> y > z /\ (x < y \/ x < S y).
adamc@144 587 my_tauto.
adamc@144 588 Qed.
adamc@144 589
adamc@144 590 Print mt3.
adamc@221 591 (** %\vspace{-.15in}% [[
adamc@147 592 fun x y z : nat =>
adamc@147 593 partialOut
adamc@147 594 (my_tauto
adamc@147 595 (Node_vm (x < S y) (Node_vm (x < y) (Empty_vm Prop) (Empty_vm Prop))
adamc@147 596 (Node_vm (y > z) (Empty_vm Prop) (Empty_vm Prop)))
adamc@147 597 (Imp
adamc@147 598 (Or (And (Atomic (Left_idx End_idx)) (Atomic (Right_idx End_idx)))
adamc@147 599 (And (Atomic (Right_idx End_idx)) (Atomic End_idx)))
adamc@147 600 (And (Atomic (Right_idx End_idx))
adamc@147 601 (Or (Atomic (Left_idx End_idx)) (Atomic End_idx)))))
adamc@147 602 : forall x y z : nat,
adamc@147 603 x < y /\ y > z \/ y > z /\ x < S y --> y > z /\ (x < y \/ x < S y)
adamc@147 604 ]]
adamc@147 605
adamc@147 606 Our goal contained three distinct atomic formulas, and we see that a three-element [varmap] is generated.
adamc@147 607
adamc@147 608 It can be interesting to observe differences between the level of repetition in proof terms generated by [my_tauto] and [tauto] for especially trivial theorems. *)
adamc@144 609
adamc@144 610 Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False.
adamc@144 611 my_tauto.
adamc@144 612 Qed.
adamc@144 613
adamc@144 614 Print mt4.
adamc@221 615 (** %\vspace{-.15in}% [[
adamc@147 616 mt4 =
adamc@147 617 partialOut
adamc@147 618 (my_tauto (Empty_vm Prop)
adamc@147 619 (Imp
adamc@147 620 (And Truth
adamc@147 621 (And Truth
adamc@147 622 (And Truth (And Truth (And Truth (And Truth Falsehood))))))
adamc@147 623 Falsehood))
adamc@147 624 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False
adam@302 625 ]]
adam@302 626 *)
adamc@144 627
adamc@144 628 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
adamc@144 629 tauto.
adamc@144 630 Qed.
adamc@144 631
adam@432 632 (* begin hide *)
adam@437 633 (* begin thide *)
adam@432 634 Definition fi := False_ind.
adam@437 635 (* end thide *)
adam@432 636 (* end hide *)
adam@432 637
adamc@144 638 Print mt4'.
adamc@221 639 (** %\vspace{-.15in}% [[
adamc@147 640 mt4' =
adamc@147 641 fun H : True /\ True /\ True /\ True /\ True /\ True /\ False =>
adamc@147 642 and_ind
adamc@147 643 (fun (_ : True) (H1 : True /\ True /\ True /\ True /\ True /\ False) =>
adamc@147 644 and_ind
adamc@147 645 (fun (_ : True) (H3 : True /\ True /\ True /\ True /\ False) =>
adamc@147 646 and_ind
adamc@147 647 (fun (_ : True) (H5 : True /\ True /\ True /\ False) =>
adamc@147 648 and_ind
adamc@147 649 (fun (_ : True) (H7 : True /\ True /\ False) =>
adamc@147 650 and_ind
adamc@147 651 (fun (_ : True) (H9 : True /\ False) =>
adamc@147 652 and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
adamc@147 653 H9) H7) H5) H3) H1) H
adamc@147 654 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
adam@302 655 ]]
adam@360 656
adam@360 657 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *)
adamc@147 658
adam@361 659 (** ** Manual Reification of Terms with Variables *)
adam@361 660
adam@362 661 (* begin thide *)
adam@361 662 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced.
adam@361 663
adam@361 664 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, maintaining lack of duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *)
adam@361 665
adam@361 666 Ltac inList x xs :=
adam@361 667 match xs with
adam@361 668 | tt => false
adam@361 669 | (x, _) => true
adam@361 670 | (_, ?xs') => inList x xs'
adam@361 671 end.
adam@361 672
adam@361 673 Ltac addToList x xs :=
adam@361 674 let b := inList x xs in
adam@361 675 match b with
adam@361 676 | true => xs
adam@361 677 | false => constr:(x, xs)
adam@361 678 end.
adam@361 679
adam@361 680 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *)
adam@361 681
adam@361 682 Ltac allVars xs e :=
adam@361 683 match e with
adam@361 684 | True => xs
adam@361 685 | False => xs
adam@361 686 | ?e1 /\ ?e2 =>
adam@361 687 let xs := allVars xs e1 in
adam@361 688 allVars xs e2
adam@361 689 | ?e1 \/ ?e2 =>
adam@361 690 let xs := allVars xs e1 in
adam@361 691 allVars xs e2
adam@361 692 | ?e1 -> ?e2 =>
adam@361 693 let xs := allVars xs e1 in
adam@361 694 allVars xs e2
adam@361 695 | _ => addToList e xs
adam@361 696 end.
adam@361 697
adam@361 698 (** We will also need a way to map a value to its position in a list. *)
adam@361 699
adam@361 700 Ltac lookup x xs :=
adam@361 701 match xs with
adam@361 702 | (x, _) => O
adam@361 703 | (_, ?xs') =>
adam@361 704 let n := lookup x xs' in
adam@361 705 constr:(S n)
adam@361 706 end.
adam@361 707
adam@361 708 (** The next building block is a procedure for reifying a term, given a list of all allowed variable values. We are free to make this procedure partial, where tactic failure may be triggered upon attempting to reflect a term containing subterms not included in the list of variables. The output type of the term is a copy of [formula] where [index] is replaced by [nat], in the type of the constructor for atomic formulas. *)
adam@361 709
adam@361 710 Inductive formula' : Set :=
adam@361 711 | Atomic' : nat -> formula'
adam@361 712 | Truth' : formula'
adam@361 713 | Falsehood' : formula'
adam@361 714 | And' : formula' -> formula' -> formula'
adam@361 715 | Or' : formula' -> formula' -> formula'
adam@361 716 | Imp' : formula' -> formula' -> formula'.
adam@361 717
adam@361 718 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *)
adam@361 719
adam@361 720 Ltac reifyTerm xs e :=
adam@361 721 match e with
adam@432 722 | True => constr:Truth'
adam@432 723 | False => constr:Falsehood'
adam@361 724 | ?e1 /\ ?e2 =>
adam@361 725 let p1 := reifyTerm xs e1 in
adam@361 726 let p2 := reifyTerm xs e2 in
adam@361 727 constr:(And' p1 p2)
adam@361 728 | ?e1 \/ ?e2 =>
adam@361 729 let p1 := reifyTerm xs e1 in
adam@361 730 let p2 := reifyTerm xs e2 in
adam@361 731 constr:(Or' p1 p2)
adam@361 732 | ?e1 -> ?e2 =>
adam@361 733 let p1 := reifyTerm xs e1 in
adam@361 734 let p2 := reifyTerm xs e2 in
adam@361 735 constr:(Imp' p1 p2)
adam@361 736 | _ =>
adam@361 737 let n := lookup e xs in
adam@361 738 constr:(Atomic' n)
adam@361 739 end.
adam@361 740
adam@361 741 (** Finally, we bring all the pieces together. *)
adam@361 742
adam@361 743 Ltac reify :=
adam@361 744 match goal with
adam@361 745 | [ |- ?G ] => let xs := allVars tt G in
adam@361 746 let p := reifyTerm xs G in
adam@361 747 pose p
adam@361 748 end.
adam@361 749
adam@361 750 (** A quick test verifies that we are doing reification correctly. *)
adam@361 751
adam@361 752 Theorem mt3' : forall x y z,
adam@361 753 (x < y /\ y > z) \/ (y > z /\ x < S y)
adam@361 754 -> y > z /\ (x < y \/ x < S y).
adam@361 755 do 3 intro; reify.
adam@361 756
adam@361 757 (** Our simple tactic adds the translated term as a new variable:
adam@361 758 [[
adam@361 759 f := Imp'
adam@361 760 (Or' (And' (Atomic' 2) (Atomic' 1)) (And' (Atomic' 1) (Atomic' 0)))
adam@361 761 (And' (Atomic' 1) (Or' (Atomic' 2) (Atomic' 0))) : formula'
adam@361 762 ]]
adam@361 763 *)
adam@361 764 Abort.
adam@361 765
adam@361 766 (** More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with [quote]. *)
adam@362 767 (* end thide *)
adam@378 768
adam@378 769
adam@378 770 (** * Building a Reification Tactic that Recurses Under Binders *)
adam@378 771
adam@378 772 (** All of our examples so far have stayed away from reifying the syntax of terms that use such features as quantifiers and [fun] function abstractions. Such cases are complicated by the fact that different subterms may be allowed to reference different sets of free variables. Some cleverness is needed to clear this hurdle, but a few simple patterns will suffice. Consider this example of a simple dependently typed term language, where a function abstraction body is represented conveniently with a Coq function. *)
adam@378 773
adam@378 774 Inductive type : Type :=
adam@378 775 | Nat : type
adam@378 776 | NatFunc : type -> type.
adam@378 777
adam@378 778 Inductive term : type -> Type :=
adam@378 779 | Const : nat -> term Nat
adam@378 780 | Plus : term Nat -> term Nat -> term Nat
adam@378 781 | Abs : forall t, (nat -> term t) -> term (NatFunc t).
adam@378 782
adam@378 783 Fixpoint typeDenote (t : type) : Type :=
adam@378 784 match t with
adam@378 785 | Nat => nat
adam@378 786 | NatFunc t => nat -> typeDenote t
adam@378 787 end.
adam@378 788
adam@378 789 Fixpoint termDenote t (e : term t) : typeDenote t :=
adam@378 790 match e with
adam@378 791 | Const n => n
adam@378 792 | Plus e1 e2 => termDenote e1 + termDenote e2
adam@378 793 | Abs _ e1 => fun x => termDenote (e1 x)
adam@378 794 end.
adam@378 795
adam@378 796 (** Here is a naive first attempt at a reification tactic. *)
adam@378 797
adam@378 798 Ltac refl' e :=
adam@378 799 match e with
adam@378 800 | ?E1 + ?E2 =>
adam@378 801 let r1 := refl' E1 in
adam@378 802 let r2 := refl' E2 in
adam@378 803 constr:(Plus r1 r2)
adam@378 804
adam@378 805 | fun x : nat => ?E1 =>
adam@378 806 let r1 := refl' E1 in
adam@378 807 constr:(Abs (fun x => r1 x))
adam@378 808
adam@378 809 | _ => constr:(Const e)
adam@378 810 end.
adam@378 811
adam@398 812 (** Recall that a regular Ltac pattern variable [?X] only matches terms that _do not mention new variables introduced within the pattern_. In our naive implementation, the case for matching function abstractions matches the function body in a way that prevents it from mentioning the function argument! Our code above plays fast and loose with the function body in a way that leads to independent problems, but we could change the code so that it indeed handles function abstractions that ignore their arguments.
adam@378 813
adam@378 814 To handle functions in general, we will use the pattern variable form [@?X], which allows [X] to mention newly introduced variables that are declared explicitly. For instance: *)
adam@378 815
adam@378 816 Reset refl'.
adam@378 817 Ltac refl' e :=
adam@378 818 match e with
adam@378 819 | ?E1 + ?E2 =>
adam@378 820 let r1 := refl' E1 in
adam@378 821 let r2 := refl' E2 in
adam@378 822 constr:(Plus r1 r2)
adam@378 823
adam@378 824 | fun x : nat => @?E1 x =>
adam@378 825 let r1 := refl' E1 in
adam@378 826 constr:(Abs r1)
adam@378 827
adam@378 828 | _ => constr:(Const e)
adam@378 829 end.
adam@378 830
adam@398 831 (** Now, in the abstraction case, we bind [E1] as a function from an [x] value to the value of the abstraction body. Unfortunately, our recursive call there is not destined for success. It will match the same abstraction pattern and trigger another recursive call, and so on through infinite recursion. One last refactoring yields a working procedure. The key idea is to consider every input to [refl'] as _a function over the values of variables introduced during recursion_. *)
adam@378 832
adam@378 833 Reset refl'.
adam@378 834 Ltac refl' e :=
adam@378 835 match eval simpl in e with
adam@378 836 | fun x : ?T => @?E1 x + @?E2 x =>
adam@378 837 let r1 := refl' E1 in
adam@378 838 let r2 := refl' E2 in
adam@378 839 constr:(fun x => Plus (r1 x) (r2 x))
adam@378 840
adam@378 841 | fun (x : ?T) (y : nat) => @?E1 x y =>
adam@378 842 let r1 := refl' (fun p : T * nat => E1 (fst p) (snd p)) in
adam@378 843 constr:(fun x => Abs (fun y => r1 (x, y)))
adam@378 844
adam@378 845 | _ => constr:(fun x => Const (e x))
adam@378 846 end.
adam@378 847
adam@378 848 (** Note how now even the addition case works in terms of functions, with [@?X] patterns. The abstraction case introduces a new variable by extending the type used to represent the free variables. In particular, the argument to [refl'] used type [T] to represent all free variables. We extend the type to [T * nat] for the type representing free variable values within the abstraction body. A bit of bookkeeping with pairs and their projections produces an appropriate version of the abstraction body to pass in a recursive call. To ensure that all this repackaging of terms does not interfere with pattern matching, we add an extra [simpl] reduction on the function argument, in the first line of the body of [refl'].
adam@378 849
adam@378 850 Now one more tactic provides an example of how to apply reification. Let us consider goals that are equalities between terms that can be reified. We want to change such goals into equalities between appropriate calls to [termDenote]. *)
adam@378 851
adam@378 852 Ltac refl :=
adam@378 853 match goal with
adam@378 854 | [ |- ?E1 = ?E2 ] =>
adam@378 855 let E1' := refl' (fun _ : unit => E1) in
adam@378 856 let E2' := refl' (fun _ : unit => E2) in
adam@378 857 change (termDenote (E1' tt) = termDenote (E2' tt));
adam@378 858 cbv beta iota delta [fst snd]
adam@378 859 end.
adam@378 860
adam@378 861 Goal (fun (x y : nat) => x + y + 13) = (fun (_ z : nat) => z).
adam@378 862 refl.
adam@378 863 (** %\vspace{-.15in}%[[
adam@378 864 ============================
adam@378 865 termDenote
adam@378 866 (Abs
adam@378 867 (fun y : nat =>
adam@378 868 Abs (fun y0 : nat => Plus (Plus (Const y) (Const y0)) (Const 13)))) =
adam@378 869 termDenote (Abs (fun _ : nat => Abs (fun y0 : nat => Const y0)))
adam@378 870 ]]
adam@378 871 *)
adam@378 872
adam@378 873 Abort.
adam@378 874
adam@378 875 (** Our encoding here uses Coq functions to represent binding within the terms we reify, which makes it difficult to implement certain functions over reified terms. An alternative would be to represent variables with numbers. This can be done by writing a slightly smarter reification function that detects variable references by detecting when term arguments are just compositions of [fst] and [snd]; from the order of the compositions we may read off the variable number. We leave the details as an exercise for the reader. *)