Hatena::ブログ(Diary)

memo

2018-05-13

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

00:09

述語論理で、ドモルガンに相当すんのが以下の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を読んで来たのに、今頃、

理解することが出来た。

よきかなよきかな。

2018-05-06

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

23:27

命題論理ドモルガン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.   
   

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

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

2017-08-23

23:59

一年前のものを見直すとひどいな。InductiveとDefinitonの区別が明らかについてないのとか。

というか、なんで今区別つくようになってんだ。自分。

2017-08-17

filter_challenge_2

19:09

夏休みに「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.

解答をネットに上げてくれるな。と書いてあるので最後までは書かない。

証明はそんなに難しいものではない。普通の帰納法で行ける。

2017-04-21

JS Promise Async Await

23:32

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が押されるまで、以降の処理の実行は完全にブロックされる。

Connection: close