Skip to content

Instantly share code, notes, and snippets.

@NobukazuHanada
Last active January 30, 2018 07:53
Show Gist options
  • Save NobukazuHanada/aefbdcf6bb49654ff0020f8fc429d9a5 to your computer and use it in GitHub Desktop.
Save NobukazuHanada/aefbdcf6bb49654ff0020f8fc429d9a5 to your computer and use it in GitHub Desktop.
class Number {}
class Zero : Number {}
class Succ<N:Number> : Number {}
typealias One = Succ<Zero>
typealias Two = Succ<Succ<Zero>>
typealias Three = Succ<Succ<Succ<Zero>>>
class Eq<S: Number, T: Number> {}
class Add<S: Number, T:Number> : Number {}
// reflective : ( m = m }
func reflective<S>(s:S.Type = S.self) -> Eq<S,S> { return Eq<S,S>() }
// symmetric : { m = n => n = m }
func symmetric<S,T>(s:S.Type = S.self, t:T.Type = T.self) -> (Eq<S,T>) -> Eq<T,S> { return {(e1:Eq<S,T>) -> Eq<T,S> in Eq<T,S>() } }
// transitive : s = t => t = r => r = s
func transitive<S,T,R>(s:S.Type = S.self, t:T.Type = T.self,r:R.Type = R.self) -> (Eq<S,T>) -> (Eq<T,R>) -> Eq<R,S> {
return { (e1: Eq<S,T>) -> ((Eq<T,R>) -> Eq<R,S>) in
{ (e2: Eq<T,R>) -> Eq<R,S> in Eq<R,S>() }
}
}
// axiom1 : s = t => succ(s) = succ(t)
func axiom1<S,T>(s:S.Type = S.self, t:T.Type = T.self) -> (Eq<S,T>) -> Eq<Succ<S>,Succ<T>> {
return { (x:Eq<S,T>) -> Eq<Succ<S>, Succ<T>> in Eq<Succ<S>, Succ<T>>() }
}
// axiom2 : s + 0 = s
func axiom2<S>(s:S.Type = S.self) -> Eq<Add<S,Zero>,S> { return Eq<Add<S,Zero>,S>() }
// axiom3 : s + succ(t) = succ(s + t)
func axiom3<S,T>(s:S.Type = S.self, t:T.Type = T.self) -> Eq<Add<S,Succ<T>>, Succ<Add<S,T>>> { return Eq<Add<S,Succ<T>>, Succ<Add<S,T>>>() }
// proof1 : succ(zero) + succ(zero) = succ(zero + succ(zero))
// use axiom3
let proof1 : Eq<Add<Succ<Zero>,Succ<Zero>>, Succ<Add<Succ<Zero>,Zero>>> = axiom3()
// proof2 : succ(zero) + zero = succ(zero)
let proof2 : Eq<Add<Succ<Zero>, Zero>, Succ<Zero>> = axiom2()
// proof3 : succ( succ(zero) + zero ) = succ(succ(zero))
let proof3 : Eq<Succ<Add<Succ<Zero>, Zero>>,Succ<Succ<Zero>>> = axiom1()(proof2)
// proof4 : succ(succ(zero)) = succ(zero) + succ(zero)
let proof4 : Eq<Succ<Succ<Zero>>,Add<Succ<Zero>, Succ<Zero>>> = transitive()(proof1)(proof3)
// proof5 : succ(zero) + succ(zero) = succ(succ(zero))
let proof5 : Eq<Add<Succ<Zero>, Succ<Zero>>,Succ<Succ<Zero>>> = symmetric()(proof4)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment