[Agda] Dependent Types at Work

[Dan Licata]

On Mar21, Tristan Wibberley wrote:
> I was expecting this to load successfully but I got an error for the
> right hand side of (succ m) +/relatefirstoperand n:
> 
> succ (m + n) != m + succ n of type Nat
> 
> but I've checked the canonical forms of both of those (C-c C-n in emacs
> with concrete m and n) and they are identical.
> 

Indeed.  Type theories that treat equality _intensionally_, like Agda,
separate a notion of _definitional equality_ (roughly, direct
computation from the definitions) from a coarser notion of
_propositional equality_, which equates more things but requires proof.
It's true that all closed instances of the two above terms are equal, as
you observed, but they're not definitionally equal, given your
definition of +:

  _+_ : Nat -> Nat -> Nat
  _+_ zero b = b
  _+_ (succ a) b = a + (succ b)

because there's no clause of the definition that says

  m + (succ n) = succ (m + n)

So, there are two solutions:

(1) you can massage the definitions so that the facts you need are
definitionally true.  In this case, change the last clause of + to

  _+_ (succ a) b = succ (a + b)

and your lemma will go through.

(2) you can prove lemmas like   m + (succ n) = succ(m + n)  explicitly.

In this case, you can use the following notion of equality:

  data _==_ {A : Set} : A -> A -> Set where                                                                                                        
    Refl : {a : A} -> a == a                                                                                                                       

and prove, using your original definition of + , that

  lemma : {a b : Nat} -> (a + (succ b)) == succ (a + b)
  lemma = {! !}

-Dan