整数の割り切れる可能性について証明しようとしています。最初に、割り切れる可能性が反射的であることを証明しようとしました。
∣-refl : ∀{n} → n ∣ n
引き算で割り切れると定義したので...
data _∣_ : ℤ → ℤ → Set where
0∣d : ∀{d} → zero ∣ d
n-d∣d : ∀{n d} → (n - d) ∣ d → n ∣ d
...という事実を使えば簡単に思えますn-n=0:
∣-refl {n} with n-n≡0 n
... | refl = n-d∣d 0∣d
しかし、Agda は refl でのパターン マッチを拒否します。の他の正規形が存在しなくてもn-n=0 n. 私はこれを別の関数で証明しました。という事実を利用するしかありませんn-n=0。
C:\Users\ebolnme\Desktop\agda\Integers.agda:118,7-11
n + neg n != zero of type ℤ
when checking that the pattern refl has type n + neg n ≡ zero
ノート：
a - bによって定義されますa + (neg b)- 私はすでに証明した
n-n≡0 : (n : ℤ) → n - n ≡ zero