下の記事では， Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}. という関数を，Coqの証明モードで作りました．ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Pri…

すごくどうでもいい証明です．．Coqを触るのは2年ぶりくらいだろうか… めちゃくちゃ非効率なことをやっていそうなので，皆さんのツッコミをお待ちしています． 前提 セッション型の双対とは，受信の双対が送信，送信の双対が受信という感じで決まっています…