Mercurial > cpdt > repo

comparison src/Hoas.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents 2c88fc1dbe33
children 7b38729be069
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, 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:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Eqdep String List. 11 Require Import Eqdep String List FunctionalExtensionality.
12 12
13 Require Import Axioms Tactics. 13 Require Import Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
725 end; 725 end;
726 match type of H with 726 match type of H with
727 | ?F = ?G => 727 | ?F = ?G =>
728 let ec := equate_conj F G in 728 let ec := equate_conj F G in
729 let var := fresh "var" in 729 let var := fresh "var" in
730 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var; 730 assert ec; [ intuition; unfold Exp; extensionality var;
731 assert (H' : F var = G var); try congruence; 731 assert (H' : F var = G var); try congruence;
732 match type of H' with 732 match type of H' with
733 | ?X = ?Y => 733 | ?X = ?Y =>
734 let X := eval hnf in X in 734 let X := eval hnf in X in
735 let Y := eval hnf in Y in 735 let Y := eval hnf in Y in
736 change (X = Y) in H' 736 change (X = Y) in H'
737 end; injection H'; my_crush'; tauto 737 end; injection H'; my_crush'; tauto
738 | intuition; subst ] 738 | intuition; subst ]
739 end); 739 end);
740 clear H 740 clear H
741 end; my_crush'); 741 end; my_crush');
742 my_crush'. 742 my_crush'.