You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
88 lines
1.7 KiB
Go
88 lines
1.7 KiB
Go
package main
|
|
|
|
//
|
|
// Encoding the semantics
|
|
//
|
|
|
|
type Bool interface{ isBool() }
|
|
|
|
type Term interface{ isTerm() }
|
|
|
|
type Term2Term interface{ isTerm2Term() }
|
|
|
|
// trick to encode higher-kinded types
|
|
type V[H Term2Term, T Term] Term
|
|
|
|
//
|
|
// Naturals
|
|
//
|
|
|
|
type Zero Term
|
|
type Succ Term2Term
|
|
|
|
// Some aliases
|
|
|
|
type One = V[Succ, Zero]
|
|
type Two = V[Succ, V[Succ, Zero]]
|
|
type Three = V[Succ, V[Succ, V[Succ, Zero]]]
|
|
|
|
//
|
|
// Equality
|
|
//
|
|
|
|
type Eq[A, B any] Bool
|
|
|
|
// Eq_Refl ~> forall x : x = x
|
|
func Eq_Reflexive[T any]() Eq[T, T] { panic("axiom") }
|
|
|
|
// Eq_Symmetric ~> forall a, b: a = b => b = a
|
|
func Eq_Symmetric[A, B any](_ Eq[A, B]) Eq[B, A] { panic("axiom") }
|
|
|
|
// Eq_Transitive ~> forall a, b, c: a = b e b = c => a = c
|
|
func Eq_Transitive[A, B, C any](_ Eq[A, B], _ Eq[B, C]) Eq[A, C] { panic("axiom") }
|
|
|
|
// Function_Eq ~> forall f function, forall a, b terms: a = b => f(a) = f(b)
|
|
func Function_Eq[F Term2Term, A, B Term](_ Eq[A, B]) Eq[V[F, A], V[F, B]] {
|
|
panic("axiom")
|
|
}
|
|
|
|
//
|
|
// Plus Axioms
|
|
//
|
|
|
|
type Plus[L, R Term] Term
|
|
|
|
// "a + 0 = a"
|
|
|
|
// Plus_Zero ~> forall a, b: a + succ(b) = succ(a + b)
|
|
func Plus_Zero[N Term]() Eq[Plus[N, Zero], N] { panic("axiom") }
|
|
|
|
// "a + (b + 1) = (a + b) + 1"
|
|
|
|
// Plus_Sum ~> forall a, b: a + succ(b) = succ(a + b)
|
|
func Plus_Sum[N, M Term]() Eq[Plus[N, V[Succ, M]], V[Succ, Plus[N, M]]] { panic("axiom") }
|
|
|
|
//
|
|
// 1 + 1 = 2
|
|
//
|
|
|
|
// Theorem_OnePlusOneEqTwo
|
|
func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] {
|
|
var en1 Eq[
|
|
Plus[One, Zero],
|
|
One,
|
|
] = Plus_Zero[One]()
|
|
|
|
var en2 Eq[
|
|
V[Succ, Plus[One, Zero]],
|
|
Two,
|
|
] = Function_Eq[Succ](en1)
|
|
|
|
var en3 Eq[
|
|
Plus[One, One],
|
|
V[Succ, Plus[One, Zero]],
|
|
] = Plus_Sum[One, Zero]()
|
|
|
|
return Eq_Transitive(en3, en2)
|
|
}
|