Created
April 24, 2014 10:38
-
-
Save yoshihiro503/11249864 to your computer and use it in GitHub Desktop.
なぜCoqが重要か ref: http://qiita.com/yoshihiro503/items/7e6a9994eb37ed7c3bf9
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 map_length: forall A B:Type f xs, | |
| length (map f xs) = length xs. | |
| Proof. | |
| intros A B f xs. induction xs. | |
| reflexivity. | |
| simpl. rewrite IHxs. reflexivity. | |
| Qed. |
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 map_length: forall A B:Type f xs, length (map f xs) = length xs. | |
| Proof. | |
| intros A B f xs. induction xs. | |
| reflexivity. | |
| simpl. rewrite IHxs. reflexivity. | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment