Skip to content

Commit 3d37f17

Browse files
SimonGuilloudHaleOIC
SimonGuilloud
and
HaleOIC
authored
Reimplement HOL mechanizing. (epfl-lara#254)
* update .gitignore * upload current progress * have some steps further * Substitute failed at TApp * fix Pi definition error and finish TApp prove * finish T-Abs set boundary check * Finish T-Abs functionality proof * Finish TAbs typing rule proof * Fix the error from abs defintion * Refactor the code * finish proving beta reduction * FIx the definition of Pi * provide some examples * Basic typing system with dependent type works! * Add more readable syntax and examples * add a new example * feat: Enhance Set Theory Library with Cardinality Definitions and Universe Structure - Added Cardinal.scala to define cardinality concepts including equinumerosity and dominance. - Introduced Universe.scala to establish the structural definition of Tarski/Grothendieck Universes. - Implemented UniverseRank.scala to define the level of a universe and its properties. - Created Predef.scala to export essential definitions from the cardinal package. - Updated Helper.scala, Examples.scala, Symbols.scala, and TypingRules.scala to integrate new cardinality and universe functionalities. - Added new theorems related to universes and cardinalities, including Cantor's theorem and the structure of universes. * draft for a strong universe * Finish the foundamental theorem(replacementImpliesFunctionRange)'s proof * feat: Add new theorems for universe closure properties and enhance Symbols with proposition variable * refactor: Simplify theorem definitions and remove commented-out universe structure theorem * feat: Enhance typing rules and tactics with new theorems for universe handling and subset relations * feat: replace the TForm with two auxilliary theorems within tactics * refactor: change the project name * feat: Add README file for LISA-CoC module with project overview and setup instructions * fix: adjust compiler options * Introduce subtyping case into current system, support automatical type-lifting * reimplement types and on the way for HOL. * mostly done with vars and functions * typechecking works! * remove 4 sorries * closed to finished with HOL steps. * small * all tests pass * moved typing to implicit context, removed HOL-specific constructors and fixed most tests. * stable for HOL steps and tests. * removed context and replace with typed variables again. Tests don't quite pass but probably nothing complicated. * good amount of refactoring and cleaning * inst_types tested * about to remove all unused imports using scalafix. * cleanup, removed unused imports, add HOLAbstraction. * made test suites for HOL, various small improvements. * add examples * add file * add file * add missing file * scalafix, scalafmt * fix issues and remove duplicates. * add HOL tactics that auto-have, and rename. --------- Co-authored-by: HaleOIC <shinehale730@gmail.com> Co-authored-by: YunsongY <yunsongyang730@gmail.com> Co-authored-by: Yunsong Y <132993600+HaleOIC@users.noreply.github.com>
1 parent 5b13582 commit 3d37f17

105 files changed

Lines changed: 3316 additions & 930 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎build.sbt‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ val commonSettings3 = commonSettings ++ Seq(
3030
scalaVersion := scala3,
3131
scalacOptions ++= Seq(
3232
"-language:implicitConversions",
33-
//"-Wconf:msg=.*will never be selected.*:silent",
34-
"-Wconf:msg=.*trait or object is defined in the compilation unit.*:silent,msg=.*not declared infix.*:silent",
33+
"-Wconf:msg=.*is not declared infix*:silent",
34+
"-Wconf:msg=.*trait or object is defined in the compilation unit.*:silent",
3535
"-language:experimental.modularity"
3636
),
3737
javaOptions += "-Xmx10G",
@@ -105,3 +105,11 @@ lazy val examples = Project(
105105
.settings(commonSettings)
106106
.settings(commonSettings3)
107107
.dependsOn(root)
108+
109+
lazy val coc = Project(
110+
id = "lisa-coc",
111+
base = file("lisa-coc")
112+
)
113+
.settings(commonSettings)
114+
.settings(commonSettings3)
115+
.dependsOn(root)

‎lisa-sets/src/main/scala/lisa/Main.scala‎

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,4 @@ trait Main extends BasicMain {
2626
knownDefs.update(𝒫, Some(powerSetAxiom))
2727
knownDefs.update(⊆, Some(subsetAxiom))
2828

29-
extension (symbol: Constant[?]) {
30-
def definition: JUSTIFICATION = {
31-
getDefinition(symbol).get
32-
}
33-
def shortDefinition: JUSTIFICATION = {
34-
getShortDefinition(symbol).get
35-
}
36-
}
37-
3829
}

‎lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ package lisa
22

33
import lisa.kernel.proof.RunningTheory
44
import lisa.utils.fol.FOL.{_, given}
5-
import lisa.utils.prooflib.Library
65

76
import scala.annotation.targetName
87

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

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,5 @@
11
package lisa.automation.kernel
22

3-
import lisa.automation.Tautology
4-
import lisa.utils.K
5-
import lisa.utils.fol.{FOL => F}
6-
import lisa.utils.prooflib.BasicStepTactic._
7-
import lisa.utils.prooflib.ProofTacticLib.{_, given}
8-
import lisa.utils.prooflib.SimpleDeducedSteps._
9-
import lisa.utils.prooflib._
10-
113
object CommonTactics {
124
/*
135

‎lisa-sets/src/main/scala/lisa/automation/Congruence.scala‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
package lisa.automation
2-
import leo.datastructures.TPTP.AnnotatedFormula.FormulaType
2+
33
import lisa.utils.K
44
import lisa.utils.fol.FOL.{_, given}
55
import lisa.utils.prooflib.BasicStepTactic._
66
import lisa.utils.prooflib.ProofTacticLib._
7-
import lisa.utils.prooflib.SimpleDeducedSteps._
87
import lisa.utils.prooflib._
98

109
/**

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

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,14 @@
11
package lisa.automation
22

3-
import lisa.kernel.proof.RunningTheory
4-
import lisa.kernel.proof.SCProof
5-
import lisa.kernel.proof.SequentCalculus
6-
import lisa.utils.K
73
import lisa.utils.Printing.printList
8-
import lisa.utils.UserLisaException
94
import lisa.utils.collection.Extensions._
105
import lisa.utils.collection.VecSet
116
import lisa.utils.fol.{FOL => F}
127
import lisa.utils.prooflib.BasicStepTactic
13-
import lisa.utils.prooflib.ProofTacticLib.{_, given}
14-
import lisa.utils.prooflib.SimpleDeducedSteps
8+
import lisa.utils.prooflib.ProofTacticLib._
159
import lisa.utils.prooflib._
1610
import lisa.utils.unification.UnificationUtils._
1711

18-
import scala.annotation.nowarn
19-
import scala.collection.mutable.{Map => MMap}
20-
2112
import F.{rewrite => _, _, given}
2213

2314
object Substitution:
@@ -196,7 +187,7 @@ object Substitution:
196187
val rightFormulas = rightRules.map(_.toFormula)
197188
val preRight = rightRewrites.map(_.toLeft).toSet
198189
val postRight = rightRewrites.map(_.toRight).toSet
199-
val rightVars = rightRewrites.head.vars
190+
val rightVars = if rightRewrites.nonEmpty then rightRewrites.head.vars else Seq.empty
200191
val rightLambda = orAllOrFalse(rightRewrites.map(_.lambda))
201192
thenHave(rpremise.left |- orAllOrFalse(preRight)) by Restate
202193
thenHave(rightFormulas ++ rpremise.left |- orAllOrFalse(preRight)) by Weakening

‎lisa-sets/src/main/scala/lisa/automation/Tableau.scala‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ import lisa.utils.prooflib.OutputManager._
77
import lisa.utils.prooflib.ProofTacticLib._
88

99
import scala.collection.immutable.HashMap
10-
import scala.collection.immutable.HashSet
1110

1211
/**
1312
* Now need to deal with variables unifying with terms containing themselves

‎lisa-sets/src/main/scala/lisa/automation/atp/Egg.scala‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package lisa.automation.atp
2-
import lisa.tptp.KernelParser._
2+
33
import lisa.tptp.ProofParser._
44
import lisa.tptp.ProofPrinter._
55
import lisa.utils.K
@@ -9,7 +9,6 @@ import lisa.utils.prooflib.OutputManager
99
import lisa.utils.prooflib.ProofTacticLib._
1010

1111
import java.io._
12-
import scala.io.Source
1312
import scala.util.Failure
1413
import scala.util.Success
1514
import scala.util.Try

‎lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package lisa.automation.atp
2-
import lisa.tptp.KernelParser._
2+
33
import lisa.tptp.ProofParser._
44
import lisa.tptp.ProofPrinter._
55
import lisa.utils.K
@@ -10,7 +10,6 @@ import lisa.utils.prooflib.OutputManager
1010
import lisa.utils.prooflib.ProofTacticLib._
1111

1212
import java.io._
13-
import scala.io.Source
1413
import scala.util.Failure
1514
import scala.util.Success
1615
import scala.util.Try

‎lisa-sets/src/main/scala/lisa/automation/atp/Prover9.scala‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package lisa.automation.atp
2-
import lisa.tptp.KernelParser._
2+
33
import lisa.tptp.ProofParser._
44
import lisa.tptp.ProofPrinter._
55
import lisa.utils.K
@@ -9,7 +9,6 @@ import lisa.utils.prooflib.OutputManager
99
import lisa.utils.prooflib.ProofTacticLib._
1010

1111
import java.io._
12-
import scala.io.Source
1312
import scala.util.Failure
1413
import scala.util.Success
1514
import scala.util.Try

0 commit comments

Comments
 (0)