Mercurial > cpdt > repo

comparison src/Reflection.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 36428dfcde84
children 2c8c693ddaba
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2008-2012, Adam Chlipala 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import List.
12 12
13 Require Import CpdtTactics MoreSpecif. 13 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 19
19 (** %\chapter{Proof by Reflection}% *) 20 (** %\chapter{Proof by Reflection}% *)
20 21
791 | Abs _ e1 => fun x => termDenote (e1 x) 792 | Abs _ e1 => fun x => termDenote (e1 x)
792 end. 793 end.
793 794
794 (** Here is a %\%naive%{}% first attempt at a reification tactic. *) 795 (** Here is a %\%naive%{}% first attempt at a reification tactic. *)
795 796
797 (* begin hide *)
798 Definition red_herring := O.
799 (* end hide *)
796 Ltac refl' e := 800 Ltac refl' e :=
797 match e with 801 match e with
798 | ?E1 + ?E2 => 802 | ?E1 + ?E2 =>
799 let r1 := refl' E1 in 803 let r1 := refl' E1 in
800 let r2 := refl' E2 in 804 let r2 := refl' E2 in
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. 814 (** 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.
811 815
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: *) 816 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: *)
813 817
814 Reset refl'. 818 Reset refl'.
819 (* begin hide *)
820 Reset red_herring.
821 Definition red_herring := O.
822 (* end hide *)
815 Ltac refl' e := 823 Ltac refl' e :=
816 match e with 824 match e with
817 | ?E1 + ?E2 => 825 | ?E1 + ?E2 =>
818 let r1 := refl' E1 in 826 let r1 := refl' E1 in
819 let r2 := refl' E2 in 827 let r2 := refl' E2 in
827 end. 835 end.
828 836
829 (** 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_. *) 837 (** 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_. *)
830 838
831 Reset refl'. 839 Reset refl'.
840 (* begin hide *)
841 Reset red_herring.
842 (* end hide *)
832 Ltac refl' e := 843 Ltac refl' e :=
833 match eval simpl in e with 844 match eval simpl in e with
834 | fun x : ?T => @?E1 x + @?E2 x => 845 | fun x : ?T => @?E1 x + @?E2 x =>
835 let r1 := refl' E1 in 846 let r1 := refl' E1 in
836 let r2 := refl' E2 in 847 let r2 := refl' E2 in
837 constr:(fun x => Plus (r1 x) (r2 x)) 848 constr:(fun x => Plus (r1 x) (r2 x))
838 849
839 | fun (x : ?T) (y : nat) => @?E1 x y => 850 | fun (x : ?T) (y : nat) => @?E1 x y =>
840 let r1 := refl' (fun p : T * nat => E1 (fst p) (snd p)) in 851 let r1 := refl' (fun p : T * nat => E1 (fst p) (snd p)) in
841 constr:(fun x => Abs (fun y => r1 (x, y))) 852 constr:(fun u => Abs (fun v => r1 (u, v)))
842 853
843 | _ => constr:(fun x => Const (e x)) 854 | _ => constr:(fun x => Const (e x))
844 end. 855 end.
845 856
846 (** 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']. 857 (** 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'].