Hatena Blog Tags
はてなブログ トップ
Coq
このタグでブログを書く
言葉の解説
ネットで話題
関連ブログ

Coq

(コンピュータ)
【こっく】

INRIAで開発されている定理支援証明器。
Gallinaというプログラミング言語で定義を記述し、それに関する性質を証明する支援をしてくれる。

文法はOCamlによく似ている。

このタグの解説についてこの解説文は、すでに終了したサービス「はてなキーワード」内で有志のユーザーが作成・編集した内容に基づいています。その正確性や網羅性をはてなが保証するものではありません。問題のある記述を発見した場合には、お問い合わせフォームよりご連絡ください。
K's Atelier•5ヶ月前

Coq and Lean

Coq Proof AssistantとLean Programming Language，やりたいことは基本的に同じだが，後発のLeanの方が洗練されているといえなくもない。どちらの言語も初めての人には絶対わけわからん言語だ。ちょうどChatGPTがあることだし，こういう未知の言語は生成AIに任せる。同一のTheoremを証明する。# Coq実行環境はこちら。 jsCoq – The Coq Theorem Prover Online IDE (* Import the standard library for natural numbers *) Require Import Coq.Ar…

#Mathematics#Coq#Lean

ネットで話題

もっと見る
469ブックマークCoqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！eh-career.com
78ブックマーク【公式】ルコックスポルティフ｜le coq sportifstore.descente.co.jp
71ブックマークWelcome! | The Coq Proof AssistantCoq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of pro...coq.inria.fr
66ブックマークCoqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQqnighy.hatenablog.com
55ブックマーク誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)m-hiyama.hatenablog.com
51ブックマーク【SOU・SOU le coq sportif より】2506:高島縮長袖シャツ | SOU・SOU homepagewww.sousou.co.jp
47ブックマークなぜCoqが重要か結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhD...proofcafe.org
34ブックマークCoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017CoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017 2/48 元ネタ ● 既発表の話です ● そのうち論文が出ます ● Safe Low-level Code Generation in Coq using Monomorphization and Monadification Akira Tanaka, Reynald Affeldt, Jacques Garrigue IPSJ SIGPRO 114, ...www.a-k-r.org
33ブックマーク疲れが抜けない「副腎疲労」、回復助けるサプリとは　ギブアップ寸前ならCoQ10とαリポ酸 - 日本経済新聞www.nikkei.com

関連ブログ

K's Atelier•1年前

Coq Proof Assistant

Coqというのは定理証明支援系。数学の証明を形式的にチェックしてくれるツールだ。 数学書を漫然と眺めていても仕方ないので，Coqのコードに書きなおしながら読めばいいんじゃないか，と思いついた。「演習 群・環・体 入門」は，本来整数の代数的定義がこの前にあって，「この公理系だけから証明しようね」という流れなのだが，今回は既存Libraryで端折ってしまった。 「はじめての数理論理学」は著者がCoqの授業もやってらっしゃるのか，非常に読みやすい，んだけど私がCoqに不慣れなせいできれいに証明が書けてない。こういう証明をいきなり書き下すのは，以前ならとんでもない苦労が必要だった。 今はChatGPT…

#Coq
::Eldesh a b = LEFT a | RIGHT b•3年前

Coqのモジュールの基本機能

あけましておめでとうございます。今年もよろしくお願いします。 Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。 リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structure です*1 。 Coqのモジュールは(S)MLのモジュールに近い機能で、型とその実装をひとまとめにして名前を付けることができます。 実はリファレンスを読んだだけではどんな機能か分からなかったので分かったことをこの記事にまとめます(多分構文はOCamlに近いけどワタシ用のメモなので随所でSMLと比較しています)。 基本 SMLで言う…

#Coq
::Eldesh a b = LEFT a | RIGHT b•3年前

CoqのマニュアルのTermの章を翻訳した

Coq v8.8.2 の Term の章を翻訳しました。 この章では Gallina の項の構成について説明しています。 恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔なので分かり易いです(それでも難しいんですが…)。 あと分かりにくいと言ったら型キャストの部分で、term とかterm は項目が存在する割には全く説明が無いに等しいので何のことやら全然分かりません。これはヒドイ。 他に気になったところでは cofix についての説明で、以下の説明に依るとこれは相互(構造)再帰ではないようなんですね。…

#Coq
::Eldesh a b = LEFT a | RIGHT b•3年前

mathcomp bigop 概要を和訳

ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。ssrcoq9.v の中では Notation であるはずの \big[op/idx]_～ が Definition になっていたりして混乱しますが、直接定義だけを追うより全体像(=この文書の内容)を把握した方が早かったようです。 (といっても Tips の内容は全然分かってませんが…) 概要 This file provides a generic definition for iterating an operator over a…

#Coq#ssreflect
::Eldesh a b = LEFT a | RIGHT b•3年前

opamでmathcompをインストールした

最近 coqtokyo 第7回Ssreflect勉強会 に参加しています。 隔週で火曜日にやっているので是非。 もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。 さっそく opam で mathcomp をインストールしようとしたところ、以下のようなエラーが出ました。 eldesh@hostname:~/work/garrigue.git$ opam install coq-mathcomp-ssreflect The following actions will be performed: ∗ install coq-mat…

sawaragikunkun’s diary•4年前

今日の証明

現代数学概説Ⅰ 1章 $2 例題2 以下を示せ。 1) Γ(x) ∍y ⇔ Γ.exp-1(y)∍x. 2) A'⊆A⊆M とする時 Γ(A')⊆Γ(A). 3) B'⊆B⊆N とする時 Γ.exp-1(B')⊆Γ.exp-1(B). 4) A⊆DomΓ とする時 A⊆Γ.exp-1 (Γ(A)). 5) B⊆ImΓ とする時 B⊆Γ(Γ.exp-1(A)). 注) .exp-1はマイナス1乗を示し、Γ.exp-1(x)はΓ(x)の逆対応を示す。 ============================== 1) Γ(x) ∍y ⇔ Γ.exp-1(y)∍x. 対応の定義により Γ=(G, M…

#Coq#証明#数学
sawaragikunkun’s diary•4年前

今日の証明

現代数学概説Ⅰ 1章 $1 例題9 M⊆M', N⊆N⇒MxN⊆M'xN'であって、 (MxN).c(Ωmn) = (M.c(Ωm)xN') ∪ (M'xN.(Ω=N')). 注) AxBはA,Bの直積を表す。A.c(Ωxx)はAの補集合で(Ω)内は母集合を表す。 Ωmn=M'xN', Ωm=M', Ωn=N'. ---------------------------------------- a) 補集合の定義より、 (MxN).c = (M'xN')-MxN. b1) (M.c(Ωm)xN') =(M'-M)xN' = M'xN'-MxN' b2) (M'xN.c(Ωn)) =M'x(N'…

#Coq#証明#数学
sawaragikunkun’s diary•4年前

今日の証明

現代数学概説Ⅰ 1章 $1 例題4 以下a)b)c)を示せ。 a) M ∪ (M ∩ N)=M, M ∩ (M ∪ N) = M. b) M ⊆ N <-> M = M ∩ N <-> N = M ∪ N. c) M ⊆ M' <-> M ∪ N ⊆ M' ∪ N, M ∩ N ⊆ M' ∩ N. ----- coq 証明 a) Theorem math_1_1_exp_4a1: forall (M N:Ensemble M), M ∪ (M ∩ N) = M.Proof. intros M N. apply Extensionality_Ensembles. unfold Same_set.…

#Coq#定理証明#数学