## 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']. |