「依存関係のある値のうちの一部をrewriteしようとしたときの問題」をAgdaで書くとどうなるか

依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか．

こういうことだろうか？

module AC-2013-5 where

open import Data.Nat
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

postulate
  f : ∀ n → n > 0 → ℕ
  h : (n : ℕ) → (H : 2 * n > 0) → f (2 * n) H ≡ n

n≡m→m>0→n>0 : ∀ {n} {m} → n ≡ m → m > 0 → n > 0
n≡m→m>0→n>0 n≡m m>0 rewrite n≡m = m>0

2*1>0 : 2 * 1 > 0
2*1>0 = s≤s z≤n

lemma : ∀ x
      → (eq : x ≡ 2 * 1)
      → let x>0 = n≡m→m>0→n>0 eq 2*1>0 in f x x>0 ≡ 1
lemma x eq rewrite eq = h 1 2*1>0

-- もしくはこっち？
lemma' : ∀ x → (H : x > 0) → (eq : x ≡ 2 * 1) → f x H ≡ 1
lemma' x H eq rewrite eq = h 1 H

だよね？

まぁ，元記事のHについても普通に証明書いて突っ込むので他の証明と特に変わりは無いかなと

後者だった場合，特に問題なくhにH突っ込んで終わり

kikさんによるとどうもxとHもpostulateではないかという話なので，その場合も

module AC-2013-5 where

open import Data.Nat
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

postulate
  f : ∀ n → n > 0 → ℕ
  h : (n : ℕ) → (H : 2 * n > 0) → f (2 * n) H ≡ n
  x : ℕ
  H : x > 0

lemma'' : (eq : x ≡ 2 * 1) → f x H ≡ 1
lemma'' = lemma' x H
  where
    lemma' : ∀ x → (H : x > 0) → (eq : x ≡ 2 * 1) → f x H ≡ 1
    lemma' x H eq rewrite eq = h 1 H

かな．

前のほうでも使ったlemma'はgeneralizeした定義での証明なので，それを使う．つまり元記事でのCoqの証明と同じことをしてるかな．

(追記)chiguriさんが先にやってた．俺がスロゥリィ