5

Peano 数に対する次の型レベル加算関数が与えられた場合

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] = a match
  case O => b
  case S[n] => S[n plus b]

次のように定理を証明したいとします

すべての自然数 n に対して、n + 0 = n

おそらくそのように指定できます

type plus_n_0 = [n <: Nat] =>> (n plus O) =:= n

次に、定理の証拠を提供することになると、特定のケースで簡単に Scala コンパイラに証拠を求めることができます

summon[plus_n_O[S[S[O]]]]  // ok, 2 + 0 = 2

しかし、 のすべてのインスタンス化の証拠を生成できるかどうかを Scala に問い合わせて[n <: Nat]、 の証明を提供するにはどうすればよいplus_n_0でしょうか?

4

1 に答える 1

5

これは、この段落の文字通りの解釈の試みである 1 つの可能なアプローチです。

すべての自然数に関する命題を証明するとき、それが に対して成り立つと仮定して、に対しておよび に対してE:N→U証明すれば十分です。つまり、 および を構成します。0succ(n)nez:E(0)es:∏(n:N)E(n)→E(succ(n))

HoTT ブック (セクション 5.1)から。

以下のコードで実装されたものの計画は次のとおりです。

  • P「すべての自然数に何らかの性質が成り立つ」という命題の証明を持つとはどういう意味か定式化してください。以下、使用します

     trait Forall[N, P[n <: N]]:
   inline def apply[n <: N]: P[n]

    -メソッドの署名は、apply本質的に「すべてn <: Nの について、証拠を生成できる」と述べていP[n]ます。

    メソッドが であると宣言されていることに注意してくださいinline。これは、実行時に証明∀n.P(n)が建設的で実行可能であることを保証するための 1 つの可能な方法です(ただし、手動で生成された証人用語を使用した別の提案については、編集履歴を参照してください)。

  • 自然数のある種の帰納法を仮定します。以下では、次の定式化を使用します。

     If
    P(0) holds, and
    whenever P(i) holds, then also P(i + 1) holds,
 then
    For all `n`, P(n) holds

    deriveいくつかのメタプログラミング機能を使用して、そのような誘導原理が可能になるはずだと私は信じています。

  • 帰納法の基本の場合と帰納の場合の証明を書いてください。

  • ???

  • 利益

コードは次のようになります。

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] <: Nat = a match
  case O => b
  case S[n] => S[n plus b]

trait Forall[N, P[n <: N]]:
  inline def apply[n <: N]: P[n]

trait NatInductionPrinciple[P[n <: Nat]] extends Forall[Nat, P]:
  def base: P[O]
  def step: [i <: Nat] => (P[i] => P[S[i]])
  inline def apply[n <: Nat]: P[n] =
    (inline compiletime.erasedValue[n] match
      case _: O => base
      case _: S[pred] => step(apply[pred])
    ).asInstanceOf[P[n]]

given liftCoUpperbounded[U, A <: U, B <: U, S[_ <: U]](using ev: A =:= B):
  (S[A] =:= S[B]) = ev.liftCo[[X] =>> Any].asInstanceOf[S[A] =:= S[B]]

type NatPlusZeroEqualsNat[n <: Nat] = (n plus O) =:= n

def trivialLemma[i <: Nat]: ((S[i] plus O) =:= S[i plus O]) =
  summon[(S[i] plus O) =:= S[i plus O]]

object Proof extends NatInductionPrinciple[NatPlusZeroEqualsNat]:
  val base = summon[(O plus O) =:= O]
  val step: ([i <: Nat] => NatPlusZeroEqualsNat[i] => NatPlusZeroEqualsNat[S[i]]) = 
    [i <: Nat] => (p: NatPlusZeroEqualsNat[i]) =>
      given previousStep: ((i plus O) =:= i) = p
      given liftPreviousStep: (S[i plus O] =:= S[i]) =
        liftCoUpperbounded[Nat, i plus O, i, S]
      given definitionalEquality: ((S[i] plus O) =:= S[i plus O]) =
        trivialLemma[i]
      definitionalEquality.andThen(liftPreviousStep)

def demoNat(): Unit = {
  println("Running demoNat...")
  type two = S[S[O]]
  val ev = Proof[two]
  val twoInstance: two = new S[S[O]]
  println(ev(twoInstance) == twoInstance)
}

コンパイル、実行、および出力します。

true

type の実行可能なevidence-termで再帰的に定義されたメソッドの呼び出しに成功したことを意味しますtwo plus O =:= two。

その他のコメント

  • これは、他の s の内部にあるs が誤って再帰ループを生成しないtrivialLemmaようにするために必要でした。これは少し面倒です。summongiven
  • では上限のある型パラメーターを持つ型コンストラクターが許可されないため、別のliftCo-method forS[_ <: U]が必要でした。=:=.liftCo
  • compiletime.erasedValue＋inline matchすごい！「消去された」型でパターン マッチングを実行できる、ある種のランタイム ギズモを自動的に生成します。これを見つける前に、適切な証人用語を手動で構築しようとしていましたが、これはまったく必要ないようです。無料で提供されています (手動で構築された証人用語によるアプローチについては、編集履歴を参照してください)。
于 2021-04-14T19:11:18.293 に答える