Agdaで整数 その5

整数の定義を素朴なものに戻した。

--（succ (succ (pred zero))などが有効、という弱点がある）
data Z : Set where
  zero : Z
  succ : Z -> Z
  pred : Z -> Z

それに加法、反数、乗法を定義したものがこちら。
整数の素朴な定義

この整数が環をなすことをAgdaで証明した。
証明にはrewriteばかり使っている。-Reasoningは使わなかった。
あれ使いづらいもん。
整数が環をなす

ガチな定義も考えたけどね

--（succ (succ (pred zero))などはもうできない）
mutual
  data Z : Set where
    zero : Z
    succ : (x : Z) -> isTrue (zeroOrSucc x) -> Z
    pred : (x : Z) -> isTrue (zeroOrPred x) -> Z

  zeroOrSucc : Z -> Bool
  zeroOrSucc zero = true
  zeroOrSucc (succ x p) = true
  zeroOrSucc (pred x p) = false
  zeroOrPred : Z -> Bool
  zeroOrPred zero = true
  zeroOrPred (succ x p) = false
  zeroOrPred (pred x p) = true
-- succ (succ zero tt) tt のように使う