Mercurial > cpdt > repo
comparison src/Reflection.v @ 484:5025a401ad9e
Last round of feedback from class at Penn
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 06 Jan 2013 16:23:26 -0500 |
parents | 40a9a36844d6 |
children | 2d66421b8aa1 |
comparison
equal
deleted
inserted
replaced
483:582cf453878e | 484:5025a401ad9e |
---|---|
399 | Imp : formula -> formula -> formula. | 399 | Imp : formula -> formula -> formula. |
400 (* end thide *) | 400 (* end thide *) |
401 | 401 |
402 (** 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. | 402 (** 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. |
403 | 403 |
404 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. *) | 404 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 wants to treat function types specially, so it gets confused if function types are part of the structure we want to encode syntactically. To trick [quote] into not noticing our uses of function types to express logical implication, we will need to declare a wrapper definition for implication, as we did in the last chapter. *) |
405 | 405 |
406 Definition imp (P1 P2 : Prop) := P1 -> P2. | 406 Definition imp (P1 P2 : Prop) := P1 -> P2. |
407 Infix "-->" := imp (no associativity, at level 95). | 407 Infix "-->" := imp (no associativity, at level 95). |
408 | 408 |
409 (** Now we can define our denotation function. *) | 409 (** Now we can define our denotation function. *) |
476 | 476 |
477 Hint Resolve allTrue_add allTrue_In. | 477 Hint Resolve allTrue_add allTrue_In. |
478 | 478 |
479 Local Open Scope partial_scope. | 479 Local Open Scope partial_scope. |
480 | 480 |
481 (** 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]. *) | 481 (** Now we can write a function [forward] that implements deconstruction of hypotheses, expanding a compound formula into a set of sets of atomic formulas covering all possible cases introduced with use of [Or]. To handle consideration of multiple cases, the function takes in a continuation argument, which will be called once for each case. |
482 | |
483 The [forward] function 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]. *) | |
482 | 484 |
483 Definition forward : forall (f : formula) (known : set index) (hyp : formula) | 485 Definition forward : forall (f : formula) (known : set index) (hyp : formula) |
484 (cont : forall known', [allTrue known' -> formulaDenote atomics f]), | 486 (cont : forall known', [allTrue known' -> formulaDenote atomics f]), |
485 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. | 487 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. |
486 refine (fix F (f : formula) (known : set index) (hyp : formula) | 488 refine (fix F (f : formula) (known : set index) (hyp : formula) |
787 | Const n => n | 789 | Const n => n |
788 | Plus e1 e2 => termDenote e1 + termDenote e2 | 790 | Plus e1 e2 => termDenote e1 + termDenote e2 |
789 | Abs _ e1 => fun x => termDenote (e1 x) | 791 | Abs _ e1 => fun x => termDenote (e1 x) |
790 end. | 792 end. |
791 | 793 |
792 (** Here is a %\%naive first attempt at a reification tactic. *) | 794 (** Here is a %\%naive%{}% first attempt at a reification tactic. *) |
793 | 795 |
794 Ltac refl' e := | 796 Ltac refl' e := |
795 match e with | 797 match e with |
796 | ?E1 + ?E2 => | 798 | ?E1 + ?E2 => |
797 let r1 := refl' E1 in | 799 let r1 := refl' E1 in |
803 constr:(Abs (fun x => r1 x)) | 805 constr:(Abs (fun x => r1 x)) |
804 | 806 |
805 | _ => constr:(Const e) | 807 | _ => constr:(Const e) |
806 end. | 808 end. |
807 | 809 |
808 (** 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. | 810 (** 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. |
809 | 811 |
810 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: *) | 812 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. A use of [@?X] must be followed by a list of the local variables that may be mentioned. The variable [X] then comes to stand for a Gallina function over the values of those variables. For instance: *) |
811 | 813 |
812 Reset refl'. | 814 Reset refl'. |
813 Ltac refl' e := | 815 Ltac refl' e := |
814 match e with | 816 match e with |
815 | ?E1 + ?E2 => | 817 | ?E1 + ?E2 => |
866 ]] | 868 ]] |
867 *) | 869 *) |
868 | 870 |
869 Abort. | 871 Abort. |
870 | 872 |
871 (** 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 identifies 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. *) | 873 (** 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 identifies 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 (though not a trivial one!) for the reader. *) |