Last round of feedback from class at Penn
author Adam Chlipala Sun, 06 Jan 2013 16:23:26 -0500 40a9a36844d6 2d66421b8aa1
comparison
equal inserted replaced
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
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]),
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. *)