[Coq] How to use Record

　Coq で Record を使う方法を調べました。基本的には記述を簡単にする構文糖のようです。これを使うと、事前条件を満たす証明を要求するコンストラクタを簡単に書けます。
　使い方は下記の例を見てもらうのが簡単でしょう。

　まず正の有理数を表すRat型を作りたいと考えます。符号は無視するとして、分母が０で無いことを保証したい、分子分母が既約である事を保証したい、とします。こんな感じに書けます。

Record Rat : Set := mkRat {
  numer : nat;
  denom : nat;
  denom_not_zero : denom <> O;
  irreducible : forall g n d:nat, 
    (mult g n)=numer /\ (mult g d)=denom -> g = S O
}.

Ratで 1/2 を定義したい時はこんな感じになります。まず補題を証明しないと値を作れません。

Lemma two_not_zero : 2 <> 0.
Proof.
  discriminate.
Qed.
Lemma one_two_irred : forall g n d:nat, (mult g n)=1 /\ (mult g d)=2 -> g = S O.
Admitted. (* 証明省略 *)

こうして初めて値を作れます。

Definition half : Rat := mkRat 1 2 two_not_zero one_two_irred.
Print half. (* mkRat 1 2 two_not_zero one_two_irred : Rat *)
Eval compute in (numer half). (* 1 : nat *)
Eval compute in (denom_not_zero half). (* two_not_zero *)

アクセサに見えるnumerなどは単なる関数です、従って同じ名前空間でnumerを他に定義出来ません。

Print numer.
numer = 
fun r : Rat => let (numer, denom, _, _) := r in numer
     : Rat -> nat

Ratに関する帰納法は下記の様になります。

Print Rat_ind.
(* forall P : Rat -> Prop,
       (forall (numer denom : nat) (denom_not_zero : denom <> 0)
          (irreducible : forall g n d : nat,
                         g * n = numer /\ g * d = denom -> g = 1),
        P (mkRat numer denom denom_not_zero irreducible)) ->
       forall r : Rat, P r *)