Scala example of Exercise 1 from CM 500 Logical Frameworks (see https://github.com/julianpeeters/hello-twelf/tree/main)

nat_even2.scala

sealed trait Nat
case object Zero extends Nat
case class Successor[N <: Nat](nat: N) extends Nat

sealed trait Even[+N]
case object EvenZ extends Even[Zero.type]
case class EvenS[N <: Nat](even: Even[N]) extends Even[Successor[Successor[N]]]

sealed trait Odd[N]
case class OddS[N <: Nat](even: Even2[N]) extends Odd[Successor[N]]

sealed trait Even2[+N]
case object Even2Z extends Even2[Zero.type]
case class Even2S[N <: Nat](odd: Odd[N]) extends Even2[Successor[N]]

// theorem: For all Nat, Even implies Even2
def evenImpliesEven2(even: Even[Nat]): Even2[Nat] =
  even match
  	case EvenZ => Even2Z
  	case EvenS(n) => Even2S(OddS(evenImpliesEven2(n)))

// proof of the claim `evenImpliesEven2`
println(evenImpliesEven2(EvenS(EvenZ)))
// Even2S(OddS(Even2Z))