* Move theorems about functions

* Add function specific nomenclature

* Add constant functions, replace definitions in types module

* Add Sigma and Pi definitions

* Remove app from TypeLib

* Revert changes to ADTExample

* Simplify FunctionProperties imports

---------

Co-authored-by: SimonGuilloud <simon.guilloud@epfl.ch>

* Move scallion and silex dependencies to jars

* Bump version to 0.7

* Make tests fork JVM correctly

* Update sbt version

* Update CI action version tags

* fix tests, small cleaning in congruence algorithm.

* further simplification

* more minor improvements to congruence

* update CHANGES.md

* old

* Update project to scala version 3.5.1. Rewrite depreciated syntax.
Hide scallion warning report.

* update changelist

* minonr fix, mark n and u infix in Lattices.scala.

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

* Reseal `Proof`

* Scala 3.4 automated rewrites

* Change scala version, set dynamic cross versions

* Update changelog

* More sensible multi line strings, up scalafmt version

* Upgrade sbt version

* Upgrade sbt plugins

* Upgrade Scala version to 3.3.3

* Update library dependencies

* Expose library main classes

* Remove infinite loop (?)

* Uncomment examples, move Goeland examples to separate object

* Scala fmt

* Comment SimpleTautology

Add a tactic called "Congruence".
This tactic tries to prove a sequent by congruence.
Consider the congruence closure of all terms and formulas in the sequent, with respect to all === and <=> left of the sequent.
The sequent is provable by congruence if one of the following conditions is met:
- The right side contains an equality s === t or equivalence a <=> b provable in the congruence closure.
- The left side contains an negated equality !(s === t) or equivalence !(a <=> b) provable in the congruence closure.
- There is a formula a on the left and b on the right such that a and b are congruent.
- There are two formulas a and !b on the left such that a and b are congruent.
- There are two formulas a and !b on the right such that a and b are congruent.
- The sequent is Ol-valid without equality reasoning
Note that complete congruence closure modulo OL is an open problem.

The tactic uses an egraph datastructure to compute the congruence closure.
The egraph itselfs relies on two underlying union-find datastructure, one for terms and one for formulas.
The union-finds are equiped with an explain method that produces a path between any two elements in the same equivalence class.
Each edge of the path can come from an external equality, or be the consequence of congruence.
The tactic uses uses this path to produce needed proofs.

Implements basis of a type system with type checking, ADTs. induction and more.
Co-authored-by: SimonGuilloud <sim-guilloud@bluewin.ch>
Co-authored-by: Simon Guilloud <simon.guilloud@bluewin.ch>
Co-authored-by: Sankalp Gambhir <sankalp.gambhir42@gmail.com>

This adds support for Goéland as a proof tactic, and for parsing of proofs in SC-TPTP format.

* Swap 'or' and 'and' in ligature column typo

* Add missing tautology tactic reference

* Fix other small typos in manual

* Fix alignment in kernel chapter

* Typos in prooflib and set theory

* Regenerate lisa manual

* Apply tactic

* Implement draft option.

While developing proofs and theories, can activate a draft option that will only check the current worked-on file and assume without checking any external theorem. This prevents having to verify the whole library at every run.

Fix README to take the folder change of the reference manual into account. Small improvements to lattices tutorial.

Minor fix to Lattices tutorial

typeset lattices example and solutions, improvements to pretty printing

* Add the file CHANGES.md

* tracking inconsistencies

* implement a first version of substeq2

* tracking a bug

* 2-version works

* removed all version, renamed versions 2 to normal. All seems to work (including Recursion.scala). Haven't run tests yet, nor tested on function substitutions

* All tests and the library work. Added sanity checks for substitution steps.

* Add tests

* scalafix, scalafmt

* update CHANGES.md

* "of" for quantified facts has been implemented and tested.

* manual and changelist updated,  order between forall and free instantiation swapped. scalafix, scalafmt.

* correct typos

* refman is the directory for manul. It has a Makefile

* Format changes (b5, small margin) to reference manual

* LISA becomes Lisa

* pull out title page

* Formatted kernel proof system to fit pages

* wider margins

* Fixed reference

* change margins again. Added text showing margin width with our font is similar to that of LNCS

This PR introduces methods witness, t.replace, t.collect, t.map and t.filter. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.

* Readd failed substitution reporting

* File Changes

* Upgrade to 3.3.1 disabling pattern matching checks

* Fixes for build

* scalafix

* Fix reference to kernel formula

* File changes

* Add colors to Branch representation in Tableaux, try to optimize it.

* Improves Tableau with a weight-based heuristic for picking substitution. Also improve printing of Branches with colors, for additional reading clarity when debugging.

* scalafix, scalafmt

* Renamed some elements of the formula hierarchy using the word "atomic"

* removed the match type for ***. Instead, use opaque types and extension methods. Should be a bit more efficient and less prone to dotty bugs

* remove ***. Only ** left

* removing apply for sequences (use applyUnsafe)

* mostly good but one theorem doesn't pass anymore

* everything goes, no more *** (i.e. no match type)

* progress

* PredKer

* mend

* ConstantAtomicLabel, AtomicFormula

* All atomic renaming completed

* back to compile

* finished tests, removed ConsOrPred

* next step: Removes contravariant labels and terms and formulas extending |->

* finish predicates, compiles

* progress, Binders to sort and organize, some renaming to do in other files. Can remove - in labels.

* finished cleaning and uniformizing definitions in Commons.scala, adapted other files accordingly. Compiles, tests passes, formated.

* re-checked some warning, removed some redundant type checks.

* fix substituteUnsafe2

* Add "lisa-sets / compile" and "lisa-examples / compile" to the CI.

* fix tableau incompleteness (was caused by impossibility of self-unification)

* scalafix, scalafmt

* remove lingering //println

Reorganize and clean up files: Remove old unussed files, move the root project to lisa-sets, change lisa.mathematics to lisa.maths, some more.

    -Add ids to terms like for formulas
    -Add serialization of proofs. Theorems can be serialized to binary files and loaded back on later run.
    -On my machine, running everything up to Recursion.scala takes 19s instead of 24s.
    -Does no hash consing, but simple optimizations to proof size (remove consecutive rewrites, flatten subproofs)
    -Cleans up the distinction between fullName (with the whole path, should be unique) and name (just the last part, possibly duplicate across different files/domains).
    -Good completion of documentation in WithTheorems
    -checkProofs does not print proofs of more thant 100 steps now.
    -fixed an indexing bug in ShrinkProof.flattenProof
    -Suite of tests for serialization, export then load a collection of theorems.
    -Push suite of tests for Tableaux tactic that were missing.

* Update README

* Swap publications

Co-authored-by: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Co-authored-by: SimonGuilloud <simon.guilloud@bluewin.ch>

* improved printing, allow return in TacticSubproof

* weird issues

* fix bugs, improve printing andextractor paterns

* scalafix, scalafmt

* Fix small bug in asFront

* super condensed propositional tableau with eqChecker data

* work on princess

* Start working on princess-lisa

* Continued work on princess integration

* more tinkering

* trying some tableau implementation

* continue work on ATP

* Mostly working, problem with test 14 (with functions).

* test 14 does pass (make variables names unique)

* improvements on Tableau

* Proof production is completely correct!

* pruning implemented

* Tableau integreated as a tactic. Working on all theorems of the Quantifiers file, except for those with equality

* integrating tests

* Integrated tests

* clean some files

* scalafix, scalafmt

* fix unsoundness in Cut, LeftOr, RightAnd and RightIff proof checking. Correct Tableau prover accordingly.

* Adapt cut proof checking

* Adapt LeftOr proof checking

* Adapt RightAnd proof checking

* Adapting RightIff proof checking and better reporting

* scalafmt

* scalafix, scalafmt

---------

Co-authored-by: Sankalp Gambhir <sankalp.gambhir47@gmail.com>

* Put list example files in a different branch

* 2 exercises

* Merge, remove ref to Lab4

* super condensed propositional tableau with eqChecker data

* work on princess

* Start working on princess-lisa

* Continued work on princess integration

* more tinkering

* trying some tableau implementation

* continue work on ATP

* Mostly working, problem with test 14 (with functions).

* test 14 does pass (make variables names unique)

* improvements on Tableau

* Proof production is completely correct!

* pruning implemented

* Tableau integreated as a tactic. Working on all theorems of the Quantifiers file, except for those with equality

* integrating tests

* Integrated tests

* clean some files

* scalafix, scalafmt

* Starting a layer of abstraction.

* swrdgv

* sedgf

* ONgoing work. FOL structure mostly implemented, substitutions ongoing.

* continued

* further changes

* LisaObject has a self type being self

* More improvements on substitution

* More work

* multivar substitution

* improvements to MapProofTest

* finished fol, need to do prooflib

* started work on prooflib, cut plenty unused code in Library.scala

* more work on substitutions

* updated WithTheorems

* finished BasicSteptactics and substitutions

* more corrections of tactics using unifier

* fixed F and K imports

* finished PrrofHelpers and definitions. Definitions possibly not final

* Done most of the simpleDeducedSteps

* ongoing work on types

* added doc in Common.scala

* more doc, some simplification

* more doc and simplification of unneeded parts

* fixed some export issues. Commented some tests. translation left for the future.

* remove some debug code

* add missing files

* continue F integration. FInished with Set theory library files, now doing CommonTactics.scala (part is Dario's work).

* simplifier remaining

* renaming and mroe compatibility

* more adaptations

* merge build.sbt

* fixing

* transforming unification to Front

* weird issues with match types and dotty

* Compiles..? Need to simplify use of Arity in formula labels now. Finger crossed.

* add missing files

* still compiles

* Term**0 |-> Term

* Does not compile (dotty crash). Possibly due to covariant schematic labels.

* Labels are contravariant

* Weird "inherits conflicting instances of non-variant base trait LisaObject"

* structure seems to work; Constant extends ConstantFunctionSymbol[0], issue with case class (has to reimplement).

* back to the "common super type with case classes" structure

* finished predicates, compiles. Connector left

* Finished datastructure. TODO: Underlyings, Arity, uncomment asFront

* Compiles, checked arity and underlyings (mostly)

* Rehabilited asFront. Next stop, Substitution.

* porting unificationUtils

* half of unificationUtils done. Need to make Common even closer structure to kernel (variableFormula extends PredicateFormula)

* progress through unification

* compiles, progressing

* safe for reset

* only applySubst remaining.
Note: given
```scala
val s: Seq[(Variable, Term)]
```
`s.toMap` crashes dotty. Instead, do `Map(s*)`.

* Substitution done, everything compiles.

* rehabilited commented function

* utils tests compiles and pass.

* Finished setTheorzLibrary, close to finish OLPropositionalSolver

* Quantifiers.scala work, completed BasicProofTactic, implemented printing of terms and formulas

* progress on compilation and run of SetTheory.scala

* ordinals1 works

* Everything works, even example package. Some tests are still commentated. Simplified a couple proofs.

* Small improvements

* Ready for demo

* scalafix, scalafmt

* git add

* Add a Quick User Guide as chapter 1 of the reference manual

* small changes to manual

* update colors and date

* git add quickguide.tex

* small manual update

* Add a section on special characters (unicode and ligatures), spellcheck.