检查推断类型时出现 Agda 错误
Agda error when checking the inferred type
我试图证明两个奇数之和是偶数。
最后一行有什么问题？
data odd : ℕ → Set
data even : ℕ → Set
data even where
ezero :
-------
even zero
esuc : ∀ {n : ℕ}
→ odd n
------
→ even (suc n)
data odd where
osuc : ∀ { n : ℕ }
→ even n
------
→ odd (suc n)
e+e≡e : ∀ {m n : ℕ}
→ even m
→ even n
----
→ even (m + n)
o+e≡o : ∀ {m n : ℕ}
→ odd m
→ even n
------
→ odd (m + n)
e+e≡e ezero en = en
e+e≡e (esuc om) en = esuc (o+e≡o om en)
o+e≡o (osuc em) en = osuc (e+e≡e em en)
o+o≡e : ∀ {m n : ℕ}
→ odd m
→ odd n
------
→ even (m + n)
o+o≡e (osuc em) on = esuc (o+e≡o on em)
我收到这个错误：
➊ - 660 Experiment.agda Agda ∏ unix | 50: 0 Bottom
/Users/max/dev/plfa.github.io/src/plfa/Experiment.agda:52,28-39
n != n₁ of type ℕ
when checking that the inferred type of an application
odd (n + _n_31)
matches the expected type
odd (n₁ + n)
但我觉得这些类型还不错。例如，如果我将右侧替换为？并检查目标，Agda 显示：
Goal: even (suc (n + n₁))
————————————————————————————————————————————————————————————
on : odd n₁
em : even n
n₁ : ℕ (not in scope)
n : ℕ (not in scope
所以我要传递证据 on n 是奇数，em m 是偶数。并将这些传递给 o+e≡e，后者需要这些类型的参数。那我哪里错了？
一般来说，我如何阅读 Agda 的错误消息？变量名后的下标是否有意义？
它告诉你 em 不等于 on：你想要 odd (m + n) 的证明，但你得到 odd (n + m) - Agda 看不到加法是可交换的。你应该交换参数。
o+o≡e on (osuc em) = esuc (o+e≡o on em)
这会产生不同的错误。该错误告诉您 Agda 无法计算出 suc (m + n) 等于 m + suc n，这意味着您需要引入一个确定等式的引理。然后回想一下 transport（一个将依赖类型 B x 的值沿着等式 x ≡ y 传输到不同依赖类型 B y 的值的函数），这会给你一种从 esuc (o+e≡o on em) 构造的值中获取所需类型值的方法。
零导入的工作解决方案：
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == x
-- congruence
cong : forall {A B : Set} {x y : A} -> (f : A -> B) -> (x == y) -> (f x) == (f y)
cong f refl = refl -- note these refls are of different types: of x == y on the left, and of (f x) == (f y) on the right
-- transport: given two values are "equal", transport one dependent value along the equality path into a different dependent value
transport : forall {A : Set} {B : A -> Set} {x y : A} -> x == y -> B x -> B y
transport refl bx = bx -- proof relies on the circumstance that the only way to construct x == y is refl, so (B x) is (B y)
-- then induction at the heart of Agda can work out that this must be valid for any x == y
-- commutativity of _==_
comm : forall {A : Set} {x y : A} -> x == y -> y == x
comm refl = refl
data Nat : Set where
zero : Nat
suc : Nat -> Nat
_+_ : ∀ (m n : Nat) -> Nat
zero + n = n
(suc m) + n = suc (m + n)
-- Proving the necessary commutativity of suc.
-- Agda can see things like "(suc m) + n == suc (m + n)" by definition
-- but other equalities need proving, and then you can transport
-- the values from one type to another
n+1≡1+n : forall (m n : Nat) -> (m + (suc n)) == (suc (m + n))
n+1≡1+n zero n = refl
n+1≡1+n (suc m) n = cong suc (n+1≡1+n m n)
data odd : Nat → Set
data even : Nat → Set
data even where
ezero :
-------
even zero
esuc : ∀ {n : Nat}
→ odd n
------
→ even (suc n)
data odd where
osuc : ∀ { n : Nat }
→ even n
------
→ odd (suc n)
e+e≡e : ∀ {m n : Nat}
→ even m
→ even n
----
→ even (m + n)
o+e≡o : ∀ {m n : Nat}
→ odd m
→ even n
------
→ odd (m + n)
e+e≡e ezero en = en
e+e≡e (esuc om) en = esuc (o+e≡o om en)
o+e≡o (osuc em) en = osuc (e+e≡e em en)
-- Prove commutativity of even based on a known proof for commutativity of suc.
e-comm : forall {m n : Nat} -> even (suc (m + n)) -> even (m + (suc n))
e-comm {m} {n} esmn = transport {B = even} (comm (n+1≡1+n m n)) esmn -- transport needs hinting what B is
-- otherwise Agda cannot infer what B is based on the definition as found in this snippet
-- the error may seem a bit obscure, but you can see it is wrangling with
-- the dependent type of B:
-- Failed to solve the following constraints:
-- _74 := λ {m} {n} esmn → transport (comm (n+1≡1+n m n)) (_72 esmn)
-- [blocked on problem 166]
-- [165] (even (suc (m + n))) =< (_B_73 (suc (m + n))) : Set
-- [166] _B_73 (m + suc n) =< even (m + suc n) : Set
-- _71 := (λ {m} {n} esmn → esmn) [blocked on problem 165]
--
-- See, it is stuck trying to work out a type _B_73 such that even
-- would be a subtype of it, and a different even would be a supertype of it.
o+o≡e : ∀ {m n : Nat}
→ odd m
→ odd n
------
→ even (m + n)
o+o≡e {m} om (osuc en) = e-comm {m} (esuc (o+e≡o om en)) -- Agda had a problem working out m, so extracting it from implicits
-- Failed to solve the following constraints:
-- _81 := λ {.n} {.m} om en → e-comm (_80 om en)
-- [blocked on problem 188]
-- [188, 189] _m_74 om en + suc (_n_75 om en) = .m + suc .n : Nat
-- _79 := λ {.n} {.m} om en → esuc (o+e≡o om en)
-- [blocked on problem 185]
-- [185, 186, 187] .m + .n = _m_74 om en + _n_75 om en : Nat
--
-- See, if e-comm is not given {m} and {n}, then it is stuck working out
-- _m_74
transport 连接依赖类型是关键概念之一。例如，_==_ 的同余和交换性可以简化为 transport:
-- congruence
cong : forall {A B : Set} {x y : A} -> (f : A -> B) -> (x == y) -> (f x) == (f y)
cong {x = x} f xy = transport {B = (\y -> (f x) == (f y))} -- just making explicit that B is a type (f x) == (f _)
xy refl -- this refl is of type (f x) == (f x), which gets transported along x == y to (f x) == (f y)
-- commutativity of _==_
comm : forall {A : Set} {x y : A} -> x == y -> y == x
comm {x = x} xy = transport {B = (_== x)} xy refl -- this refl is of type x == x, which gets transported along x == y to y == x
我试图证明两个奇数之和是偶数。
最后一行有什么问题？
data odd : ℕ → Set
data even : ℕ → Set
data even where
ezero :
-------
even zero
esuc : ∀ {n : ℕ}
→ odd n
------
→ even (suc n)
data odd where
osuc : ∀ { n : ℕ }
→ even n
------
→ odd (suc n)
e+e≡e : ∀ {m n : ℕ}
→ even m
→ even n
----
→ even (m + n)
o+e≡o : ∀ {m n : ℕ}
→ odd m
→ even n
------
→ odd (m + n)
e+e≡e ezero en = en
e+e≡e (esuc om) en = esuc (o+e≡o om en)
o+e≡o (osuc em) en = osuc (e+e≡e em en)
o+o≡e : ∀ {m n : ℕ}
→ odd m
→ odd n
------
→ even (m + n)
o+o≡e (osuc em) on = esuc (o+e≡o on em)
我收到这个错误：
➊ - 660 Experiment.agda Agda ∏ unix | 50: 0 Bottom
/Users/max/dev/plfa.github.io/src/plfa/Experiment.agda:52,28-39
n != n₁ of type ℕ
when checking that the inferred type of an application
odd (n + _n_31)
matches the expected type
odd (n₁ + n)
但我觉得这些类型还不错。例如，如果我将右侧替换为？并检查目标，Agda 显示：
Goal: even (suc (n + n₁))
————————————————————————————————————————————————————————————
on : odd n₁
em : even n
n₁ : ℕ (not in scope)
n : ℕ (not in scope
所以我要传递证据 on n 是奇数，em m 是偶数。并将这些传递给 o+e≡e，后者需要这些类型的参数。那我哪里错了？
一般来说，我如何阅读 Agda 的错误消息？变量名后的下标是否有意义？
它告诉你 em 不等于 on：你想要 odd (m + n) 的证明，但你得到 odd (n + m) - Agda 看不到加法是可交换的。你应该交换参数。
o+o≡e on (osuc em) = esuc (o+e≡o on em)
这会产生不同的错误。该错误告诉您 Agda 无法计算出 suc (m + n) 等于 m + suc n，这意味着您需要引入一个确定等式的引理。然后回想一下 transport（一个将依赖类型 B x 的值沿着等式 x ≡ y 传输到不同依赖类型 B y 的值的函数），这会给你一种从 esuc (o+e≡o on em) 构造的值中获取所需类型值的方法。
零导入的工作解决方案：
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == x
-- congruence
cong : forall {A B : Set} {x y : A} -> (f : A -> B) -> (x == y) -> (f x) == (f y)
cong f refl = refl -- note these refls are of different types: of x == y on the left, and of (f x) == (f y) on the right
-- transport: given two values are "equal", transport one dependent value along the equality path into a different dependent value
transport : forall {A : Set} {B : A -> Set} {x y : A} -> x == y -> B x -> B y
transport refl bx = bx -- proof relies on the circumstance that the only way to construct x == y is refl, so (B x) is (B y)
-- then induction at the heart of Agda can work out that this must be valid for any x == y
-- commutativity of _==_
comm : forall {A : Set} {x y : A} -> x == y -> y == x
comm refl = refl
data Nat : Set where
zero : Nat
suc : Nat -> Nat
_+_ : ∀ (m n : Nat) -> Nat
zero + n = n
(suc m) + n = suc (m + n)
-- Proving the necessary commutativity of suc.
-- Agda can see things like "(suc m) + n == suc (m + n)" by definition
-- but other equalities need proving, and then you can transport
-- the values from one type to another
n+1≡1+n : forall (m n : Nat) -> (m + (suc n)) == (suc (m + n))
n+1≡1+n zero n = refl
n+1≡1+n (suc m) n = cong suc (n+1≡1+n m n)
data odd : Nat → Set
data even : Nat → Set
data even where
ezero :
-------
even zero
esuc : ∀ {n : Nat}
→ odd n
------
→ even (suc n)
data odd where
osuc : ∀ { n : Nat }
→ even n
------
→ odd (suc n)
e+e≡e : ∀ {m n : Nat}
→ even m
→ even n
----
→ even (m + n)
o+e≡o : ∀ {m n : Nat}
→ odd m
→ even n
------
→ odd (m + n)
e+e≡e ezero en = en
e+e≡e (esuc om) en = esuc (o+e≡o om en)
o+e≡o (osuc em) en = osuc (e+e≡e em en)
-- Prove commutativity of even based on a known proof for commutativity of suc.
e-comm : forall {m n : Nat} -> even (suc (m + n)) -> even (m + (suc n))
e-comm {m} {n} esmn = transport {B = even} (comm (n+1≡1+n m n)) esmn -- transport needs hinting what B is
-- otherwise Agda cannot infer what B is based on the definition as found in this snippet
-- the error may seem a bit obscure, but you can see it is wrangling with
-- the dependent type of B:
-- Failed to solve the following constraints:
-- _74 := λ {m} {n} esmn → transport (comm (n+1≡1+n m n)) (_72 esmn)
-- [blocked on problem 166]
-- [165] (even (suc (m + n))) =< (_B_73 (suc (m + n))) : Set
-- [166] _B_73 (m + suc n) =< even (m + suc n) : Set
-- _71 := (λ {m} {n} esmn → esmn) [blocked on problem 165]
--
-- See, it is stuck trying to work out a type _B_73 such that even
-- would be a subtype of it, and a different even would be a supertype of it.
o+o≡e : ∀ {m n : Nat}
→ odd m
→ odd n
------
→ even (m + n)
o+o≡e {m} om (osuc en) = e-comm {m} (esuc (o+e≡o om en)) -- Agda had a problem working out m, so extracting it from implicits
-- Failed to solve the following constraints:
-- _81 := λ {.n} {.m} om en → e-comm (_80 om en)
-- [blocked on problem 188]
-- [188, 189] _m_74 om en + suc (_n_75 om en) = .m + suc .n : Nat
-- _79 := λ {.n} {.m} om en → esuc (o+e≡o om en)
-- [blocked on problem 185]
-- [185, 186, 187] .m + .n = _m_74 om en + _n_75 om en : Nat
--
-- See, if e-comm is not given {m} and {n}, then it is stuck working out
-- _m_74
transport 连接依赖类型是关键概念之一。例如，_==_ 的同余和交换性可以简化为 transport:
-- congruence
cong : forall {A B : Set} {x y : A} -> (f : A -> B) -> (x == y) -> (f x) == (f y)
cong {x = x} f xy = transport {B = (\y -> (f x) == (f y))} -- just making explicit that B is a type (f x) == (f _)
xy refl -- this refl is of type (f x) == (f x), which gets transported along x == y to (f x) == (f y)
-- commutativity of _==_
comm : forall {A : Set} {x y : A} -> x == y -> y == x
comm {x = x} xy = transport {B = (_== x)} xy refl -- this refl is of type x == x, which gets transported along x == y to y == x