いつものように $ brew update && brew upgrade してたら coq の version が 8.9.0 になってしまい、今まで書いていたコードが動かなくなったので、coq の version を 8.8.2 にします。 ほとんど ↓ の記事を見ながらやりました。 参考: Homebrew で旧バージョンのパッケージをインストールしたい brew でバージョン指定してインストールする方法 ローカルに Coq がある場合 $ brew info coq を実行して version 8.8.2 がローカルに残っているなと思ったら $ brew switch coq 8.8.2 で coq の version を変えれるらしいです。 ローカルに Coq がない場合 まず、 $ cd /usr/local/Homebrew/Library/Taps/homebrew/homebrew-core/Formula $ git log coq.rb で適当に指定の version を見つける。 commit ef92c34e061cb99920f7ae05d3ba205fccc5f1b8 Author: BrewTestBot <homebrew-test-bot@lists.sfconservancy.org> Date: Wed Oct 31 17:08:20 2018 +0000 coq: update 8....

はじめに SICPを読んでたらフェルマーテストについて書いてあって、ほんとにこれ速いのかやってみようと思った話です。 ソースはfermat_test.hsからダウンロード! フェルマーテストとは フェルマーの小定理はご存知ですよね？ $p$を素数のとき、$a$を$p$と互いに素な整数に対して、 $$a ^ p \equiv a \pmod{p}$$ が成り立つ。 これの対偶を考えます。 整数$n$について、$n$と互いに素な整数$a$に対して、 $$ a ^ n \not \equiv a \pmod{n} $$ が成り立つとき、整数$n$は合成数である。 これによって、ある数が素数であることは示せないが合成数であることを速く示すことはできます。 実装 部品を 1 つ 1 つ揃えていきます。 互いに素 最小公倍数を求める関数を考えます。 gcd' :: Integer -> Integer -> Integer gcd' n 0 = n gcd' n m = gcd' m (n `mod` m) これを用いて、 gcd' n m == 1 とすれば$n, m$は互いに素です。 (Haskell には標準で gcd があるのでそれを使っても良い) $a^{n-1} \pmod{n}$を求める いわゆる、$a^7 = a * (a^3)^2 = a * (a * a^2)^2$として計算量をへらすやつを使います。 途中で$\pmod{n}$を挟みます。...

目的 代数入門―群と加群 を読んでいたら自然数が加法,乗法について可換モノイドだと書いてあった気がするので、それを Coq/SSReflect で示します。 (実際はSoftware Foundations の第一章を SSReflect 使って解いただけ。) 可換モノイド S が可換モノイドとは 結合律 $$ \forall x, y, z \in S, (x \cdot y) \cdot z = x \cdot (y \cdot z) $$ 単位元の存在 $$ \exists e \in S, \forall x \in S , e \cdot x = x \cdot e = x $$ 可換 $$ \forall x, y \in S, x \cdot y = y \cdot x $$ を満たすことである。...

直観論理とは Coq は直観論理で許される推論規則で演繹を行う。 直観論理の説明はWikipediaにある。 簡単に説明すると、私達が普通に数学で用いている論理は古典論理で、直観論理は古典論理から排中律を除いたものである。 排中律を除くことで二重否定の除去など、古典論理では証明できるが直観論理では証明できないものがある。 Coq ではClassicalというライブラリを Import すると古典論理を使えるようになる。 詳しい説明は情報科学における論理を読むと良い。 この記事では、直感論理と古典論理の微妙な違いを集めて遊ぼうと思います。 直感論理で示せる命題 二重否定をつける Lemma PPNN : forall p : Prop, p -> ~~p. Proof. intros. intro. apply H0. trivial. Qed. 三重否定を否定にする Lemma NNN : forall p : Prop, ~~~ p -> ~p. Proof. intros. intro. apply H. intro. contradiction. Qed. 対偶の片方 Lemma Cont : forall p q : Prop, (p -> q) -> (~q -> ~p). Proof. intros. intro. apply H0....

Root なしで人権を得る方法です。 Tmux をビルドする。 こんな素晴らしい記事がある。 これをコピペして実行。 linuxbrewを用いる。 以下を~/.bashrcに追加して再度ログイン。 if [ ! -r ~/.linuxbrew ]; then git clone https://github.com/Linuxbrew/brew.git ~/.linuxbrew fi if [ -r ~/.linuxbrew ]; then export PATH="$HOME/.linuxbrew/bin:$HOME/.linuxbrew/sbin:$PATH" export MANPATH="$MANPATH:$HOME/.linuxbrew/share/man" export INFOPATH="$INFOPATH:$HOME/.linuxbrew/share/info" #export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$HOME/.linuxbrew/lib" fi

外延性の公理から集合の等号に対して同値関係を示します。(Coq で) 外延性の公理とは A, B を任意の集合とするとき、もし任意の集合 X について「X が A の要素であるならば、そのときに限り X は B の要素である」が成り立つならば、A と B は等しい。 外延性の公理から引用。 ∈ と=を定義する Section Axiom_Of_Extensionality. Variable Var : Type. Variable In : Var -> Var -> Prop. Variable Eq : Var -> Var -> Prop. (* ここにコードを書く *) End Axiom_Of_Extensionality. ∈ を In、=を Eq とした。 同値関係とは 反射律: a = a 対称律: a = b ⇒ b = a 推移律: a = b ∧ b = c ⇒ a = c 同値関係を参考。...

随時更新していきます。 通常編 とりあえず Atom をインストールしたら入れるプラグイン atomic-emacs Atom で Emacs のキーバインドを使う。 japanese-menu 設定を日本語化 platformio-ide-terminal Ctrl-`で下からターミナルが出てくるようになる。 project-manager project を管理できるようになる。 LaTex 環境編 tex を Atom で書くときのプラグイン一覧。 language-latex シンタックスハイライト latex tex のコンパイル latexer 補完 pdf-view pdf を見れるようになる。 感想 Atom で Coq やりたい。 Atom では Vim より Emacs のが使いやすい。

はじめに Coq で集合を扱う標準ライブラリEnsemblesの再開発を行います。 勉強のため auto.を使わないで証明を行います。 集合論 Section Ensembles. (* ここにコードを書く *) End Ensembles. 集合とは 1 変数の述語を用いて集合論を定義する。 Variable U : Type. Definition Ensemble := U -> Prop. U は述語の変数の型であり、Ensemble は U を受け取って命題を返す 1 変数の述語である。 今回は Ensemble を集合とする。 ∈ を定義 元 a が集合 A に含まれるということは、変数 a と 1 変数の述語 A について A(a)ということである。 例): 「ソクラテスが人間という集合に含まれる。」は、「ソクラテスが人間ある。」ということである。 Definition In (A : Ensemble) (a : U) : Prop := A a. Notation "a ∈ A" := (In A a) (at level 55,no associativity)....

Hugo とは オープンソースの軽量ブログジェジェネレーターです。 Markdown で書くことが出来て楽です。 Hugo の使い方 インストール方法 brew install hugo ブログの作成 hugo new site hugo 記事の作成 hugo new post/fuga.md localhost でテスト hugo server を実行し、http://localhost:1313/ にアクセス。 この時は public には何も作成されない。 ページを作成する。 hugo を実行すると public にサイトが作成される。 git で管理する方法 HUGO でブログ作成 → GitHub Pages で公開する手順に git のサブモジュールを用いて管理する方法が書いてある。 素晴らしいのでやると良い。 感想 GitHub Pages でブログができてドメイン代しかかからないのが素晴らしいと思いました。 git で push すると更新なのでネットがないところでも blog が書けるのもいいと思います。 Hexo もいいけど npm で拡張するとかめんどくさいから Hugo が楽で良いと思った。 テーマを変えるのも楽だけど、私のセンスがないのでこのブログはダサい。