Software Foundations

Prop.v

*** Exercise: 3 stars, optional (R_fact) にて、

That is, if R m n o is true,って書いてあるけど、R m n oは命題なんだから、Trueじゃね？と思う。
でもSoftwareFoundations/coqの世界のなかで、Trueとは、

True : Prop := I : True.

でしかないから、また違うか。
命題が証明可能であることを示す何か、、、
は、よく考えたらあるわけなかった。一般的に命題が証明可能であることを示すことなど出来ないんだった。

しかし、どっか別の場所で命題とbool値は別物ですと書いた口で、「命題〜〜がtrueだったら」とか書くのは止めて欲しい気はする。

その上で、この問題はよく分からん。

しかし、

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0 
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

などの定義が,どんな証明木を作り得るかについてはイメージが湧くようにはなった。
どれも、これくらい簡単ならなあ。

    --------- c1
     R 0 0 0 
    ----------c2
     R 1 0 1
    ----------c2
     R 2 0 2
    ----------c3
     R 2 1 3
    ----------c4
     R 1 0 1

というわけで関係Rは、 m + n = o だ! 今、実際に証明木を書いてみて初めて分かった。(つまり全然分かってなかった。駄目じゃん)

常に手を動かさないとなあ。

ああなるほど。
m + n = o -> R m n o.と
R m n o -> m + n = o. を証明しろってか。
日記書きながら把握。問題文の翻訳が先人の翻訳の丸写しだったので意味が通じてなかった。新版で問題文変わってるわ。直しとこ。