Add the example package

src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala

@@ -0,0 +1,59 @@
+package me.cassayre.florian.masterproject.examples
+
+import scala.util.chaining.*
+import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
+import me.cassayre.florian.masterproject.front.proof.Proof.{*, given}
+import me.cassayre.florian.masterproject.front.parser.FrontMacro.{*, given}
+import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter.*
+import me.cassayre.florian.masterproject.front.printer.{FrontPrintStyle, KernelPrinter}
+import me.cassayre.florian.masterproject.front.theory.SetTheory.*
+
+@main def frontInteractiveProof1(): Unit = {
+  val s = SchematicFunctionLabel[0]("s")
+
+  // The first step is to provide the global environment, i.e. the underlying theory
+  given ProofEnvironment = newSetTheoryEnvironment()
+
+  val t0: Theorem = {
+    // To enter proof mode, the user should specify the conclusion of the fact to prove
+    val p = ProofMode(sequent"|- (!?a \/ ?b) <=> (?a => ?b)")
+    import p.*
+
+    // Then they should apply tactics to update and eventually eliminate the goals
+    apply(introRIff)
+    apply(introRImp)
+    apply(introRImp)
+    apply(introLOr)
+    apply(introLNot)
+    apply(introHypo)
+    apply(introHypo)
+
+    apply(introRImp)
+    apply(introROr)
+    apply(introLImp)
+    apply(introRNot)
+    apply(introHypo)
+
+    apply(introHypo)
+
+    // Once all the goals are eliminated, this method can be called to obtain a theorem
+    asTheorem()
+  }
+  // Note: this proof could in fact be made shorter, see `frontSolver`
+
+  // Axioms act as proven theorems, except that no proof is needed to use them
+  val axEmpty: Axiom = axiomEmpty.asJustified.display()
+
+  val t1: Theorem = {
+    val p = ProofMode(sequent"|- ({} in {}) => ?a")
+
+    p.apply(introRImp)
+    p.apply(elimRNot)
+    // Here we implicitly instantiate the axiom to match our goal
+    p.apply(justificationInst(
+      elimRForallS(RuleParameters(AssignedFunction(Notations.t, s)))(axEmpty).get
+    ))
+
+    p.asTheorem()
+  }
+}

src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala

@@ -0,0 +1,160 @@
+package me.cassayre.florian.masterproject.examples
+
+import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
+import me.cassayre.florian.masterproject.front.parser.FrontMacro.{*, given}
+import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter.*
+import me.cassayre.florian.masterproject.front.printer.{FrontPrintStyle, KernelPrinter}
+import me.cassayre.florian.masterproject.front.proof.Proof.{*, given}
+import me.cassayre.florian.masterproject.front.theory.SetTheory.*
+
+import scala.util.chaining.*
+
+@main def frontInteractiveProof2(): Unit = {
+  val (s, t, u, v) = (SchematicFunctionLabel[0]("s"), SchematicFunctionLabel[0]("t"), SchematicFunctionLabel[0]("u"), SchematicFunctionLabel[0]("v"))
+
+  given ProofEnvironment = newSetTheoryEnvironment()
+
+  val axExt: Axiom = axiomExtensionality.asJustified.display()
+  val axUnion: Axiom = axiomUnion.asJustified.display()
+  val axPower: Axiom = axiomPower.asJustified.display()
+  val defSubset: Axiom = definitionSubset.asJustified.display()
+
+  // 1. Generalize universal quantifiers
+
+  val thmExtSchema: Theorem = {
+    val t0 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, s)))(axExt).get
+    val t1 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, t)))(t0).get
+    t1
+  }.display()
+
+  val thmUnionSchema: Theorem = {
+    val t0 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, s)))(axUnion).get
+    val t1 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, t)))(t0).get
+    t1
+  }.display()
+
+  val thmPowerSchema: Theorem = {
+    val t0 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, s)))(axPower).get
+    val t1 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, t)))(t0).get
+    t1
+  }.display()
+
+  val thmSubsetSchema: Theorem = {
+    val t0 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, s)))(defSubset).get
+    val t1 = elimRForallS(RuleParameters(AssignedFunction(Notations.t, t)))(t0).get
+    t1
+  }.display()
+
+  // 2. Prove a lemma
+
+  val lemmaSubsetRefl = {
+    val p = ProofMode(sequent"|- (?s sub ?s) <=> ((?t in ?s) => (?t in ?s))")
+    import p.*
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, x => formula"$x <=> ((?t in ?s) => (?t in ?s))")
+        .withPredicate(Notations.a, formula"forall z. (z in ?s) => (z in ?s)")
+    ))
+    focus(1)
+    apply(rewrite(sequent"|- (?s sub ?s) <=> (forall z. (z in ?s) => (z in ?s))"))
+    apply(justificationInst(thmSubsetSchema))
+    apply(introRIff)
+    apply(introRImp)
+    apply(introLForall(RuleParameters(AssignedFunction(Notations.t, t))))
+    apply(introHypo)
+    apply(introRImp)
+    apply(weaken(left = Set(0)))
+    apply(introRForallS(RuleParameters(AssignedFunction(Notations.t, v))))
+    apply(solveProp)
+
+    asTheorem()
+  }
+
+  // 3. Prove the complete theorem
+
+  val thmUnionAny = {
+    val p = ProofMode(() |- unionSet(powerSet(s)) === s)
+    import p.*
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"forall z. (z in U(P(?s))) <=> (z in ?s)")
+    ))
+    focus(1)
+
+    apply(justification(
+      thmExtSchema(AssignedFunction(Notations.t, unionSet(powerSet(s))))(AssignedFunction(Notations.u, s))
+        .rewrite(sequent"|- (forall z. (z in U(P(?s))) <=> (z in ?s)) <=> (U(P(?s)) = ?s)")
+        .display()
+    ))
+
+    apply(introRForallS(RuleParameters(AssignedFunction(Notations.t, t))))
+
+
+    apply(RuleSubstituteRightIff(
+      RuleParameters()
+        .withConnector(Notations.f, x => formula"(?t in U(P(?s))) <=> $x")
+        .withPredicate(Notations.a, formula"exists y. (?t in y) /\ (y in P(?s))")
+    ))
+
+    apply(justificationInst(thmUnionSchema))
+
+    apply(introRIff)
+    apply(introRImp)
+    apply(introLExistsS(RuleParameters(AssignedFunction(Notations.t, u))))
+    apply(introLAnd)
+
+    apply(elimLSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"?u sub ?s")
+        .withPredicate(Notations.b, formula"?u in P(?s)")
+    ))
+    focus(1)
+    apply(weaken(left = Set(0), right = Set(0)))
+    apply(rewrite(sequent"|- (?u in P(?s)) <=> (?u sub ?s)"))
+    apply(justificationInst(thmPowerSchema))
+
+    apply(elimLSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"forall z. (z in ?u) => (z in ?s)")
+        .withPredicate(Notations.b, formula"?u sub ?s")
+    ))
+    focus(1)
+    apply(weaken(left = Set(0), right = Set(0)))
+    apply(rewrite(sequent"|- (?u sub ?s) <=> (forall z. (z in ?u) => (z in ?s))"))
+    apply(justificationInst(thmSubsetSchema))
+
+    apply(introLForall(RuleParameters(AssignedFunction(Notations.t, t))))
+    apply(solveProp)
+
+    apply(introRExists(RuleParameters(AssignedFunction(Notations.t, s))))
+    apply(solveProp)
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"?s sub ?s")
+    ))
+    focus(1)
+    apply(weaken(left = Set(0)))
+    apply(rewrite(sequent"|- (?s in P(?s)) <=> (?s sub ?s)"))
+    apply(justificationInst(thmPowerSchema))
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"(?t in ?s) => (?t in ?s)")
+    ))
+    focus(1)
+    apply(weaken(left = Set(0)))
+    apply(rewrite(sequent"|- (?s sub ?s) <=> ((?t in ?s) => (?t in ?s))"))
+    apply(justification(lemmaSubsetRefl))
+    apply(solveProp)
+
+    asTheorem()
+  }
+}

src/main/scala/me/cassayre/florian/masterproject/examples/frontMatching.scala

@@ -0,0 +1,118 @@
+package me.cassayre.florian.masterproject.examples
+
+import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
+import me.cassayre.florian.masterproject.front.proof.Proof.{*, given}
+import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter.*
+
+@main def frontMatching(): Unit = {
+  val (s, t) = (SchematicFunctionLabel[0]("s"), SchematicFunctionLabel[0]("t"))
+  val (cs, ct, cu) = (ConstantFunctionLabel[0]("s"), ConstantFunctionLabel[0]("t"), ConstantFunctionLabel[0]("u"))
+  val (a, b, c) = (SchematicPredicateLabel[0]("a"), SchematicPredicateLabel[0]("b"), SchematicPredicateLabel[0]("c"))
+  val (ca, cb, cc) = (ConstantPredicateLabel[0]("a"), ConstantPredicateLabel[0]("b"), ConstantPredicateLabel[0]("c"))
+  val f = SchematicConnectorLabel[1]("f")
+  val p = SchematicPredicateLabel[1]("p")
+  val cq = ConstantPredicateLabel[1]("q")
+  val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+  def contextsEqual(ctx1: UnificationContext, ctx2: UnificationContext): Boolean = {
+    def names(lambda: WithArityType[?]): Seq[String] = (0 until lambda.arity).map(i => s"unique_name_$i")
+    def normalizeFunction(lambda: LambdaFunction[?]): LambdaFunction[?] = {
+      val newParams = names(lambda).map(SchematicFunctionLabel.apply[0])
+      LambdaFunction.unsafe(
+        newParams,
+        instantiateTermSchemas(lambda.body, lambda.parameters.zip(newParams).map { case (l1, l2) => RenamedLabel.unsafe(l1, l2).toAssignment })
+      )
+    }
+    def normalizePredicate(lambda: LambdaPredicate[?]): LambdaPredicate[?] = {
+      val newParams = names(lambda).map(SchematicFunctionLabel.apply[0])
+      LambdaPredicate.unsafe(
+        newParams,
+        instantiateFormulaSchemas(lambda.body, lambda.parameters.zip(newParams).map { case (l1, l2) => RenamedLabel.unsafe(l1, l2).toAssignment }, Seq.empty, Seq.empty)
+      )
+    }
+    def normalizeConnector(lambda: LambdaConnector[?]): LambdaConnector[?] = {
+      val newParams = names(lambda).map(SchematicPredicateLabel.apply[0])
+      LambdaConnector.unsafe(
+        newParams,
+        instantiateFormulaSchemas(lambda.body, Seq.empty, lambda.parameters.zip(newParams).map { case (l1, l2) => RenamedLabel.unsafe(l1, l2).toAssignment }, Seq.empty)
+      )
+    }
+    def normalizeContext(ctx: UnificationContext): UnificationContext =
+      UnificationContext(
+        ctx.predicates.view.mapValues(normalizePredicate).toMap,
+        ctx.functions.view.mapValues(normalizeFunction).toMap,
+        ctx.connectors.view.mapValues(normalizeConnector).toMap,
+        ctx.variables,
+      )
+    normalizeContext(ctx1) == normalizeContext(ctx2)
+  }
+
+  val sep = ", "
+  def prettyContext(ctx: UnificationContext): String = {
+    def schema(label: SchematicLabelType): String = s"?${label.id}"
+    def assignment(variable: String, value: String): String = s"$variable |-> $value"
+    def lambda(parameters: Seq[SchematicLabelType], body: String): String =
+      if(parameters.isEmpty) body else s"(${parameters.map(schema).mkString(sep)}) |=> $body"
+    "{" +
+      (ctx.connectors.toSeq.map { case (k, v) => assignment(schema(k), lambda(v.parameters, prettyFormula(v.body))) } ++
+        ctx.predicates.toSeq.map { case (k, v) => assignment(schema(k), lambda(v.parameters, prettyFormula(v.body))) } ++
+        ctx.functions.toSeq.map { case (k, v) => assignment(schema(k), lambda(v.parameters, prettyTerm(v.body))) } ++
+        ctx.variables.toSeq.map { case (k, v) => assignment(k.id, v.id) }
+        ).mkString(sep) +
+      "}"
+  }
+
+  extension (left: Option[UnificationContext]) {
+    infix def ==?==(right: Option[UnificationContext]): Unit = {
+      (left, right) match {
+        case (Some(l), Some(r)) if !contextsEqual(l, r) =>
+          throw AssertionError(s"Expected ${prettyContext(r)}, got ${prettyContext(l)}")
+        case (Some(l), None) =>
+          throw AssertionError(s"Expected a failure, got ${prettyContext(l)}")
+        case (None, Some(r)) =>
+          throw AssertionError(s"Expected ${prettyContext(r)}, got a failure")
+        case (None, None) =>
+          println("Result: (failure)")
+        case (Some(l), _) =>
+          println(s"Result: ${prettyContext(l)}")
+      }
+      println()
+    }
+  }
+
+  var index = 1
+  def matching(patterns: PartialSequent*)(values: Sequent*)(ctx: UnificationContext = UnificationContext()): Option[UnificationContext] = {
+    println(s"#$index")
+    index += 1
+    println(s"Patterns: ${patterns.map(prettyPartialSequent(_)).mkString(sep)}  |  Values: ${values.map(prettySequent(_)).mkString(sep)}  |  Partial assignment: ${prettyContext(ctx)}")
+    val (patternsISeq, valuesISeq) = (patterns.toIndexedSeq, values.toIndexedSeq)
+
+    unifyAndResolve(
+      patternsISeq,
+      valuesISeq,
+      IndexedSeq.empty,
+      ctx,
+      matchIndices(Map.empty, patternsISeq, valuesISeq).head,
+    ).map(_._2)
+  }
+
+  val U = UnificationContext()
+  val A = Assigned
+
+  matching(||- (a /\ cb))(|- (cc /\ cb))() ==?== Some(U + A(a, cc))
+  matching(||- (a /\ b))(|- (ca /\ cb))(U + A(a, cb)) ==?== None
+  matching(||- (a))(|- (cc /\ cb))(U + A(a, cb /\ cc)) ==?== Some(U + A(a, cb /\ cc))
+  matching(||- (a))(|- (a /\ cb))() ==?== Some(U + A(a, a /\ cb))
+  matching(||- (a /\ a))(|- ((cb \/ cc) /\ (cc \/ cb)))() ==?== Some(U + A(a, cb \/ cc))
+  matching(||- (p(ct)))(|- (ct === cu))() ==?== Some(U + A(p, LambdaPredicate[1](x => x === cu)))
+  matching(||- (p(t)))(|- (ct === cu))() ==?== None
+  matching(||- (p(t)))(|- (ct === cu))(U + A(t, ct)) ==?== Some(U + A(p, LambdaPredicate[1](x => x === cu)) + A(t, ct))
+  matching(||- (p(t)))(|- (ct === cu))(U + A(p, LambdaPredicate[1](x => x === cu))) ==?== Some(U + A(p, LambdaPredicate[1](x => x === cu)) + A(t, ct))
+  matching(||- (p(t), cq(t)))(|- (ct === cu, cq(ct)))() ==?== Some(U + A(p, LambdaPredicate[1](x => x === cu)) + A(t, ct))
+  matching(||- (f(a /\ cb)))(|- ((a /\ b) \/ (b /\ a)))() ==?== None
+  matching(||- (f(a /\ cb), a))(|- (cc \/ (cb /\ ca), ca))() ==?== Some(U + A(a, ca) + A(f, LambdaConnector[1](x => cc \/ x)))
+  matching(||- (exists(x, cq(x))))(|- (exists(y, cq(y))))() ==?== Some(U + (x, y))
+  matching(||- (exists(x, a)))(|- (exists(y, y === cu)))() ==?== None
+  matching(||- (exists(x, p(x))))(|- (exists(y, y === cu)))() ==?== Some(U + (x, y) + A(p, LambdaPredicate[1](x => x === cu)))
+
+}