{"action":"created","issue":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/71","labels_url":"https://api.github.com/repos/snu-sf/pl2015/issues/71/labels{/name}","comments_url":"https://api.github.com/repos/snu-sf/pl2015/issues/71/comments","events_url":"https://api.github.com/repos/snu-sf/pl2015/issues/71/events","html_url":"https://github.com/snu-sf/pl2015/issues/71","id":69107515,"number":71,"title":"About the usage of SearchAbout and SearchPattern","user":{"login":"jaewooklee93","id":11328376,"avatar_url":"https://avatars.githubusercontent.com/u/11328376?v=3","gravatar_id":"","url":"https://api.github.com/users/jaewooklee93","html_url":"https://github.com/jaewooklee93","followers_url":"https://api.github.com/users/jaewooklee93/followers","following_url":"https://api.github.com/users/jaewooklee93/following{/other_user}","gists_url":"https://api.github.com/users/jaewooklee93/gists{/gist_id}","starred_url":"https://api.github.com/users/jaewooklee93/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaewooklee93/subscriptions","organizations_url":"https://api.github.com/users/jaewooklee93/orgs","repos_url":"https://api.github.com/users/jaewooklee93/repos","events_url":"https://api.github.com/users/jaewooklee93/events{/privacy}","received_events_url":"https://api.github.com/users/jaewooklee93/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-04-17T09:58:10Z","updated_at":"2015-04-17T11:31:00Z","closed_at":null,"body":"For proving ```pigeonhole_principle```, I used the theorem ```S n < S m -> n < m```.\r\n\r\nHowever, the problem is that I don't know how I can find that theorem using ```SearchPattern```. My first try was ```SearchPattern (S _ < S _ -> _ < _)```, however, it didn't give any useful information. It only showed\r\n```\r\nCoq < SearchPattern (S _ < S _ -> _ < _).\r\n\r\nWarning: query commands should not be inserted in scripts\r\n```\r\n\r\nSo I tried again with ```SearchPattern (S _ <= S _ -> _ <= _)```. At this time, I got the following result.\r\n```\r\nCoq < SearchPattern (S _ <= S _ -> _ <= _).\r\n\r\nWarning: query commands should not be inserted in scripts\r\nle_S_n: forall n m : nat, S n <= S m -> n <= m\r\nLe.le_S_n: forall n m : nat, S n <= S m -> n <= m\r\nSn_le_Sm__n_le_m: forall n m : nat, S n <= S m -> n <= m\r\n```\r\n\r\nThus, I just guessed that I could use ```Lt.lt_S_n``` for my purpose, since ```Le.le_S_n``` gave such result. That guess was found to be correct. After I had known the name if theorem, I could find its content with using ```SearchAbout```.\r\n```\r\nCoq < SearchAbout \"lt_S_n\".\r\n\r\nWarning: query commands should not be inserted in scripts\r\nLt.lt_S_n: forall n m : nat, S n < S m -> n < m\r\n```\r\n\r\nOn the other hand, when I used ```SearchAbout``` instead of ```SearchPattern``` to look for the theorem related to ```<=```, it gave \r\n```\r\nCoq < SearchAbout le.\r\n\r\nWarning: query commands should not be inserted in scripts\r\nBetween.between_le:\r\n  forall (P : nat -> Prop) (k l : nat), Between.between P k l -> k <= l\r\nBetween.between_Sk_l:\r\n  forall (P : nat -> Prop) (k l : nat),\r\n  Between.between P k l -> S k <= l -> Between.between P (S k) l\r\nBetween.between_restr:\r\n  forall (P : nat -> Prop) (k l m : nat),\r\n  k <= l -> l <= m -> Between.between P k m ->\r\n...\r\n\r\n(1000 lines of incomprehensible search results)\r\n```\r\nSo I think that ```SearchAbout``` is almost useless if I deal with built-in objects like ```plus```, ```mult``` or ```le```, since it brings us bunch of theorems we don't need as well. Is it right?\r\n\r\nIn conclusion, my questions are, \r\n\r\n1. In both of homework and exams, can we use all theorems which can be found by ```SearchAbout``` or ```SearchPattern```, such as ```le_S_n```, ```Le.le_S_n``` and ```Sn_le_Sm__n_le_m```. Or, is there the most preferable one among them?\r\n\r\n2. What is the proper way to find the theorem ```S n < S m -> n < m``` using ```SearchPattern``` in one-shot?\r\n\r\n3. Can we use ```SearchAbout``` to search for theorems related to built-in objects? Since ```SearchPattern``` needs the exact pattern of theorem, it is sometimes harder to use than ```SearchAbout```."},"comment":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/comments/93969026","html_url":"https://github.com/snu-sf/pl2015/issues/71#issuecomment-93969026","issue_url":"https://api.github.com/repos/snu-sf/pl2015/issues/71","id":93969026,"user":{"login":"fortunist","id":1583071,"avatar_url":"https://avatars.githubusercontent.com/u/1583071?v=3","gravatar_id":"","url":"https://api.github.com/users/fortunist","html_url":"https://github.com/fortunist","followers_url":"https://api.github.com/users/fortunist/followers","following_url":"https://api.github.com/users/fortunist/following{/other_user}","gists_url":"https://api.github.com/users/fortunist/gists{/gist_id}","starred_url":"https://api.github.com/users/fortunist/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fortunist/subscriptions","organizations_url":"https://api.github.com/users/fortunist/orgs","repos_url":"https://api.github.com/users/fortunist/repos","events_url":"https://api.github.com/users/fortunist/events{/privacy}","received_events_url":"https://api.github.com/users/fortunist/received_events","type":"User","site_admin":false},"created_at":"2015-04-17T11:31:00Z","updated_at":"2015-04-17T11:31:00Z","body":"2.\r\nI found the way using <code>SearchAbout (Peano.lt (S _) (S _) -> Peano.lt _ _).</code>\r\nThough I cannot explain why it does not work without <code>Require Export \"Prop\".</code>......"}}