kikx https://blog.hatena.ne.jp/kikx/ 菊やんの雑記帳 https://kikx.hatenadiary.org/ Coq assert form ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。 ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。中間結果 form を指定すると、サブゴールにformが追加されて、元のゴールにはformが仮定として追加される。 < Goal forall x y: Z, x>=0 -> x*x>y*y -> x-y>0. < intros. 1 subgoal x : Z y : Z H : x >= 0 H0 : x * x > y * y ======================… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkikx.hatenadiary.org%2Fentry%2F20070415%2F1176610896" title=" - 菊やんの雑記帳" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2007-04-15 13:21:36 rich https://kikx.hatenadiary.org/entry/20070415/1176610896 1.0 100%