Reseal Proof trait, upgrade to Scala 3.4.2 (#225)

* Explicitly mark `of` and `has` as infix

* Reseal `Proof`

* Scala 3.4 automated rewrites

* Change scala version, set dynamic cross versions

* Update changelog

CHANGES.md

@@ -1,5 +1,10 @@
 # Change List
 
+## 2024-07-22
+Resealed the `Proof` trait following a fix of the relevant compiler bug [scala/scala3#19031](https://github.com/scala/scala3/issues/19031). 
+
+Updated to Scala 3.4.2, and relevant minor syntax changes from `-rewrite -source 3.4-migration`.
+
 ## 2024-04-12
 Addition of the Congruence tactic, solving sequents by congruence closure using egraphs.
 

build.sbt

@@ -15,22 +15,22 @@ ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
 ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
 
+val scala2 = "2.13.8"
+val scala3 = "3.4.2"
+
 val commonSettings = Seq(
-  crossScalaVersions := Seq("3.3.3"),
+  crossScalaVersions := Seq(scala3, scala2),
   run / fork := true
 )
 
-val scala2 = "2.13.8"
-val scala3 = "3.3.3"
-
 val commonSettings2 = commonSettings ++ Seq(
   scalaVersion := scala2,
   scalacOptions ++= Seq("-Ypatmat-exhaust-depth", "50")
 )
 val commonSettings3 = commonSettings ++ Seq(
   scalaVersion := scala3,
   scalacOptions ++= Seq(
-    "-language:implicitConversions",
+    "-language:implicitConversions"
   ),
   javaOptions += "-Xmx10G",
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",

lisa-sets/src/main/scala/lisa/automation/Apply.scala

@@ -112,7 +112,7 @@ class Apply(using val lib: Library, val proof: lib.Proof)(thm: proof.Fact) exten
     * @param tSubst the assignment for term variables
     */
   private def substitute(using _proof: lib.Proof)(fact: _proof.Fact, fSubst: FormulaSubstitution, tSubst: TermSubstitution): _proof.Fact =
-    fact.of(fSubst.toFSubstPair: _*).of(tSubst.toTSubstPair: _*)
+    fact.of(fSubst.toFSubstPair*).of(tSubst.toTSubstPair*)
 
   /**
   * Applies on method with a varargs instead of a sequence.

lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala

@@ -178,14 +178,14 @@ object CommonTactics {
 
           // Instantiate terms in the definition
           val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
-          val P = definition.f.substitute(subst: _*)
+          val P = definition.f.substitute(subst*)
           val expected = P.substitute(y := fxs)
           if (!F.isSame(expected, bot.right.head)) {
             return proof.InvalidProofTactic("Right-hand side of bottom sequent should be of the form P(f(xs)).")
           }
 
           TacticSubproof {
-            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
             lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
             lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
             lib.thenHave(P.substitute(y := fxs)) by Restate
@@ -218,7 +218,7 @@ object CommonTactics {
           // val instantiations: Seq[(F.SchematicTermLabel, F.LambdaTermTerm)] = vars.zip(xs.map(x => F.LambdaTermTerm(Seq(), x)))
 
           val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
-          val P = definition.f.substitute(subst: _*)
+          val P = definition.f.substitute(subst*)
           // Instantiate terms in the definition
           // val P = F.LambdaTermFormula(Seq(y), expr(xs))
 
@@ -248,7 +248,7 @@ object CommonTactics {
           }
 
           TacticSubproof {
-            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
             lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
             lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
             lib.thenHave(P.substitute(y := fxs)) by Restate

lisa-sets/src/main/scala/lisa/automation/Substitution.scala

@@ -236,7 +236,7 @@ object Substitution {
               leftContextReduced.termRules.map { case (_, (rule, subst)) =>
                 sourceOf.get(rule) match {
                   case Some(f: proof.Fact) =>
-                    f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+                    f.of(subst.toSeq.map((l, r) => (l := r))*)
                   // case Some(j: lib.theory.Justification) =>
                   //   j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
                   case _ =>
@@ -246,7 +246,7 @@ object Substitution {
                 leftContextReduced.formulaRules.map { case (_, (rule, subst)) =>
                   sourceOf.get(rule) match {
                     case Some(f: proof.Fact) =>
-                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
                     // case Some(j: lib.theory.Justification) =>
                     //   j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
                     case _ =>
@@ -257,7 +257,7 @@ object Substitution {
               rightContextReduced.termRules.map { case (_, (rule, subst)) =>
                 sourceOf.get(rule) match {
                   case Some(f: proof.Fact) =>
-                    f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+                    f.of(subst.toSeq.map((l, r) => (l := r))*)
                   // case Some(j: lib.theory.Justification) =>
                   //   j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
                   case None =>
@@ -267,7 +267,7 @@ object Substitution {
                 rightContextReduced.formulaRules.map { case (_, (rule, subst)) =>
                   sourceOf.get(rule) match {
                     case Some(f: proof.Fact) =>
-                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
                     // case Some(j: lib.theory.Justification) =>
                     //   j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
                     case None =>

lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala

@@ -40,7 +40,7 @@ object TypeLib extends lisa.Main {
   // C |> D is the functional class of functionals from the class C to the class D
   // F is C |> D desugars into ∀(x, (x is C) => (F(x) is D))
 
-  val testTheorem = Theorem((x is A, f is (A |=> B), F is (A |=> B) |> (A |=> B) ) |- (F(f)*(x) is B)) {
+  val testTheorem = Theorem((x `is` A, f `is` (A |=> B), F `is` (A |=> B) |> (A |=> B) ) |- (F(f)*(x) `is` B)) {
     have(thesis) by TypeChecker.prove
   }
 
@@ -87,7 +87,7 @@ object TypeSystem  {
 
   case class FunctionalClass(in: Seq[Class], args: Seq[Variable], out: Class, arity: Int) {
     def formula[N <: Arity](f: (Term**N |-> Term)): Formula = 
-      val inner = (args.zip(in.toSeq).map((term, typ) => (term is typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) is out)
+      val inner = (args.zip(in.toSeq).map((term, typ) => (term `is` typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) `is` out)
       args.foldRight(inner)((v, form) => forall(v, form))
 
     override def toString(): String = in.map(_.toStringSeparated()).mkString("(", ", ", ")") + " |> " + out.toStringSeparated()
@@ -112,8 +112,8 @@ object TypeSystem  {
   }
 
   extension [A <: Class](t: Term) {
-    def is(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
-    def ::(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
+    def is(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
+    def ::(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
     def @@(t2: Term): AppliedFunction = AppliedFunction(t, t2)
     def *(t2: Term): AppliedFunction = AppliedFunction(t, t2)
   }
@@ -318,7 +318,7 @@ object TypeSystem  {
 
   extension (c: Constant) {
     def typedWith[A <: Class](typ:A)(justif: JUSTIFICATION) : TypedConstant[A] = 
-      if justif.statement.right.size != 1  || justif.statement.left.size != 0 || !K.isSame((c is typ).asFormula.underlying, justif.statement.right.head.underlying) then
+      if justif.statement.right.size != 1  || justif.statement.left.size != 0 || !K.isSame((c `is` typ).asFormula.underlying, justif.statement.right.head.underlying) then
         throw new IllegalArgumentException(s"A proof of typing of $c must be of the form ${c :: typ}, but the given justification shows ${justif.statement}.")
       else TypedConstant(c.id, typ, justif)
   }
@@ -345,7 +345,7 @@ object TypeSystem  {
       var typingError: proof.ProofTacticJudgement = null
       bot.right.find(goal =>
         goal match
-          case (term is typ) => 
+          case (term `is` typ) => 
             val ptj = typecheck(using SetTheoryLibrary)(context.toSeq, term, Some(typ))
             if ptj.isValid then
               success = ptj
@@ -378,21 +378,21 @@ object TypeSystem  {
           def innerTypecheck(context2: Map[Term, Seq[Class]], term:Term, typ:Option[Class]): Class= {
             val possibleTypes = typingAssumptions.getOrElse(term, Nil)
             if typ == Some(any) then 
-              have(term is any) by Restate.from(TypeLib.any.definition of (x := term))
+              have(term `is` any) by Restate.from(TypeLib.any.definition of (x := term))
               any
             else if typ.isEmpty && possibleTypes.size >=1 then
-              have(term is possibleTypes.head) by Restate
+              have(term `is` possibleTypes.head) by Restate
               possibleTypes.head
             else if (typ.nonEmpty && possibleTypes.contains(typ.get)) then
-              have(term is typ.get) by Restate
+              have(term `is` typ.get) by Restate
               typ.get
             else term match
               case tc: TypedConstant[?] => 
                 if typ.isEmpty then
-                  have(tc is tc.typ) by Restate.from(tc.justif)
+                  have(tc `is` tc.typ) by Restate.from(tc.justif)
                   tc.typ
-                else if K.isSame((tc is typ.get).asFormula.underlying, (tc is tc.typ).asFormula.underlying) then
-                  have(tc is typ.get) by Restate.from(tc.justif)
+                else if K.isSame((tc `is` typ.get).asFormula.underlying, (tc `is` tc.typ).asFormula.underlying) then
+                  have(tc `is` typ.get) by Restate.from(tc.justif)
                   typ.get
                 else throw TypingException("Constant " + tc + " expected to be of type " + typ + " but has type " + tc.typ + ".")
 
@@ -404,18 +404,18 @@ object TypeSystem  {
                 funcType match
                   case inType |=> outType => typ match
                     case None => 
-                      if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
-                        have(term is outType) by Tautology.from(
+                      if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+                        have(term `is` outType) by Tautology.from(
                           funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
                           funcProof,
                             argProof
                         )
                         outType
                       else throw 
                         TypingException("Function " + func + " found to have type " + funcType + ", but argument " + arg + " has type " + argType + " instead of expected " + inType + ".")
-                    case Some(typ) if K.isSame((term is typ).asFormula.underlying, (term is outType).asFormula.underlying) =>
-                      if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
-                        have(term is outType) by Tautology.from(
+                    case Some(typ) if K.isSame((term `is` typ).asFormula.underlying, (term `is` outType).asFormula.underlying) =>
+                      if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+                        have(term `is` outType) by Tautology.from(
                           funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
                           funcProof,
                             argProof
@@ -450,7 +450,7 @@ object TypeSystem  {
                       labelTypes.find((labelType, step) =>
                         labelType.arity == args.size && 
                         (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) => 
-                          K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying) //
+                          K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying) //
                         )
                       ) match 
                         case None =>
@@ -461,28 +461,28 @@ object TypeSystem  {
                           val in: Seq[Class] = labelType.in.toSeq
                           //val labelProp = labelType.formula(label.asInstanceOf)
                           val labelPropStatement = step()
-                          val labInst = labelPropStatement.of(args: _*)
+                          val labInst = labelPropStatement.of(args*)
                           val subst = (labelType.args zip args).map((v, a) => (v := a))
                           val newOut: Class = out match {
-                            case t: Term => t.substitute(subst: _*)
-                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+                            case t: Term => t.substitute(subst*)
+                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
                           }
-                          have(term is newOut) by Tautology.from(
-                            (argTypesProofs :+ labInst ) : _*
+                          have(term `is` newOut) by Tautology.from(
+                            (argTypesProofs :+ labInst )*
                           )
                           newOut
                     case Some(typValue) => 
                       labelTypes.find((labelType, step) =>
                         labelType.arity == args.size && 
                         (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) => 
-                          K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying)
+                          K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying)
                         ) && {
                           val subst = (labelType.args zip args).map((v, a) => (v := a))
                           val newOut: Class = labelType.out match {
-                            case t: Term => t.substitute(subst: _*)
-                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+                            case t: Term => t.substitute(subst*)
+                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
                           }
-                          K.isSame((term is newOut).asFormula.underlying, (term is typValue).asFormula.underlying)
+                          K.isSame((term `is` newOut).asFormula.underlying, (term `is` typValue).asFormula.underlying)
 
                         }
                       ) match
@@ -493,8 +493,8 @@ object TypeSystem  {
                           val in: Seq[Class] = labelType.in.toSeq
                           //val labelProp = labelType.formula(label.asInstanceOf)
                           val labelPropStatement = step()
-                          have(term is typValue) by Tautology.from(
-                            (argTypesProofs :+ labelPropStatement.of(args: _*) ) : _*
+                          have(term `is` typValue) by Tautology.from(
+                            (argTypesProofs :+ labelPropStatement.of(args*) )*
                           )
                           typValue
 

lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala

@@ -201,7 +201,7 @@ object ADTSyntax {
       val semanticCons = trimmedNames.tail.zip(syntacticCons).map(SemanticConstructor(_, _, syntacticADT))
       val semanticADT = SemanticADT[N](syntacticADT, semanticCons)
       val cons = semanticCons.map(Constructor(_)) 
-      (ADT[N](semanticADT, cons), new constructors[N](cons : _*))
+      (ADT[N](semanticADT, cons), new constructors[N](cons*))
 
   }
 
@@ -356,7 +356,7 @@ object ADTSyntax {
       * @param adt the ADT
       * @return a tuple containing the ADT and its constructors
       */
-    private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors : _*))
+    private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors*))
 
     /**
       * Outputs a polymorphic ADT and constructors from a user specification
@@ -514,7 +514,7 @@ object ADTSyntax {
       val subst = adtVar -> consTerm
 
       val assumptions = 
-        (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _)) : _*))))
+        (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _))*))))
         ++ 
         cons.underlying.syntacticSignature(vars).filter(_._2 == Self).map((v, _) => prop.substitute(adtVar -> v)))
 

lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala

@@ -265,7 +265,7 @@ private[adt] object ADTDefinitions {
     def substitute(p: SubstPair*): ConstructorArgument = 
       this match
         case Self => Self
-        case GroundType(t) => GroundType(t.substitute(p : _*))
+        case GroundType(t) => GroundType(t.substitute(p*))
   }
 
   /**

lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala

@@ -47,10 +47,10 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
 
     val prop = lambda[Term, Formula](x, propFun(x))
     val typeVariablesSubstPairs = adt.typeVariables.toSeq.zip(typeVariablesSubst).map(SubstPair(_, _))
-    val instTerm = adt(typeVariablesSubst : _*)
+    val instTerm = adt(typeVariablesSubst*)
 
-    adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop)): _*)) ( (acc, c) =>
-      val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs : _*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
+    adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop))*)) ( (acc, c) =>
+      val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
         val (v, ty) = el
         val accRight: Formula = acc2.statement.right.head
         ty match 
@@ -140,7 +140,7 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
 
         val prop = inferedProp.getOrElse(bot.right.head)
         val propFunction = (t: Term) => inferedProp.getOrElse(bot.right.head).substitute(inferedVar -> t)
-        val assignment = inferedVar :: inferedADT(inferedArgs : _*)
+        val assignment = inferedVar :: inferedADT(inferedArgs*)
         val context = (if inferedProp.isDefined then bot else bot -<< assignment).left
         val builder = ADTSyntax.CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)]((context |- prop, inferedArgs, inferedVar))
         cases(using builder)