いや、来週くらいに書くけど。
昨日（世界のどこかの時間では）の担当だったよしひろさんが書いた記事
依存関係のある値のうちの一部をrewriteしようとしたときの問題
に最後にこんな一言があった。
> また、依存型に定評のあるAgdaではどうなるかなども興味深い。
なるほど、この問いには答えねば。
そう思いAgdaを起動してまねた記述を作る。
ファイル名はYIquestion.agdaとする。
module YIquestion where
open import Data.Nat
open import Relation.Binary.Core
postulate
f : (n : ℕ) → n > 0 → ℕ
h : (n : ℕ) (H : 2 * n > 0) → f (2 * n) H ≡ n
postulate
x : ℕ
H : x > 0
goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = ?
同じ流れならここでeqを展開（rewrite相当）、Coqではエラーの出る展開である。
だが、エラーメッセージがなんか違うぞ・・・
Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the inferred
indices [x] with the expected indices [2 * 1]
when checking that the expression ? has type f x H ≡ 1
(●△●)？？
Hが問題とかそれ以前の問題のようだ。
え、なに？xと2*1をunifyしようとして詰まった・・・？？
何を言ってるのだろう。
というヒントを元に作った正解はこちら。
goal' : (x : ℕ) → (x ≡ 2 * 1) → (H : x > 0) → f x H ≡ 1
goal' .2 refl H = h 1 H
goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = goal' x eq H
最初のgoal'の記述は
goal' x eq H = ?
からeqを展開して作成した。
これを見ると何となく見えてくるのは、
どうもAgdaは引数が実際になんだったかしかreflで書き換えないらしい
ということである。
つまり、Coqの場合同様にHが依存していることももちろん問題だったのだが、それ以前に
xが適当に置かれた変数であるせいで、展開できない
ということの方がよっぽど問題だったという。
やっぱりAgdaのエラーメッセージはわかりにくい・・・
ちなみにCoqでは上のやり方に相当するパターンマッチではなくeq_indなどで書き換えているので注意。
