Created
May 30, 2015 02:41
-
-
Save nkaretnikov/b93957d383155e1043bd to your computer and use it in GitHub Desktop.
optimize_plus0
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Theorem optimize_plus0_sound: forall a, | |
| aeval (optimize_plus0 a) = aeval a. | |
| Proof. | |
| intros a. | |
| induction a. | |
| Case "ANum". reflexivity. | |
| Case "APlus". destruct a2. | |
| SCase "a2 = ANum n". destruct n. | |
| SSCase "n = 0". simpl. rewrite IHa1. rewrite plus_0_r. reflexivity. | |
| SSCase "n <> 0". simpl. rewrite IHa1. reflexivity. | |
| SCase "a2 = APlus a2_1 a2_2". | |
| simpl. simpl in IHa2. rewrite IHa2. | |
| rewrite IHa1. reflexivity. | |
| SCase "a2 = AMinus a2_1 a2_2". | |
| simpl. simpl in IHa2. rewrite IHa2. | |
| rewrite IHa1. reflexivity. | |
| SCase "a2 = AMult a2_1 a2_2". | |
| simpl. simpl in IHa2. rewrite IHa2. | |
| rewrite IHa1. reflexivity. | |
| Case "AMinus". | |
| simpl. rewrite IHa2. rewrite IHa1. reflexivity. | |
| Case "AMult". | |
| simpl. rewrite IHa2. rewrite IHa1. reflexivity. | |
| Qed. | |
| Theorem optimize_plus0_sound': forall a, | |
| aeval (optimize_plus0 a) = aeval a. | |
| Proof. | |
| intros. induction a; | |
| try (simpl; try (rewrite IHa2; rewrite IHa1); reflexivity); | |
| destruct a2; | |
| try (destruct n; simpl; rewrite IHa1; try rewrite plus_0_r; reflexivity); | |
| try (simpl; simpl in IHa2; rewrite IHa2; rewrite IHa1; reflexivity). | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment