coqでドモルガン 述語論理編

述語論理で、ドモルガンに相当すんのが以下の4つ
¬(∃x,P x) -> ∀x,¬ P x
∀x,¬ P x -> ¬(∃x,P x)
∃x, ¬ P x -> ¬(∀x,P x)
¬(∀x,P x) -> ∃x, ¬ P x

例によって最後のやつが排中律or二重否定則とかないと証明出来ないらしい。

Require Import Coq.Logic.Classical.
Check NNPP. (* =>  : forall P : Prop, P -> ~ ~ P -> P *)
Lemma JDM2 (T:Type) (P: T -> Prop) :
  ~(forall x, P x) -> exists x, ~(P x).
Proof.
  move=> Hyp.
  apply: NNPP.
  move=>Hnen.
  apply: Hyp.
  move=> x0. apply: NNPP.
  move=>Hnen2. apply: Hnen. exists x0. by [].
Qed.

exists x, ~(P x). に対して二重否定則適用&コンテキストに
~ (exists x, ~ P x)を上げる
現状のサブゴールに対して、最初の仮定 ~(forall x, P x) を適用
forall xをコンテキストにx0として上げる。
現状のサブゴール P x0に対して再び二重否定則適用
~~P x0
このサブゴールは
コンテキストの仮定 ~ (exists x, ~ P x)
と大体同じものなので証明終了。

テキトーだ。
何書いてるか分かんねえ....

存在量化子 exのコンストラクタ ex_introの読みかたがあやふやだった。
P -> Qは、forall _ : P, Qの糖衣構文であるというのを
ようやく。何度もSoftware Foundationを読んで来たのに、今頃、
理解することが出来た。
よきかなよきかな。

coqでドモルガン 命題論理編

命題論理ドモルガン4兄弟
¬(A ∨ B) → ¬A ∧ ¬B.
¬A ∧ ¬B → ¬(A ∨ B).
¬A ∨ ¬B → ¬(A ∧ B).
¬(A ∧ B) → ¬A ∨ ¬B.

のうち、直観主義論理の範囲で証明出来ないらしい
¬(A ∧ B) → ¬A ∨ ¬B.の証明。
排中律を前提とする。

排中律を使って、A∨¬AとB∨¬Bをコンテキストに加えて、場合分け。
AかつBのときだけ、¬(A ∧ B) の前提が使われる。

ssreflectの本を読み始めたので、SSReflectのスタイルで。

Hypothesis ExMidLaw : forall P : Prop, P \/ ~P.
Lemma Demorgan1_1 (A B : Prop) :  ~(A /\ B) -> ~A \/ ~B.
Proof.
  move: (ExMidLaw A) => HAnA.
  move: (ExMidLaw B) => HBnB.
  case: HBnB.
  -case:HAnA. 
   +move => HA HB HnAB. case: HnAB.  by [].
   +move => HnA HB HnAB. apply: or_introl HnA.
  -move => HnB HnAB. apply: or_intror HnB.
Qed.

自分でも騙されている感じしかしない。

述語論理版はどうやったらいいのか良くわからん。

filter_challenge_2

夏休みに「software foundation」を読み返している。もう読み始めて何年たってるのか。前読んでた時から半年とか空くと全部忘れてるのでまた読み直しが発生して、とかの悪循環。どんどん後退している。年も食ってるし。

以前の自分の解答で諦めてたらしい(諦めたことも忘れている。)filter_challenge_2が出来たっぽいので久し振りにBLOGを書く。

問題はこうだ。

[filter] の振る舞いに関する特性を別の切り口で表すとこうなります。
「[test] の結果が [true] なる要素だけでできた、リスト [l] のすべての部分リストの中で、[filter test l] が最も長いリストである。」これを形式的に記述し、それを証明しなさい。

filterは各要素が満たすべき関数とリストを渡して、リストから関数のチェックをパスする要素だけ集めたリストを返すよくあるやつ。

今回も最初案の定全く分からなかったが、問題を分割して考えたら上手く行けそうな感じがした。

まず、

「[test] の結果が [true] なる要素だけでできた、リスト [l] のすべての部分リスト

これを形式化、つまり上記のリスト全てを構成する方法を考える。
二つの空リストから出発して、各リストに要素を上記の条件を満たすように加えていくのである。そうすれば、上記のリストを全て構成することが出来る。
このやりかたは、偶数を構成する命題や、二つの数字を比較する関係や正規表現などなどで、IndProp.vの章まででいろいろやっているのでなんとなく分かる。

Inductive part_test_list {X}  (test : (X -> bool)) : list X -> list X -> Prop :=
| ptl_nil : part_test_list test [] []
| ptl_true : forall l1 l2 x, part_test_list test l1 l2 -> test x = true -> part_test_list test (x :: l1) (x :: l2)
| ptl_any : forall l1 l2 x, part_test_list test l1 l2 -> part_test_list test (x::l1) l2.

最初testを各枝のforallに入れていて訳分かんなくなった。

つぎに、「〜が最も長い」ということを形式化する。

なんかのリストの集合の要素lの長さは、HOGEの長さを越えない。

forall l, なんかlが満たすべき属性 ->  length l <= length HOGE.

という感じで行けそう？

という感じで以下になる。

Lemma filter_challenge_2 : forall X test (l1 l2 : list X),
  part_test_list test l1 l2 -> (length l2) <= (length (filter test l1)).
Proof.
Admitted.

解答をネットに上げてくれるな。と書いてあるので最後までは書かない。
証明はそんなに難しいものではない。普通の帰納法で行ける。

JS Promise Async Await

jsの比較的新しい機能のPromiseとasync/awaitを使って非同期関数を同期関数っぽくみせかけることが出来る。

たとえば、jquery uiのconfirmダイアログをwindow標準のconfirmと似たような使い勝手にすることも一応可能。

function myconfirm_promise() {
  var promise = new Promise(function(resolve, reject) {
    $("#dialog").dialog({
       modal:true,
       buttons: [
         {text: "OK", click: function() {
            resolve(true);
         }},
         {text: "Cancel", click: function() {
            resolve(false);
         }},
       ]
    });
  });
  return promise;
}

function async hoge() {
   var ret = await myconfirm_promise();
   if (ret) {
      // OKが押された
   } else {
      // Cancelが押された。
   }
}

一応可能と言ったのは、完全に同じではないから。
同期関数ぽく見えてるだけで、function async hoge()関数自体は非同期関数である。
つまり、

hoge();
//この部分の続きの処理はhoge()の呼出のあと普通に実行されてしまう。
。。。
var ret = await myconfirm_promise();

の呼びだしが、

var ret = confirm();

だった場合、
hoge関数は同期関数になり、OK/Cancelが押されるまで、以降の処理の実行は完全にブロックされる。

コンパクト定理

スマリヤンの数理論理学の本を斜め読みしてて、コンパクト定理のとこでわけが分からなくなって放置してたんだけど、最近読み直して、なんとなくその時なぜ分からないと思ったのかが分かったような気がする。

本の構成上、その直前まで木について説明が続いてて、その後唐突に集合のコンパクト定理の話になってたせいだと思われ。

木に関しては、どうもこのコンパクト定理ってのが上手く嵌らない気がして、わけが分かんなくなってたようだ。
当たり前だ。木の話じゃないんだから。

しかもコンパクト定理を構成的に説明するために、クラブという別の例えが出て来てそれが混乱に拍車がかかっていた。

ちょっと違うかもしんないけど、
クラブになる = (ある)性質(P)を満たしている。
最大クラブ = 最大部分集合

集合Aとその部分集合の性質Pがコンパクトであるとは、
Aの任意の部分集合Sが性質Pを満たすことと、Sの有限部分集合全てがPを満たすことが同値であることを言う。

大麻について

麻薬使用者を憐んであげますというエントリ
http://fujipon.hatenablog.com/entry/2016/10/27/011319

ブックマーク
http://b.hatena.ne.jp/entry/fujipon.hatenablog.com/entry/2016/10/27/011319

大麻取締法の時効は七年だそうで、もう時効だから書きますが、昔旅行に行ったときに数回吸わせてもらいました。(諸外国でなかば合法化されてる中で大麻取締法には国外犯規定が付け加えられました。原理的には外国で所持しただけで罪になるようです。外国で使っただけの人が掴まったという例は知りません)

大麻がどんな感じなのかは私の個人的な(20年も前の)ほんの数回の体験に過ぎませんが、少し書いてみようかと思いました。なんつーか擁護にしてもアルコールより毒性が低いとか悪評の否定ばかりで、メリットそのものが書かれてないように感じたので。


大麻樹脂をタバコに少量混ぜて紙に巻いたものを経験者の人に作ってもらってそれを吸いました。

吸うと体全体が軽く脱力したように感じます。感覚はアルコールと違って鈍くはならず、やや鋭くなったような不思議な感じ。
そして、気分が拡大される感じがします。楽しい気分はより楽しく、不安な気分はより不安な感じになるのかと。

不安な気分(例えば、俺は麻薬を吸ってしまった。もう犯罪者だ。元には戻れないだー。みたいな)で吸うとそいつが拡大されて非道い目(バッドトリップ？)にあうんでしょうかね。私は教えて一緒に吸ってくれた人がよかったのか、そういうのにはなりませんでした。


ほんの数口でしたが、効果は一時間くらいはあったと思います。私はそのまま寝ました。

幻覚とかは当然見えませんでした。見たい人は、やったことありませんが、LSDとかマジックマッシュルームとかやればよいのではないでしょうか。(ほぼ全ての国で違法だと思いますが・・・)

酒は最初アッパーとして働き、飲みすぎるとダウナーみたいになって潰れます。大麻は、基本ダウナーなので、最初から潰れてるように見えるのが、酒飲みからすると違和感があるんでしょうか。


まあ私の語れるメリットといったところで、大麻を吸った時の感覚が全てですが。
酒を飲んだことのない人に酒の味や酔った感覚を説明するのが難しいように、個人的な感覚を説明するのは難しいですね。
酒と違って理性を飛ばさないので、酒を大麻に少しでも置き換えたら、酒に酔った上での犯罪(駅員さんへの暴力とか猥褻行為だとか)は減るような気はします。

酒と同様に人によって、合う合わないは当然あると思います。悪い先入観が少しでも少なくなれば、楽しめる人は酒よりも多いのではないかと思うんですが・・・

それでもバッドトリップすることも当然あるでしょうし、医療用に無条件に使えるのかどうかは疑問です



旅行から帰ったあとは、あの美味しかった料理をもう一回食べたいな。みたいな感じで思うこともありますが、大麻を吸ったことはありません。基本引きこもりなので、クラブとか行かないし、吸う知り合いもいません。北海道に自生してるとか言うけど、取りに行くの面倒臭いし。そもそも日本で吸うのは犯罪です。

嗜好品として解禁されて、手が届く値段であれば、またやってもいいかな。とは思いますが、解禁のために運動とかすんの面倒だし、ないならないでまあいいし。

つまるところ、経験した側から見ると、単なる酒よりマシな嗜好品が特に根拠もなく規制されてるようにしか見えないんですね。

諸外国が解禁の流れですし、この10〜20年くらいでまた大麻を巡る認識も変わるような気もしてます。外国行って大麻に触れるひともさらに多くなってるでしょうし。老後の楽しみとして取っておきます。

大昔に少し経験しただけの素人が主観だけを頼りに書いてるエントリーですので間違いも多々あると思います。いろいろご指摘いただければ幸いです。


まあこんな過疎ダイアリー見てる人いないわな。増田にでも転記するか…