agdaplfa

Agda error when checking the inferred type


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?


Solution

  • 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