Proving Assoziativität der natürliche Zahl zusätzlich mit Scala formlos

Question

Der folgende Code ist 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 

Ich bin eine sehr harte Zeit, das zu formlos zu übersetzen. Ich habe ein paar verschiedene Kodierungen versucht, aber ich denke, das ist der vielversprechendste Start war:

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] = ??? 
} 

Ich habe Probleme mit der Induktion und macht Scala erkennen, dass wir zwei mögliche Fälle müssen Rekursion auf. Gibt es einen Trick für die Codierung dieses Teils?

Answer 1

Mit der Definition von Nat und Sum in formlos, können Sie wirklich nichts beweisen. Das weil Sum keine Funktion, mit denselben Argumenten, können wir anderes Ergebnis haben:

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

Aber wenn wir Naturals definieren und ein wenig Summierung anders:

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._ 

Die Add (und Plus) sind jetzt wohlerzogene Typ-Level-Funktionen.

---

Dann die wir Beweis der Assoziativität von Plus schreiben:

/* 
    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) 
    } 
} 

Und wie wir auf implicits verlassen, müssen wir diese scalac testen unsere „Regeln“ wirklich bauen kann Beweis mit:

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