Coq

はじめに 久々に Coq で遊びたくなったので、M1 Mac にインストールしてみた。 最近の Coq は VSCode で書くのが主流？らしいが、今回は Emacs + Proof-General で環境構築を行う。 環境構築の方法 基本的にbrewやmelpaなどの package 管理システムになるべく依存した形で環境構築を行う。 はじめに、Coqのインストール(–build-from-source をつけないとcoqtop実行時にエラーが出た。) brew install coq --build-from-source GUI 版 Emacs のインストール brew install emacs --cask Emacs の設定 次は Emacs の設定を行う。 Emacs の設定ファイルは~/.emacs.d/init.elに記載する。 まずはmelpa(Emacs のプラグインのパッケージマネージャー)のセットアップを行う。 ~/.emacs.d/init.elに以下を記載し、 (require 'package) (let* ((no-ssl (and (memq system-type '(windows-nt ms-dos)) (not (gnutls-available-p)))) (proto (if no-ssl "http" "https"))) (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)) (package-initialize) emacs を起動して...

いつものように $ 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....

目的 代数入門―群と加群 を読んでいたら自然数が加法,乗法について可換モノイドだと書いてあった気がするので、それを 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....

外延性の公理から集合の等号に対して同値関係を示します。(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 同値関係を参考。...

はじめに 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)....