読者です 読者をやめる 読者になる 読者になる

エンジニアですよ!

頑張れ俺くん、巨匠と呼ばれるその日まで

Coq入門 - 4

進捗あまりない。

update · 702639b · totem3/coq-prac · GitHub

全然わからんのでもうImportしたのを使って証明せずに進めているw

できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。

こうなってくると、今後まともにやっていくうえで大事なのはSearchを使いこなすことのような気がしてくるんだけど、不等号系が全然SearchRewriteとか使っても出てこない

このあたりがよくわからない。次使いこなすべきはSearchかなと思った

n <= m -> ~ m < nとかFalseの証明がでてきたけど、これがやっぱりわからない。

Searchを使いこなせるようになるのと、矛盾を示せるようになりたい