Agda error when checking the inferred type

Question

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?

Answer 1

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