{"id":182748,"date":"2013-06-10T13:51:03","date_gmt":"2013-06-10T09:51:03","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=182748"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=182748","title":{"rendered":"<span class=\"post_title\">\u041c\u044f\u0433\u043a\u043e\u0435 \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432 Coq: \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f<\/span>"},"content":{"rendered":"<div class=\"content html_format\">   \t\u0412 <a href=\"http:\/\/habrahabr.ru\/post\/182442\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439<\/a> \u0447\u0430\u0441\u0442\u0438 \u043c\u044b \u043d\u0430\u0443\u0447\u0438\u043b\u0438\u0441\u044c \u0437\u0430\u0434\u0430\u0432\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0435 \u0442\u0438\u043f\u044b \u0438 \u0441\u0442\u0440\u043e\u0438\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043d\u0430\u0434 \u0438\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u043c\u0438. \u0412 \u044d\u0442\u043e\u0439 \u043d\u0435\u0431\u043e\u043b\u044c\u0448\u043e\u0439 \u0437\u0430\u043c\u0435\u0442\u043a\u0435 \u044f \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u044e\u0441\u044c \u043d\u0430 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u0445, \u0447\u0442\u043e\u0431\u044b \u0432\u043d\u0435\u0441\u0442\u0438 \u044f\u0441\u043d\u043e\u0441\u0442\u044c \u0438 \u043d\u0430\u043c\u0435\u0442\u0438\u0442\u044c \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0438\u0435 \u0442\u0435\u043c\u044b \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f.<\/p>\n<p>  \u0420\u0430\u043d\u0435\u0435 \u044f \u0441\u043a\u0430\u0437\u0430\u043b, \u0447\u0442\u043e \u0432 Coq \u043d\u0435\u0442 \u0431\u0430\u0442\u0430\u0440\u0435\u0435\u043a. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435 \u044f \u0441\u043b\u0443\u043a\u0430\u0432\u0438\u043b \u2014 \u0432 Coq \u0435\u0441\u0442\u044c \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u0430\u044f \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0445 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0439. \u041f\u043e\u043c\u0438\u043c\u043e \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0442 \u0438 \u0431\u043e\u043b\u0435\u0435 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0432\u0435\u0449\u0438, \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u044b \u043f\u043e\u043a\u0430 \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u043e\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0442\u044c\u0441\u044f.<br \/>  <a name=\"habracut\"><\/a><br \/>  \u0412 \u043c\u043e\u043c\u0435\u043d\u0442 \u0441\u0442\u0430\u0440\u0442\u0430 CoqIDE \u0432 \u0444\u043e\u043d\u043e\u0432\u043e\u043c \u0440\u0435\u0436\u0438\u043c\u0435 \u043f\u043e\u0434\u0440\u0443\u0433\u0436\u0430\u044e\u0442\u0441\u044f \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438, \u0441\u043f\u0438\u0441\u043e\u043a \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u043e\u0436\u043d\u043e \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u043e\u043c\u0430\u043d\u0434\u044b <code>Print Libraries<\/code>:<\/p>\n<pre> Loaded and imported library files:    Coq.Init.Notations    Coq.Init.Logic    Coq.Init.Datatypes    Coq.Init.Specif    Coq.Init.Peano    Coq.Init.Wf    Coq.Init.Tactics    Coq.Init.Prelude    Coq.Init.Logic_Type <\/pre>\n<p>  \u0412 \u0430\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0446\u0435\u043b\u044f\u0445 \u043c\u044b \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u043c\u0438 \u0438\u0437 \u044d\u0442\u0438\u0445 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a.<\/p>\n<p>  \u041a\u0430\u043a \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e, \u043d\u0438 \u043e\u0434\u043d\u0430 \u0432\u0432\u043e\u0434\u043d\u0430\u044f \u0441\u0442\u0430\u0442\u044c\u044f \u043f\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u043c\u0443 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044e \u043d\u0435 \u043e\u0431\u0445\u043e\u0434\u0438\u0442\u0441\u044f \u0431\u0435\u0437 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f \u0444\u0430\u043a\u0442\u043e\u0440\u0438\u0430\u043b\u0430. \u041c\u044b \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u043e\u0442\u0445\u043e\u0434\u0438\u0442\u044c \u043e\u0442 \u044d\u0442\u043e\u0439 \u0442\u0440\u0430\u0434\u0438\u0446\u0438\u0438 \u0438 \u043d\u0430\u043f\u0438\u0448\u0435\u043c \u0441\u0432\u043e\u0439 \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 \u0444\u0430\u043a\u0442\u043e\u0440\u0438\u0430\u043b \u0441 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438.<\/p>\n<h4>\u041d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430<\/h4>\n<p>  \u0418\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u044e\u0442\u0441\u044f \u0432 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0435 \u043f\u043e\u0432\u0441\u0435\u043c\u0435\u0441\u0442\u043d\u043e. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430 \u0441 \u043f\u043e\u0437\u0438\u0446\u0438\u0438 \u0442\u0435\u043e\u0440\u0438\u0438 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432 \u0432\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/latex.codecogs.com\/gif.download?O&amp;space;=&amp;space;\\emptyset\\\\&amp;space;S(n)&amp;space;=&amp;space;n&amp;space;\\cup&amp;space;\\left&amp;space;\\{&amp;space;n&amp;space;\\right&amp;space;\\}\" alt=\"image\"\/><\/p>\n<p>  \u0410\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0437\u0430\u0434\u0430\u0442\u044c \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430 \u0432 Coq. \u0414\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043d\u0435 \u0437\u0430\u0441\u043e\u0440\u044f\u0442\u044c \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u043e \u0438\u043c\u0435\u043d, \u0432\u043e\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u0441\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u043e\u0439 \u043c\u043e\u0434\u0443\u043b\u0435\u0439:<\/p>\n<pre> Module Test1.   Inductive nat : Type :=    | O : nat    | S : nat -&gt; nat.  <\/pre>\n<p>  \u042d\u0442\u043e \u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u0435 \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0447\u0438\u0442\u0430\u0442\u044c \u0442\u0430\u043a:<\/p>\n<ol>\n<li>O \u2014 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e,<\/li>\n<li>S \u2014 \u044d\u0442\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e, \u0438 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0435\u0449\u0435 \u043e\u0434\u043d\u043e \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e: \u0435\u0441\u043b\u0438 n \u2208 N, \u0442\u043e \u0438 S n \u2208 N.<\/li>\n<\/ol>\n<p>  \u041f\u043e\u043b\u044c\u0437\u0443\u044f\u0441\u044c \u044d\u0442\u0438\u043c \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435\u043c \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043b\u044e\u0431\u043e\u0435 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e:<\/p>\n<pre> Eval simpl in (S O). (* ==&gt; 1 : nat *) Eval simpl in (S (S O)). (* ==&gt; 2 : nat *) Eval simpl in (S (S (S O))). (* ==&gt; 3 : nat *) <\/pre>\n<p>  \u0422\u0435\u043f\u0435\u0440\u044c, \u043a\u043e\u0433\u0434\u0430 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430, \u0441\u0430\u043c\u043e\u0435 \u0432\u0440\u0435\u043c\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043d\u0430\u0431\u043e\u0440 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 \u043d\u0430\u0434 \u044d\u0442\u0438\u043c\u0438 \u0447\u0438\u0441\u043b\u0430\u043c\u0438:<\/p>\n<pre> Fixpoint plus (n : nat) (m : nat) : nat :=   match n with     | O =&gt; m     | S n' =&gt; S (plus n' m)   end. <\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u043c\u044b \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u043b\u0438 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u0443\u044e (\u043a\u043b\u044e\u0447\u0435\u0432\u043e\u0435 \u0441\u043b\u043e\u0432\u043e <code>Fixpoint<\/code>) \u0444\u0443\u043d\u043a\u0446\u0438\u044e <code>plus<\/code>, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 \u0434\u0432\u0430 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u0442\u0438\u043f\u0430 <code>nat<\/code> \u0438 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u0442\u0438\u043f\u0430 <code>nat<\/code>. \u0423\u0431\u0435\u0434\u0438\u0442\u044c\u0441\u044f \u0432 \u044d\u0442\u043e\u043c \u043c\u043e\u0436\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u043e\u043c\u0430\u043d\u0434\u044b <code>Check<\/code>:<\/p>\n<pre> Check plus. (* ==&gt; plus : nat -&gt; nat -&gt; nat *) <\/pre>\n<p>  \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0435\u0435 \u0440\u0430\u0431\u043e\u0442\u0443 \u043d\u0430 \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u043e\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0435. \u0412\u044b\u0447\u0438\u0441\u043b\u0438\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f 3 + 2:<\/p>\n<pre> Eval simpl in (plus (S (S (S O))) (S (S O))). (* ==&gt; 5 : nat *) <\/pre>\n<p>  \u041e\u0442\u043b\u0438\u0447\u043d\u043e! \u0412\u0441\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442. \u041d\u043e \u043a\u0430\u043a \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442\u0441\u044f \u044d\u0442\u043e \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442?<\/p>\n<pre> (*  plus (S (S (S O))) (S (S O))     ==&gt; S (plus (S (S O)) (S (S O))) \u0432\u0442\u043e\u0440\u043e\u0439 \u043a\u043b\u043e\u0437 \u0432 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 ==&gt; S (S (plus (S O) (S (S O)))) \u0432\u0442\u043e\u0440\u043e\u0439 \u043a\u043b\u043e\u0437 \u0432 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 ==&gt; S (S (S (plus O (S (S O))))) \u0432\u0442\u043e\u0440\u043e\u0439 \u043a\u043b\u043e\u0437 \u0432 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 ==&gt; S (S (S (S (S O))))          \u043f\u0435\u0440\u0432\u044b\u0439 \u043a\u043b\u043e\u0437 \u0432 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 *) <\/pre>\n<p>  \u0410\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0443\u043c\u043d\u043e\u0436\u0435\u043d\u0438\u044f \u0438 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0435 \u0444\u0430\u043a\u0442\u043e\u0440\u0438\u0430\u043b\u0430, \u0431\u0435\u0437 \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043d\u0435 \u043e\u0431\u0445\u043e\u0434\u0438\u0442\u0441\u044f \u043d\u0438 \u043e\u0434\u0438\u043d \u0443\u0447\u0435\u0431\u043d\u0438\u043a \u043f\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u043c\u0443 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044e:<\/p>\n<pre> Fixpoint mult (n m : nat) : nat :=   match n with     | O =&gt; O     | S n' =&gt; plus m (mult n' m)   end.  Fixpoint factorial (n : nat) : nat :=   match n with     | O =&gt; S O     | S n' =&gt; mult n (factorial n')   end.  Eval simpl in (factorial (S (S (S (S (S O)))))). (* ==&gt; 120 : nat *) <\/pre>\n<p>  <\/p>\n<h4>\u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435<\/h4>\n<p>  \u0414\u043b\u044f \u0437\u0430\u043a\u0440\u0435\u043f\u043b\u0435\u043d\u0438\u044f \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u0430 \u044f \u043d\u0430\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0443\u044e \u0447\u0438\u0442\u0430\u0442\u0435\u043b\u044e \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u0432\u0441\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u044b \u0432 CoqIDE. \u0412 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u0447\u0430\u0441\u0442\u0438 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0440\u0430\u0431\u043e\u0442\u0443 \u0441 \u0431\u0430\u0437\u043e\u0432\u044b\u043c\u0438 \u0442\u0430\u043a\u0442\u0438\u043a\u0430\u043c\u0438 Coq.    \t<\/p>\n<div class=\"clear\"><\/div>\n<\/p><\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"http:\/\/habrahabr.ru\/post\/182748\/\"> http:\/\/habrahabr.ru\/post\/182748\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div class=\"content html_format\">   \t\u0412 <a href=\"http:\/\/habrahabr.ru\/post\/182442\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439<\/a> \u0447\u0430\u0441\u0442\u0438 \u043c\u044b \u043d\u0430\u0443\u0447\u0438\u043b\u0438\u0441\u044c \u0437\u0430\u0434\u0430\u0432\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0435 \u0442\u0438\u043f\u044b \u0438 \u0441\u0442\u0440\u043e\u0438\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043d\u0430\u0434 \u0438\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u043c\u0438. \u0412 \u044d\u0442\u043e\u0439 \u043d\u0435\u0431\u043e\u043b\u044c\u0448\u043e\u0439 \u0437\u0430\u043c\u0435\u0442\u043a\u0435 \u044f \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u044e\u0441\u044c \u043d\u0430 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u0445, \u0447\u0442\u043e\u0431\u044b \u0432\u043d\u0435\u0441\u0442\u0438 \u044f\u0441\u043d\u043e\u0441\u0442\u044c \u0438 \u043d\u0430\u043c\u0435\u0442\u0438\u0442\u044c \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0438\u0435 \u0442\u0435\u043c\u044b \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f.<\/p>\n<p>  \u0420\u0430\u043d\u0435\u0435 \u044f \u0441\u043a\u0430\u0437\u0430\u043b, \u0447\u0442\u043e \u0432 Coq \u043d\u0435\u0442 \u0431\u0430\u0442\u0430\u0440\u0435\u0435\u043a. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435 \u044f \u0441\u043b\u0443\u043a\u0430\u0432\u0438\u043b \u2014 \u0432 Coq \u0435\u0441\u0442\u044c \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u0430\u044f \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0445 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0439. \u041f\u043e\u043c\u0438\u043c\u043e \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0442 \u0438 \u0431\u043e\u043b\u0435\u0435 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0432\u0435\u0449\u0438, \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u044b \u043f\u043e\u043a\u0430 \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u043e\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0442\u044c\u0441\u044f.  <\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-182748","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/182748","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=182748"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/182748\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=182748"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=182748"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=182748"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}