Proving properties in Scala 3

relationships.scala

import language.implicitConversions
import compiletime.ops.int.*
import compiletime.ops.string.*


object Relationships:
  protected sealed trait Theorem
  protected class ==>[P, Q]

  type Has[T <: Theorem]
  type :|[O, T <: Theorem] = O & Has[T]

  trait Greater[B <: Int] extends Theorem
  object Greater:
    inline def apply[B <: Int](x: Int)(using (B < x.type) =:= true): Int :| Greater[B] = x.asInstanceOf

  trait MaxLength[B <: Int] extends Theorem
  object MaxLength:
    inline def apply[B <: Int](x: String)(using (B >= Length[x.type]) =:= true): String :| MaxLength[B] = x.asInstanceOf

  inline given applies_to[O, T1 <: Theorem, T2 <: Theorem](using T1 ==> T2): Conversion[O :| T1, O :| T2] = _.asInstanceOf

  given greater_transitive[B1 <: Int, B2 <: Int](using (B1 < B2) =:= true): (Greater[B2] ==> Greater[B1]) = ==>()
  given bounded_transitive[B1 <: Int, B2 <: Int](using (B1 >= B2) =:= true): (MaxLength[B2] ==> MaxLength[B1]) = ==>()
import Relationships.*


/* examples */
val x: Int :| Greater[5] = Greater(10)
val y: Int :| Greater[0] = x

// val yc: Int :| Greater[10] = x // does not compile

val test: String :| MaxLength[10] = MaxLength("Testing")

def println_max_10(s: String :| MaxLength[42]): Unit =
  println(s.take(42))

println_max_10(test)
println_max_10(MaxLength("random"))
//  println_max_10("random")
//  println_max_10(MaxLength[43]("The quick brown fox jumps over the lazy dog"))

tuple_laws.scala

import language.implicitConversions

/* helpers */
class Inverse[F[_], G[_]]
type MatchSome[X] = X match { case Some[t] => t }
def matchSome[X](x: X): MatchSome[X] = x match { case k: Some[t] => k.get }
given Inverse[MatchSome, Some] = new Inverse

extension [T](x: T) inline def widen[S >: T]: S = x

/* laws */
given [X, Y](using ev: X =:= Y): Conversion[X, Y] = ev(_)
given simplify_map_map[T <: Tuple, F[_], G[_]]: (Tuple.Map[Tuple.Map[T, G], F] =:= Tuple.Map[T, [X] =>> F[G[X]]]) = <:<.refl[Any].asInstanceOf
given simplify_map_id[T <: Tuple]: (Tuple.Map[T, [X] =>> X] =:= T) = <:<.refl[Any].asInstanceOf
given mapinverse_inversemap[T <: Tuple, F[_], G[_]](using Inverse[F, G]): (Tuple.Map[T, F] =:= Tuple.InverseMap[T, G]) = <:<.refl[Any].asInstanceOf
given simplify_map_inversemap[T <: Tuple, F[_]]: (Tuple.InverseMap[Tuple.Map[T, F], F] =:= T) = <:<.refl[Any].asInstanceOf


/* examples */
def f[T <: Tuple](t: T): Tuple.Map[T, [X] =>> Option[List[X]]] =
  val tl: Tuple.Map[T, List] = t.widen.map([X] => (x: X) => List(x))
  val tol: Tuple.Map[Tuple.Map[T, List], Option] = tl.widen.map([X] => (x: X) => Option(x))
  tol

f(4, 2)


def g[T <: Tuple](t: T): T =
  val nt: Tuple.Map[T, [X] =>> X] = t.widen.map[[X] =>> X]([X] => (x: X) => {println(x); x})
  nt

g(4, 2)


def h[T <: Tuple](to: T): Tuple.InverseMap[T, Some] =
  val t: Tuple.Map[T, MatchSome] = to.widen.map(([X] => (x: X) => matchSome(x)))
  t

def back_forth[T <: Tuple](t: T): T =
  val nt = h(t.map([X] => (x: X) => Some(x)))
  nt

back_forth(4, 2)