minh kết hợp của số tự nhiên Ngoài ra sử dụng Scala hình thù

Question

Các mã sau đây là 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 

Tôi đang gặp một thời gian rất khó khăn dịch đó để hình thù. Tôi đã thử một vài mã hóa khác nhau, nhưng tôi nghĩ rằng đây là khởi đầu đầy hứa hẹn nhất:

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

Tôi đang gặp rắc rối với cảm ứng và làm cho Scala nhận ra rằng chúng tôi có 2 trường hợp có thể recurse đến. Có một mẹo để mã hóa phần này không?

Answer 1

Với định nghĩa Nat và Sum không có hình dạng, bạn không thể chứng minh được điều gì. Đó là bởi vì Sum không phải là một chức năng, với cùng một lý lẽ, chúng ta có thể có kết quả khác nhau:

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

Nhưng nếu chúng ta định nghĩa bẩm và tổng kết một chút khác nhau:

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

Các Add (và Plus) hiện đang hoạt động tốt ở mức loại.

---

Sau đó, chúng ta có thể viết bằng chứng về kết hợp của 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) 
    } 
} 

Và như chúng tôi dựa vào implicits, chúng ta phải kiểm tra scalac rằng thực sự có thể xây dựng bằng chứng sử dụng "quy tắc" của chúng tôi:

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