I'm trying to show that the sum of two odd numbers is even.
What is wrong with the last line?
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)
I'm getting this error:
➊ - 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)
But the types seem fine to me. For example, if I replace the right side with ? and check the goals, Agda shows:
Goal: even (suc (n + n₁))
————————————————————————————————————————————————————————————
on : odd n₁
em : even n
n₁ : ℕ (not in scope)
n : ℕ (not in scope
So I'm passing evidence on that n is odd and em that m is even. And passing these to o+e≡e, which expects arguments of exactly those types. So where did I go wrong?
And in general, how can I read Agda's error messages? Are the subscripts after variable names meaningful?
It's telling you that em is not equal to on: you want a proof of odd (m + n), but you get odd (n + m) - Agda can't see addition is commutative. You should swap the arguments.
o+o≡e on (osuc em) = esuc (o+e≡o on em)
This produces a different error. That error tells you that Agda is unable to work out that suc (m + n) is equal to m + suc n, which means you need to introduce a lemma that establishes the equality. Then recall transport (a function that transports a value of a dependent type B x along equality x ≡ y to a value of a different dependent type B y), and that will give you a way to obtain a value of the needed type from the value that esuc (o+e≡o on em) constructs.
Working solution with zero imports:
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 joining dependent types is one of the key concepts. For example, congruence and commutativity of _==_ can be reduced to 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