zehnpaard https://blog.hatena.ne.jp/zehnpaard/ Arantium Maestum https://zehnpaard.hatenablog.com/ Coq Logical Foundationsを進めがてら、基礎固め的に簡単な命題論理の命題を証明してみたいと思ってググったらこんなスレに遭遇した： coq.discourse.group このうちの最初の問題が簡単ながらもいくつか面白い点があったのでメモ。 証明する命題： Lemma a1 : forall (A B C D : Prop), (A -> B) -> (A -> C) -> (B -> C -> D) -> (A -> D). まずは命題と仮定を導入しておく： Proof. intros A B C D. intros Hab Hac Hbcd Ha. この時点での仮定とゴールは以下… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fzehnpaard.hatenablog.com%2Fentry%2F2021%2F04%2F12%2F081526" title="Coqの演習問題、あるいはifとapplyについて - Arantium Maestum" 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 2021-04-12 08:15:26 rich https://zehnpaard.hatenablog.com/entry/2021/04/12/081526 1.0 100%