Skip to content

Instantly share code, notes, and snippets.

View mathink's full-sized avatar

m mathink

11 followers · 1 following
View GitHub Profile
@mathink
mathink / from_nand.v
Created December 6, 2015 09:11
回路作って真理値表チェック。間違ってたら型エラー。
Set Implicit Arguments.
Unset Strict Implicit.
Definition True_or_Eq (b: bool) := if b then True else 0 = 0.
Definition I_or_0eq0 (b: bool): True_or_Eq b :=
match b as b' return True_or_Eq b' with
| true => I
| false => (eq_refl 0)
end.
Definition onlyTrue (H: True): True := H.
@mathink
mathink / ideal.v
Last active December 6, 2015 00:35
Module Ideal.
Open Scope ring_scope.
Class spec (R: Ring)(P: R -> Prop) :=
proof {
contain_subst: Proper ((==) ==> flip impl) P;
add_close:
forall x y,
P x -> P y -> P (x + y);
@mathink
mathink / ring.v
Created December 4, 2015 09:56
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
@mathink
mathink / semiring.v
Created December 3, 2015 11:37
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
@mathink
mathink / adv_cal_2015_1205_question.v
Last active December 11, 2015 13:38
0 なのか 1 なのか、そういうのめんどくさいので任意の自然数 N から始まる "自然数" を考えました。循環じゃなくて重複です。つきましては、 加算と乗算を定義し、それらが正しいものであることを証明してみましょう。ついでに可換律と結合律も。http://qiita.com/advent-calendar/2015/theorem-prover で書くのはこれの解説 "ではありません"。
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Arith.
(* Base "から" 始まる "自然数" *)
Inductive number :=
| Base: number
| Next: number -> number.
@mathink
mathink / length_as_natrans.v
Last active November 20, 2015 11:42
length は リスト函手から定数函手への自然変換だよ on Coq.
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.
Class Setoid :=
{
carrier: Type;
equal: carrier -> carrier -> Prop;
@mathink
mathink / algebraic_structure_middle.v
Last active December 7, 2015 01:39
「代数的構造と Coq：破」のためのスクリプト(at Coq8.4pl6)
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
@mathink
mathink / endo_monoid.v
Last active November 17, 2015 11:56
自己函数は合成で以ってモノイドを成すよ。
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Setoids.Setoid Morphisms.
Delimit Scope cat_scope with cat.
Open Scope cat_scope.
Class Setoid :=
{
@mathink
mathink / mpl.v
Last active November 13, 2015 16:23
モナド、命題、証明、ホーアトリプル
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.
Class Setoid :=
{
carrier: Type;
equal: carrier -> carrier -> Prop;
@mathink
mathink / mpl.v
Created November 12, 2015 08:57
モナド、命題、証明、交わり半束
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.
Class Setoid :=
{
carrier: Type;
equal: carrier -> carrier -> Prop;