GitHub PullRequestReviewCommentEvent at 2014-04-23 19:12:26
Repository: HoTT
Actor: JasonGross
Payload: {"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/11918243","id":11918243,"diff_hunk":"@@ -256,3 +256,24 @@ End minus1TruncMonad.\n \n (** We may want to define the other connectives to at some point. *)\n Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).\n+\n+(** If the goal is an hProp, we may remove [minus1Trunc] in hypotheses. *)\n+Ltac strip_truncations :=\n+  (** get the type of the goal *)\n+  let G := match goal with |- ?G => constr:(G) end in\n+  (** prove that the goal is an hProp *)\n+  let H := fresh in\n+  assert (H : forall z w : G, z = w) by apply allpath_hprop;\n+    (** search for truncated hypotheses *)\n+    progress repeat match goal with\n+                      | [ T : _ |- _ ]\n+                        => revert T;\n+                          refine (@minus1Trunc_rect_nondep _ _ _ H);\n+                          intro T\n+                    end;\n+    (** clear the IsHProp hypothesis *)\n+    clear H.\n+\n+(** Define a lengthy pun for the above tactic. *)\n+Ltac since_the_goal_is_a_mere_proposition_we_may_strip_truncations","path":"theories/hit/minus1Trunc.v","position":23,"original_position":23,"commit_id":"7f6d4cfe2c0213e83cd3486286ca1ff1e7e4b1dd","original_commit_id":"7f6d4cfe2c0213e83cd3486286ca1ff1e7e4b1dd","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?","gravatar_id":"c11c7cc23517cf5f043b51fc7914049a","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"body":"Quoting from the individual commit, so that this sticks around better with the pull request:\r\n\r\n@spitters said\r\n> Why this pun ?\r\n\r\nI figured that anyone wanting to mirror proofs in the book ~verbatim might appreciate this tactic, (or maybe it should be `Tactic Notation \"Since\" \"the\" \"goal\" \"is\" \"a\" \"mere\" \"proposition,\" \"we\" \"may\" \"strip\" \"truncations\"`).  I could probably get it even closer, if there's actually an interest here, so that you could write `Since our goal is a mere proposition, we may assume given a : A and H : P a.` and have it find a truncated thing of type `{ a : A | P a}` and give you back a hypothesis `a : A` and a hypothesis `H : P a`.","created_at":"2014-04-23T19:12:26Z","updated_at":"2014-04-23T19:12:26Z","html_url":"https://github.com/HoTT/HoTT/pull/378#discussion_r11918243","pull_request_url":"https://api.github.com/repos/HoTT/HoTT/pulls/378","_links":{"self":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/11918243"},"html":{"href":"https://github.com/HoTT/HoTT/pull/378#discussion_r11918243"},"pull_request":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/378"}}}}