kagcc lesguillemets

11 followers · 40 following

Kyoto, Japan
https://lesguillemets.github.io/blog

View GitHub Profile

lesguillemets / adv_cal_2015_1205_question.v

Last active December 11, 2015 13:41 — forked from mathink/adv_cal_2015_1205_question.v

0 なのか 1 なのか、そういうのめんどくさいので任意の自然数 N から始まる "自然数" を考えました。循環じゃなくて重複です。つきましては、加算と乗算を定義し、それらが正しいものであることを証明してみましょう。ついでに可換律と結合律も。http://qiita.com/advent-calendar/2015/theorem-prover で書くのはこれの解説 "ではありません"。

	Set Implicit Arguments.
	Unset Strict Implicit.

	Require Import Arith.

	(* Base "から" 始まる "自然数" *)
	Inductive number :=
	\| Base: number
	\| Next: number -> number.