整数の定義を素朴なものに戻した。 --（succ (succ (pred zero))などが有効、という弱点がある） data Z : Set where zero : Z succ : Z -> Z pred : Z -> Z それに加法、反数、乗法を定義したものがこちら。 整数の素朴な定義この整数が環をなすことをAgda…

定理証明手習い作者: Daniel P. Friedman,Carl Eastlund,中野圭介出版社/メーカー: ラムダノート発売日: 2017/10/23メディア: 単行本（ソフトカバー）この商品を含むブログ (7件) を見る番外編ということで、定理証明手習いをAgdaでやってみた。 最初は、組…

Agdaでカリーのパラドックスをやってみた。 自信作です。 ポイントは(X ≡ (X → Y)) → Xを先に考える事です。Agda/Curry5.agda at master · righ1113/Agda · GitHub

足し算の定義：0と−が存在して結合法則と交換法則を満たすような演算のことを足し算と呼ぶ （－1）×（－1）＝1の数学的証明が凄すぎて大草原 | 不思議.net ここを見て、Agdaで(-1)*(-1) = 1を証明したいと思った。 いちおうできた。 Agda/integer7.agda at m…

俺整数が加法に対してアーベル群をなす事の証明を洗練させてみた。全体的に、reflで整数から自然数の組に展開させて、 congで自然数の法則を使って、 symで自然数の組から整数に戻す、ということをやっている。仮定(postulate)したのは ・自然数の結合法則 …

前回作った俺整数の正しさを証明するために、 俺整数が加法に対してアーベル群をなす事を証明しようと思った。 加法の定義は少し変えた。 module integer4 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl; sym…

Agdaで俺整数を定義してみた。 Natから符号を付けてIntを定義する方法も考えたけど、ゴチャゴチャしてやめた。 0と、+1を表すPと、-1を表すMで構成した。 module integer2 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using …

Agdaのインストールについては Agdaのインストール | righ1113のブログ を参照ください。Agda 入門 を参考にしながら、というか写しで書いてみた。 module plus where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl…