Proving associativity of natural number addition using Scala shapeless

Question

The following code is Idris:

natAssociative : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a + b) + c = a + (b + c)
natAssociative Z b c = the (b + c = b + c) refl
natAssociative (S k) b c = replace {P=\x => S (k + b) + c = S x} (natAssociative k b c) refl

I'm having a very tough time translating that to shapeless. I've tried a few different encodings, but I think this was the most promising start:

import scalaz.Leibniz._
import shapeless.{ HNil, Nat, Succ, Poly3 }
import shapeless.Nat._
import shapeless.ops.nat._

object natAssociative extends Poly3 {
  implicit def case0[B <: Nat, C <: Nat]: Case[_0, B, C] = at[_0, B, C] {
    case (Nat._0, b, c) => refl[Sum[B, C]#Out]
  }
  implicit def caseSucc[K <: Nat, B <: Nat, C <: Nat] = ???
}

I'm having trouble with induction and making Scala recognise that we have 2 possible cases to recurse to. Is there a trick for encoding this part?

Answer 1

With the definition of Nat and Sum in shapeless, you cannot really prove anything. That because Sum isn't a function, with same arguments, we can have different result:

object Pooper {
  implicit def invalidSum: Sum[_1, _1] = new Sum[_1, _1] {
    type Out = _3
  }
}

But if we define naturals and summation a bit differently:

package plusassoc

import scala.language.higherKinds
import scalaz.Leibniz

sealed trait Nat {
  type Add[A <: Nat] <: Nat // 1.add(5)
}

case class Zero() extends Nat {
  type Add[A <: Nat] = A
}

case class Succ[N <: Nat]() extends Nat {
  type Add[A <: Nat] = Succ[N#Add[A]]
}

// a for aliases
package object a {
  // Equality on nats
  type ===[A <: Nat, B <: Nat] = Leibniz[Nothing, Nat, A, B]

  type Plus[A <: Nat, B <: Nat] = A#Add[B]

  type One = Succ[Zero]
  type Two = Succ[One]
  type Three = Succ[Two]
}

import a._

The Add (and Plus) are now well-behaved type-level functions.

---

Then the we can write proof of associativity of Plus:

/*
  plus-assoc : ∀ n m p → (n + (m + p)) ≡ ((n + m) + p)
  plus-assoc zero m p = refl
  plus-assoc (suc n) m p = cong suc (plus-assoc n m p)
*/
trait PlusAssoc[N <: Nat, M <: Nat, P <: Nat] {
  val proof: Plus[N,Plus[M, P]] === Plus[Plus[N, M], P]
}

object PlusAssoc {
  implicit def plusAssocZero[M <: Nat, P <: Nat]: PlusAssoc[Zero, M, P] = new PlusAssoc[Zero, M, P] {
    val proof: Plus[M,P] === Plus[M,P] = Leibniz.refl
  }

  implicit def plusAssocSucc[N <: Nat, M <: Nat, P <: Nat](implicit
    ih: PlusAssoc[N, M, P]): PlusAssoc[Succ[N], M, P] = new PlusAssoc[Succ[N], M, P] {
      // For some reason scalac fails to infer right params for lift :(
      val proof: Succ[Plus[N,Plus[M, P]]] === Succ[Plus[Plus[N, M], P]] = Leibniz.lift[
        Nothing, Nothing,
        Nat, Nat,
        Succ,
        Plus[N, Plus[M, P]], Plus[Plus[N, M], P]
      ](ih.proof)
    }
}

And as we rely on implicits, we have to test that scalac can really construct evidence using our "rules":

import plusassoc._
import plusassoc.a._
import plusassoc.PlusAssoc._

implicitly[PlusAssoc[One, Two, Three]].proof
res0: ===[Plus[One,Plus[Two,Three]],Plus[Plus[One,Two],Three]] = scalaz.LeibnizFunctions$$anon$2@7b2c4c00
// with plusassoc.a. prefix skipped