天泣記

2021-03-11 (Thu)

#1 Coq/SSReflect/MathComp で整数を使う

Coq で整数というと標準の ZArith ライブラリが提供している Z 型があるが、 これは SSReflect の eqType 対応がなくて == が使えないとか、 SSReflect 的ではない。

自分で eqType 対応するのは可能ではあるだろうけど、 SSReflect 的な整数が提供されていないわけがないだろうということで探すと、 mathcomp/algebra/ssrint.v にあった。

中を見ると以下の型が定義されていて、Z 型とは違う型のようだ。

Variant int : Set := Posz of nat | Negz of nat.

ちょっと試してみると、以下のように使える模様。

From mathcomp Require Import all_ssreflect ssralg ssrint.

Open Scope int_scope.
Open Scope distn_scope.
Open Scope ring_scope.

Compute 2%:Z. (* 2, Posz (S (S O)) *)
Compute -2%:Z. (* Negz 1, Negz (S O) *)
Compute 1%:Z + 2%:Z. (* 3 *)
Compute 1%:Z - 3%:Z. (* Negz 1 *)
Compute 2%:Z * 3%:Z. (* 6 *)
Compute 3%:Z ^ 2%:Z. (* 9 *)
Compute `| 1%:Z - 2%:Z |. (* 1 : nat *)

Check 1%:Z = 2%:Z :> int. (* @eq int (Posz (S O)) (Posz (S (S O))) *)
Check 1%:Z == 2%:Z :> int. (* @eq_op int_eqType (Posz (S O) : int) (Posz (S (S O)) : int) *)
Check 1%:Z != 2%:Z :> int. (* negb (@eq_op int_eqType (Posz (S O) : int) (Posz (S (S O)) : int)) *)
Check 1%:Z <> 2%:Z :> int. (* not (@eq int (Posz (S O)) (Posz (S (S O)))) *)

2021-03-12 (Fri)

#1 Coq/SSReflect/MathComp の整数の比較

比較の使い方がよくわからなかったのだが、ssreflect/order.v を使えて、 (x < y)%O というような感じに記述できるようだ。

Check (2%:Z < 3%:Z)%O. (* @Order.lt ssrnum.ring_display int_porderType (Posz (S (S O))) (Posz (S (S (S O)))) *)
Compute (2%:Z < 3%:Z)%O. (* true *)

[latest]


田中哲