Coq
諸事情により、本シリーズを終了します。
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る @suharahiromichi この文書のソースコードは以下にあります。 https:/…
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る @suharahiromichi この文書のソースコードは以下にあります。 https:/…
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る @suharahiromichi この文書のソースコードは以下にあります。 https:/…
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る @suharahiromichi この文書のソースコードは以下にあります。 https:/…
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る @suharahiromichi この文書のソースコードは以下にあります。 https:/…
定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見るこの本を練習しようと思った。 Schemeでやるのはつらいな〜と思ってい…
Coqでやってみた。 Require Import Arith. (* ring_simplify *) Require Import Omega. (* omega *) Theorem t1 (x:nat) : 3*(x+1) < 5*(x+1). Proof. omega. Qed. Theorem t1' (x:nat) : 3*(x+1) < 5*(x+1). Proof. induction x. simpl. auto. (* View -> Q…
前回の続き。 assert((n>1->n=n+0)->(S n>1->n=n+0)). より assert((n>1->n=n+0)->(S n>1->S n=S n+0)). のほうがエレガントですかね。例1 Lemma l3_2: forall (n:nat), n>1 -> n=n+0. Proof. intros. induction n. reflexivity. (* ここがポイント *) asser…
これは楽勝。 Lemma l2: forall (n:nat), n=n+0. Proof. intros. induction n. reflexivity. simpl. f_equal. apply IHn. Qed. しかし式をforall (n:nat), n>1 -> n=n+0.にすると、 普通にやると、ゴールがn>1、仮定がS n>1となりうまくいきません。 そこで…
2010-09-19 - ひとり勉強会の練習問題。 ||<Require Import Arith Omega. Fixpoint sum (n: nat) := match n with | O => 0 | S m => n + sum m end. Theorem Sum_of_nat: forall (n m: nat), m = 2 * sum n -> m = n*(n+1). Proof. intro n. induction n. (以下は練習問題) なんとか解けたけどかなり苦戦した。三日かかった。 Require </require>…
コラッツ予想の証明にギャップがあったので修正しました。 まだpre版で、日本語と英語が混ざってて気持ち悪いですが、 良かったら見てみてください。 Coqも使っています。collatz_CA_2pre_jp.pdf - Google ドライブ
カリーのパラドックス（英: Curry's paradox）は、素朴集合論や素朴論理学で見られるパラドックスであり、自己言及文といくつかの一見問題ない論理的推論規則から任意の文が派生されることを示す。名称の由来は論理学者のハスケル・カリーから。 カリーのパ…
