Это говорит вам, что em не равно on: вам нужно подтверждение odd (m + n), но вы получаете odd (n + m) - Агда не видит, что сложение коммутативно. Вы должны поменять аргументы.
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