让 Agda 减少目标类型中的表达式

Question

使用 the standard library 中的 ℕ 和 _≟_，我有

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

foo : ℕ -> ℕ -> ℕ
foo x y with x ≟ y
foo x .x | yes refl = x
foo x y  | no contra = y

data Bar : ℕ -> Set where
  bar : (x : ℕ) -> Bar (foo x x)

我要实施

mkBar : (x : ℕ) -> Bar x
mkBar x = bar x

Agda 抱怨，

Type mismatch:
expected: x
  actual: foo x x | x ≟ x
when checking that the expression bar x
has type Bar x

这对我来说很有意义：Agda 不知道先验 x ≟ x 总是求值为 yes refl，所以它不会求值 foo x x 直到它对 x.

有了更多的了解

所以我尝试重写目标以强制 x ≟ x 解析为 yes refl,

eq-refl : forall x -> (x ≟ x) ≡ yes refl
eq-refl x with x ≟ x
eq-refl x | yes refl = refl
eq-refl x | no contra = ⊥-elim (contra refl)

mkBar : (x : ℕ) -> Bar x
mkBar x rewrite eq-refl x = bar x

但无济于事。同样的错误信息。我也尝试通过 foo x x ≡ x:

重写

foo-eq : forall x -> foo x x ≡ x
foo-eq x rewrite eq-refl x = refl

mkBar : (x : ℕ) -> Bar x
mkBar x rewrite foo-eq x = bar x

This answer建议在mkBar左侧的x ≟ x上进行模式匹配，但似乎也没有效果：

mkBar : (x : ℕ) -> Bar x
mkBar x with x ≟ x
mkBar x | yes refl = bar x
mkBar x | no contra = ⊥-elim (contra refl)

我一定是漏掉了一个技巧。如何去除目标类型中的 | 并使 foo x x 减少为 x？（我不想直接在 mkBar 的 LHS 中检查 x。）

Answer 1

您快到了：需要注意的重要一点是 rewrite 在目标中使用 x ≡ y 并用 y 替换 x。 foo-eq x 有类型 foo x x ≡ x 但目标中没有要替换的 foo x x！

你需要做的是由 sym (foo-eq x) 像这样重写：

mkBar : (x : ℕ) → Bar x
mkBar x rewrite sym (foo-eq x) = bar x

Bar x 然后变成 Bar (foo x x) 意味着你可以应用你的构造函数。

让 Agda 减少目标类型中的表达式

Making Agda reduce an expression in a goal type

theorem-proving

agda

dependent-type