AnbLnの日記

AnbLn@ぽりえすてるのブログ

Coq-math-ssreflect その1

6月19日 (火)

六月発の更新です、、、、
もっと更新しないと、、、、

Coqの勉強をかねてライブラリの説明を日本語に訳します

これで、しばらく記事の内容を考えなくてすむかな、、



mathcomp.ssreflect.eqtype

このファイルでは二つの基礎的なインターフェースを定義します。

eqType : 決定的な等価性をもつ構造
Equality mixins can be made Canonical to allow generic folding
of equality predicates.

一言:数学のあらゆる対象で等号=は当たり前に定義されている。
あまり難しく考えず=が定義されている対象AをA : eqTypeと宣言するとだけ覚えておくと良い。

subType p : {x : T | p x}に同型な構造。
p: pred T (pred は一項関係)



eqTypeでは次の演算が使えます。
x == y : xとyを比較して一致するならtrueを返す
x == y :> T : xとyをT型として比較して一致するならtrueを返す
x != y : xとyを比較して一致するならfalseを返す
x != y :> T : xとyをT型として比較して一致するならfalseを返す
x =P y :: a proof of reflect (x = y) (x == y); this coerces to x == y -> x = y.

comparable T <-> equality on T is decidable := forall x y : T, decidable (x = y)
comparableClass compT == eqType mixin/class for compT : comparable T.
pred1 a : 一点集合 [pred x | x == a].
pred2, pred3, pred4 : 二、三、四点集合
predC1 a : 一点集合の補集合 [pred x | x != a].
[predU1 a & A] : [pred x | (x == a) || (x \in A) ].
[predD1 A & a] : [pred x | x != a & x \in A].
predU1 a P, predD1 P a == applicative versions of the above.
frel f == f : T -> T に対して、[rel x y | f x == y].
invariant k f == elements of T whose k-class is f-invariant.
:= [pred x | k (f x) == k x] with f : T -> T.

[fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n]
[eta f with a1 |-> e1, .., a_n |-> e_n] ==
the auto-expanding function that maps x = a_i to e_i,
and other values of x to e0 (resp. f x).
In the first form the `: T' is optional and x can occur in a_i or e_i.
おそらく、有限個の元の像を指定する関数.

Equality on an eqType is proof-irrelevant (lemma eq_irrelevance).
The eqType interface is implemented for most standard datatypes: bool,
unit, void, option, prod (denoted A * B), sum (denoted A + B),
sig (denoted {x | P}), sigT (denoted {i : I & T}).
We also define tagged_as u v == v cast as T(tag u) if tag v == tag u, else u.

> We have u == v <=> (tag u == tag v) && (tagged u == tagged_as u v).



subTypeの演算はまた今度


参考: mathcomp.ssreflect.eqtype