{"action":"created","issue":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/17","repository_url":"https://api.github.com/repos/mit-plv/fiat-crypto","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/17/labels{/name}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/17/comments","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/17/events","html_url":"https://github.com/mit-plv/fiat-crypto/issues/17","id":163050085,"number":17,"title":"Our [nsatz] is weaker than the standard library's [nsatz]","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","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},"labels":[],"state":"open","locked":false,"assignee":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"assignees":[{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false}],"milestone":null,"comments":7,"created_at":"2016-06-29T23:27:39Z","updated_at":"2016-06-30T06:39:00Z","closed_at":null,"body":"Here is code that works:\r\n```coq\r\nRequire Import Coq.Reals.Reals Coq.nsatz.Nsatz.\r\n\r\nLocal Open Scope R.\r\n\r\nGoal forall a b yx xz : R,\r\n  yx^2 = xz^3 + a * xz + b ->\r\n  (- yx)^2 = xz^3 + a * xz + b ->\r\n  xz * (2 * yx)^2 - ((3 * xz^2 + a)^2 - xz * (2 * yx)^2 - xz * (2 * yx)^2) = 0 ->\r\n  (3 * xz^2 + a)^2 - 2 * (2 * yx)^2 * xz = (2 * yx)^2 * xz.\r\nProof.\r\n  intros ???? H0 H1 H2.\r\n  nsatz.\r\nQed.\r\n```\r\nAnd here is code that doesn't:\r\n```coq\r\nRequire Import Crypto.Tactics.Nsatz Crypto.Algebra Crypto.Util.Notations.\r\n\r\nSection F.\r\n  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}\r\n          {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.\r\n  Local Infix \"=\" := Feq : type_scope. Local Notation \"a <> b\" := (not (a = b)) : type_scope.\r\n  Local Infix \"+\" := Fadd. Local Infix \"*\" := Fmul.\r\n  Local Infix \"-\" := Fsub. Local Infix \"/\" := Fdiv.\r\n  Local Notation \"- x\" := (Fopp x).\r\n  Local Notation \"x ^ 2\" := (x*x). Local Notation \"x ^ 3\" := (x*x^2).\r\n  Local Notation \"0\" := Fzero.  Local Notation \"1\" := Fone.\r\n  Notation \"2\" := (1+1). Notation \"3\" := (1+2).\r\n  Local Open Scope core_scope.\r\n\r\n  Goal forall a b yx xz : F,\r\n    yx^2 = xz^3 + a * xz + b ->\r\n    (- yx)^2 = xz^3 + a * xz + b ->\r\n    xz * (2 * yx)^2 - ((3 * xz^2 + a)^2 - xz * (2 * yx)^2 - xz * (2 * yx)^2) = 0 ->\r\n    (3 * xz^2 + a)^2 - 2 * (2 * yx)^2 * xz = (2 * yx)^2 * xz.\r\n  Proof.\r\n    intros ???? H0 H1 H2.\r\n    nsatz. (* In nested Ltac calls to \"nsatz\", \"nsatz\", \"nsatz_sugar_power\" and \"nsatz_domain_sugar_power\", last\r\ncall failed.\r\nError: No applicable tactic.\r\ncomputation without sugar\r\np: [9]*b^4 + [(-12)]*a^2*b + [6]*b^2*c + [1]*c^2 \r\nlp:\r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 \r\nremainder: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\ncomputation of the Groebner basis\r\n[3,3]0[3,2]\r\nnew polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\nremainder: 0\r\npolynomial reduced to 0\r\nr ok\r\nr: 0\r\nverif sum: [9]*b^4 + [(-9)]*a^2*b + [9]*b^2*c + [9]*b*d \r\ncoefficient: [(-1)] \r\ncomputed\r\ntime:      0.000s\r\ncert ok\r\nuseless spolynomials: 0\r\nuseful spolynomials: 2\r\nnumber of parametres: -1\r\nterm computed\r\nterm computed\r\ncomputation without sugar\r\np: [81]*b^8 + [(-216)]*a^2*b^5 + [108]*b^6*c + [144]*a^4*b^2 + [(-144)]*a^2*b^3*c + [54]*b^4*c^2 + [(-24)]*a^2*b*c^2 + [12]*b^2*c^3 + [1]*c^4 \r\nlp:\r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 \r\nremainder: [(-9)]*a^4*b^2 + [(-18)]*a^2*b^3*c + [(-27)]*b^4*c^2 + [81]*b^5*d + [24]*a^2*b*c^2 + [(-12)]*b^2*c^3 + [(-135)]*a^2*b^2*d + [27]*b^3*c*d + [(-1)]*c^4 \r\ncomputation of the Groebner basis\r\n[3,3]0[3,2]\r\nnew polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\nremainder: [9]*a^4*c + [(-3)]*a^2*b*c^2 + [(-15)]*b^2*c^3 + [27]*a^2*b^2*d + [54]*b^3*c*d + [1]*c^4 + [(-9)]*a^2*c*d + [(-27)]*b*c^2*d + [81]*b^2*d^2 \r\n[4,4]c[4,3]\r\nnew polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d \r\nremainder: 0\r\npolynomial reduced to 0\r\nr ok\r\nr: 0\r\nverif sum: [81]*b^8 + [(-216)]*a^2*b^5 + [108]*b^6*c + [135]*a^4*b^2 + [(-153)]*a^2*b^3*c + [54]*b^4*c^2 + [(-9)]*a^4*c + [(-18)]*a^2*b*c^2 + [27]*b^2*c^3 + [(-54)]*a^2*b^2*d + [(-54)]*b^3*c*d + [9]*a^2*c*d + [27]*b*c^2*d + [(-81)]*b^2*d^2 \r\ncoefficient: [(-1)] \r\ncomputed\r\ntime:      0.000s\r\ncert ok\r\nuseless spolynomials: 0\r\nuseful spolynomials: 3\r\nnumber of parametres: -1\r\nterm computed\r\nterm computed\r\ncomputation without sugar\r\np: [729]*b^12  + 16 terms\r\nlp:\r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 \r\nremainder: [(-27)]*a^8  + 17 terms\r\ncomputation of the Groebner basis\r\n[3,3]0[3,2]\r\nnew polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\nremainder: [(-27)]*a^8  + 17 terms\r\n[4,4]c[4,3]\r\nnew polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d \r\nremainder: 0\r\npolynomial reduced to 0\r\nr ok\r\nr: 0\r\nverif sum: [729]*b^12 + [(-2916)]*a^2*b^9 + [1458]*b^10*c + [3888]*a^4*b^6 + [(-3888)]*a^2*b^7*c + [1215]*b^8*c^2 + [(-1728)]*a^6*b^3 + [2592]*a^4*b^4*c + [(-1944)]*a^2*b^5*c^2 + [540]*b^6*c^3 + [27]*a^8 + [54]*a^6*b*c + [405]*a^4*b^2*c^2 + [(-477)]*a^2*b^3*c^3 + [135]*b^4*c^4 + [81]*a^4*b^3*d + [(-63)]*a^4*c^3 + [(-18)]*a^2*b*c^4 + [81]*b^2*c^5 + [135]*a^6*d + [243]*a^4*b*c*d + [(-486)]*a^2*b^2*c^2*d + [(-378)]*b^3*c^3*d + [486]*a^2*b^3*d^2 + [9]*a^2*c^3*d + [135]*b*c^4*d + [81]*a^4*d^2 + [(-1215)]*b^2*c^2*d^2 + [729]*b^3*d^3 + [54]*c^3*d^2 + [(-243)]*a^2*d^3 + [(-729)]*b*c*d^3 \r\ncoefficient: [(-1)] \r\ncomputed\r\ntime:      0.000s\r\ncert ok\r\nuseless spolynomials: 0\r\nuseful spolynomials: 3\r\nnumber of parametres: -1\r\nterm computed\r\nterm computed\r\ncomputation without sugar\r\np: [6561]*b^16  + 25 terms\r\nlp:\r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 \r\nremainder: [81]*a^10*b  + 27 terms\r\ncomputation of the Groebner basis\r\n[3,3]0[3,2]\r\nnew polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\nremainder: [(-81)]*a^8*c^2  + 27 terms\r\n[4,4]c[4,3]\r\nnew polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d \r\nremainder: 0\r\npolynomial reduced to 0\r\nr ok\r\nr: 0\r\nverif sum: [(-6561)]*b^16 + [34992]*a^2*b^13 + [(-17496)]*b^14*c + [(-69984)]*a^4*b^10 + [69984]*a^2*b^11*c + [(-20412)]*b^12*c^2 + [62208]*a^6*b^7 + [(-93312)]*a^4*b^8*c + [58320]*a^2*b^9*c^2 + [(-13608)]*b^10*c^3 + [(-20736)]*a^8*b^4 + [41472]*a^6*b^5*c + [(-46656)]*a^4*b^6*c^2 + [25920]*a^2*b^7*c^3 + [(-5670)]*b^8*c^4 + [81]*a^10*b + [243]*a^8*b^2*c + [7074]*a^6*b^3*c^2 + [(-10368)]*a^4*b^4*c^3 + [6480]*a^2*b^5*c^4 + [(-1512)]*b^6*c^5 + [(-108)]*a^8*c^2 + [(-378)]*a^6*b*c^3 + [(-891)]*a^4*b^2*c^4 + [1053]*a^2*b^3*c^5 + [(-252)]*b^4*c^6 + [891]*a^8*b*d + [1620]*a^6*b^2*c*d + [243]*a^4*b^3*c^2*d + [297]*a^4*c^5 + [(-18)]*a^2*b*c^6 + [(-279)]*b^2*c^7 + [(-1593)]*a^6*c^2*d + [(-2025)]*a^4*b*c^3*d + [3078]*a^2*b^2*c^4*d + [2106]*b^3*c^5*d + [3402]*a^6*b*d^2 + [1458]*a^4*b^2*c*d^2 + [(-5832)]*a^2*b^3*c^2*d^2 + [135]*a^2*c^5*d + [(-711)]*b*c^6*d + [(-2673)]*a^4*c^2*d^2 + [324]*a^2*b*c^3*d^2 + [10773]*b^2*c^4*d^2 + [4374]*a^4*b*d^3 + [(-8748)]*a^2*b^2*c*d^3 + [(-15309)]*b^3*c^2*d^3 + [(-432)]*c^5*d^2 + [3645]*a^2*c^2*d^3 + [8991]*b*c^3*d^3 + [(-2187)]*a^2*b*d^4 + [(-15309)]*b^2*c*d^4 + [729]*c^2*d^4 + [(-6561)]*b*d^5 \r\ncoefficient: [1] \r\ncomputed\r\ntime:      0.001s\r\ncert ok\r\nuseless spolynomials: 0\r\nuseful spolynomials: 3\r\nnumber of parametres: -1\r\nterm computed\r\nterm computed\r\ncomputation without sugar\r\np: [59049]*b^20  + 36 terms\r\nlp:\r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d \r\n[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 \r\nremainder: [(-243)]*a^12*b^2  + 38 terms\r\ncomputation of the Groebner basis\r\n[3,3]0[3,2]\r\nnew polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d \r\nremainder: [729]*a^12*c  + 39 terms\r\n[4,4]c[4,3]\r\nnew polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d \r\nremainder: 0\r\npolynomial reduced to 0\r\nr ok\r\nr: 0\r\nverif sum: [59049]*b^20 + [(-393660)]*a^2*b^17 + [196830]*b^18*c + [1049760]*a^4*b^14 + [(-1049760)]*a^2*b^15*c + [295245]*b^16*c^2 + [(-1399680)]*a^6*b^11 + [2099520]*a^4*b^12*c + [(-1224720)]*a^2*b^13*c^2 + [262440]*b^14*c^3 + [933120]*a^8*b^8 + [(-1866240)]*a^6*b^9*c + [1749600]*a^4*b^10*c^2 + [(-816480)]*a^2*b^11*c^3 + [153090]*b^12*c^4 + [(-248832)]*a^10*b^5 + [622080]*a^8*b^6*c + [(-933120)]*a^6*b^7*c^2 + [777600]*a^4*b^8*c^3 + [(-340200)]*a^2*b^9*c^4 + [61236]*b^10*c^5 + [243]*a^12*b^2 + [243]*a^10*b^3*c + [103680]*a^8*b^4*c^2 + [(-207360)]*a^6*b^5*c^3 + [194400]*a^4*b^6*c^4 + [(-90720)]*a^2*b^7*c^5 + [17010]*b^8*c^6 + [729]*a^12*c + [81]*a^10*b*c^2 + [(-2430)]*a^8*b^2*c^3 + [(-18900)]*a^6*b^3*c^4 + [25920]*a^4*b^4*c^5 + [(-15120)]*a^2*b^5*c^6 + [3240]*b^6*c^7 + [3402]*a^10*b^2*d + [4860]*a^8*b^3*c*d + [(-135)]*a^8*c^4 + [1998]*a^6*b*c^5 + [2241]*a^4*b^2*c^6 + [(-2205)]*a^2*b^3*c^7 + [405]*b^4*c^8 + [4131]*a^10*c*d + [(-5670)]*a^8*b*c^2*d + [(-22680)]*a^6*b^2*c^3*d + [(-7047)]*a^4*b^3*c^4*d + [18225]*a^8*b^2*d^2 + [24786]*a^6*b^3*c*d^2 + [(-1251)]*a^4*c^7 + [198]*a^2*b*c^8 + [1053]*b^2*c^9 + [10827]*a^6*c^4*d + [12879]*a^4*b*c^5*d + [(-16902)]*a^2*b^2*c^6*d + [(-10746)]*b^3*c^7*d + [(-486)]*a^8*c*d^2 + [(-48114)]*a^6*b*c^2*d^2 + [(-34020)]*a^4*b^2*c^3*d^2 + [46170]*a^2*b^3*c^4*d^2 + [43740]*a^6*b^2*d^3 + [26244]*a^4*b^3*c*d^3 + [(-1287)]*a^2*c^7*d + [3591]*b*c^8*d + [31833]*a^4*c^4*d^2 + [(-4536)]*a^2*b*c^5*d^2 + [(-76059)]*b^2*c^6*d^2 + [(-30618)]*a^6*c*d^3 + [(-104976)]*a^4*b*c^2*d^3 + [145800]*a^2*b^2*c^3*d^3 + [169857]*b^3*c^4*d^3 + [32805]*a^4*b^2*d^4 + [(-85293)]*a^2*b^3*c*d^4 + [2538]*c^7*d^2 + [(-26487)]*a^2*c^4*d^3 + [(-79461)]*b*c^5*d^3 + [(-19683)]*a^4*c*d^4 + [24057]*a^2*b*c^2*d^4 + [328050]*b^2*c^3*d^4 + [(-39366)]*a^2*b^2*d^5 + [(-157464)]*b^3*c*d^5 + [(-16038)]*c^4*d^4 + [45927]*a^2*c*d^5 + [196830]*b*c^2*d^5 + [(-59049)]*b^2*d^6 \r\ncoefficient: [(-1)] \r\ncomputed\r\ntime:      0.001s\r\ncert ok\r\nuseless spolynomials: 0\r\nuseful spolynomials: 3\r\nnumber of parametres: -1\r\nterm computed\r\nterm computed\r\n *)\r\n  Qed.\r\nEnd F.\r\n```\r\n\r\nThis seems somehow related to the fact that we have duplicate information in the hypotheses."},"comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments/229572827","html_url":"https://github.com/mit-plv/fiat-crypto/issues/17#issuecomment-229572827","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/17","id":229572827,"user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"created_at":"2016-06-30T06:39:00Z","updated_at":"2016-06-30T06:39:00Z","body":"Standard library `nsatz` on `Coq.Reals.Reals` does not recognize `^` as opaque and thus uses the following list of variables: `yx ^ 2 :: xz ^ 3  :: a :: xz :: b :: (- yx) ^ 2 :: (2 * yx) ^ 2 :: (3 * xz ^ 2 + a) ^ 2`, which enables it to succeed: https://gist.github.com/andres-erbsen/ba351881bb42d101b84b30cda06f56d6. When `^2` and `^3` defined as notations for simple multiplication, standard library nsatz fails the same way as our nsatz -- `nsatz_compute` generates an invalid certificate: https://gist.github.com/andres-erbsen/d25133e021ffb0b7b4b11134a6c5e278"}}
{"actor":{"display_login":"andres-erbsen"}}