Skip to content
Snippets Groups Projects
Unverified Commit 265ed45e authored by SimonGuilloud's avatar SimonGuilloud Committed by GitHub
Browse files

Types (#166) 

* 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

* Removed unused option in build.sbt, run scalafixAll and scalafmtAll on lisa-examples, add a newline in build.properties
parent c3bd76a6
Branches
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2122 additions and 858 deletions
.gitignore
+ 5
− 0
View file @ 265ed45e
...@@ -11,3 +11,8 @@ target ...@@ -11,3 +11,8 @@ target
*.scala.semanticdb *.scala.semanticdb
*.iml *.iml
# silex and scallion
silex/*
scallion/*
build.sbt
+ 14
− 5
View file @ 265ed45e
...@@ -17,6 +17,15 @@ inThisBuild( ...@@ -17,6 +17,15 @@ inThisBuild(
) )
) )
val commonSettings = Seq(
version := "0.9",
crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
organization := "ch.epfl.lara",
scalacOptions ++= Seq("-Ximport-suggestion-timeout", "0")
)
val scala2 = "2.13.8" val scala2 = "2.13.8"
val scala3 = "3.2.2" val scala3 = "3.2.2"
...@@ -49,9 +58,9 @@ lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.gi ...@@ -49,9 +58,9 @@ lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.gi
lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18") lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
lazy val root = Project( lazy val root = Project(
id = "lisa", id = "lisa",
base = file(".") base = file(".")
) )
.settings(commonSettings3) .settings(commonSettings3)
.settings( .settings(
version := "0.1" version := "0.1"
...@@ -86,6 +95,6 @@ lazy val examples = Project( ...@@ -86,6 +95,6 @@ lazy val examples = Project(
id = "lisa-examples", id = "lisa-examples",
base = file("lisa-examples") base = file("lisa-examples")
) )
.settings(commonSettings)
.settings(commonSettings3) .settings(commonSettings3)
.dependsOn(root) .dependsOn(root)
\ No newline at end of file
lisa-examples/src/main/scala/Example.scala
+ 88
− 114
View file @ 265ed45e
import lisa.automation.kernel.OLPropositionalSolver.* import lisa.automation.kernel.OLPropositionalSolver.*
import lisa.kernel.fol.FOL.* import lisa.prooflib.Substitution.{ApplyRules as Substitute}
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.*
import lisa.mathematics.settheory.SetTheory.*
import lisa.prooflib.BasicStepTactic.*
import lisa.prooflib.ProofTacticLib.*
import lisa.prooflib.Substitution
import lisa.prooflib.Substitution.ApplyRules
import lisa.utils.FOLPrinter.*
import lisa.utils.KernelHelpers.checkProof
import lisa.utils.unification.UnificationUtils.*
/**
* Discover some of the elements of LISA to get started.
*/
object Example {
import lisa.kernel.proof.SequentCalculus.*
def main(args: Array[String]): Unit = {
val phi = formulaVariable()
val psi = formulaVariable()
val PierceLaw = SCProof(
Hypothesis(phi |- phi, phi),
Weakening(phi |- (phi, psi), 0),
RightImplies(() |- (phi, phi ==> psi), 1, phi, psi),
LeftImplies((phi ==> psi) ==> phi |- phi, 2, 0, (phi ==> psi), phi),
RightImplies(() |- ((phi ==> psi) ==> phi) ==> phi, 3, (phi ==> psi) ==> phi, phi)
)
val PierceLaw2 = SCProof(
RestateTrue(() |- ((phi ==> psi) ==> phi) ==> phi)
)
checkProof(PierceLaw)
checkProof(PierceLaw2)
val theory = new RunningTheory
val pierceThm: theory.Theorem = theory.makeTheorem("Pierce's Law", () |- ((phi ==> psi) ==> phi) ==> phi, PierceLaw, Seq.empty).get
}
}
object ExampleDSL extends lisa.Main { object Example extends lisa.Main {
// Simple Theorem with LISA's DSL
val x = variable val x = variable
val P = predicate(1) val y = variable
val f = function(1) val P = predicate[1]
val f = function[1]
// Simple proof with LISA's DSL
val fixedPointDoubleApplication = Theorem(∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))) { val fixedPointDoubleApplication = Theorem(∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))) {
assume(∀(x, P(x) ==> P(f(x)))) assume(∀(x, P(x) ==> P(f(x))))
assume(P(x)) assume(P(x))
...@@ -55,32 +16,52 @@ object ExampleDSL extends lisa.Main { ...@@ -55,32 +16,52 @@ object ExampleDSL extends lisa.Main {
val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
have(thesis) by Tautology.from(step1, step2) have(thesis) by Tautology.from(step1, step2)
} }
show
// More complicated example of a proof with LISA DSL // Example of set theoretic development
val y = variable
val z = variable /**
val unionOfSingleton = Theorem(union(singleton(x)) === x) { * Theorem --- The empty set is a subset of every set.
val X = singleton(x) *
val forward = have(in(z, x) ==> in(z, union(X))) subproof { * `|- ∅ ⊆ x`
have(in(z, x) |- in(z, x) /\ in(x, X)) by Tautology.from(pairAxiom of (y -> x, z -> x)) */
val step2 = thenHave(in(z, x) |- ∃(y, in(z, y) /\ in(y, X))) by RightExists val emptySetIsASubset = Theorem(
have(thesis) by Tautology.from(step2, unionAxiom of (x -> X)) ∅ ⊆ x
} ) {
have((y ∈ ∅) ==> (y ∈ x)) by Weakening(emptySetAxiom of (x := y))
val backward = have(in(z, union(X)) ==> in(z, x)) subproof { val rhs = thenHave(∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
have(in(z, y) |- in(z, y)) by Restate have(thesis) by Tautology.from(subsetAxiom of (x := ∅, y := x), rhs)
val step2 = thenHave((y === x, in(z, y)) |- in(z, x)) by ApplyRules(y === x)
have(in(z, y) /\ in(y, X) |- in(z, x)) by Tautology.from(pairAxiom of (y -> x, z -> y), step2)
val step4 = thenHave(∃(y, in(z, y) /\ in(y, X)) |- in(z, x)) by LeftExists
have(in(z, union(X)) ==> in(z, x)) by Tautology.from(unionAxiom of (x -> X), step4)
}
have(in(z, union(X)) <=> in(z, x)) by RightIff(forward, backward)
thenHave(forall(z, in(z, union(X)) <=> in(z, x))) by RightForall
andThen(Substitution.applySubst(extensionalityAxiom of (x -> union(X), y -> x)))
} }
show
/**
* Theorem --- If a set has an element, then it is not the empty set.
*
* `y ∈ x ⊢ ! x = ∅`
*/
val setWithElementNonEmpty = Theorem(
(y ∈ x) |- x =/= ∅
) {
have((x === ∅) |- !(y ∈ x)) by Substitute(x === ∅)(emptySetAxiom of (x := y))
}
/**
* Theorem --- A power set is never empty.
*
* `|- !powerAxiom(x) = ∅`
*/
val powerSetNonEmpty = Theorem(
powerSet(x) =/= ∅
) {
have(thesis) by Tautology.from(
setWithElementNonEmpty of (y := ∅, x := powerSet(x)),
powerAxiom of (x := ∅, y := x),
emptySetIsASubset
)
}
/*
import lisa.mathematics.settheory.SetTheory.*
// Examples of definitions // Examples of definitions
val succ = DEF(x) --> union(unorderedPair(x, singleton(x))) val succ = DEF(x) --> union(unorderedPair(x, singleton(x)))
...@@ -89,53 +70,46 @@ object ExampleDSL extends lisa.Main { ...@@ -89,53 +70,46 @@ object ExampleDSL extends lisa.Main {
val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x)) val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x))
show show
val defineNonEmptySet = Lemma(∃!(x, !(x === ∅) /\ (x === unorderedPair(∅, ∅)))) {
val subst = have(False <=> in(∅, ∅)) by Rewrite(emptySetAxiom of (x -> ∅()))
have(in(∅, unorderedPair(∅, ∅)) <=> False |- ()) by Rewrite(pairAxiom of (x -> ∅(), y -> ∅(), z -> ∅()))
andThen(Substitution.applySubst(subst))
thenHave(∀(z, in(z, unorderedPair(∅, ∅)) <=> in(z, ∅)) |- ()) by LeftForall
andThen(Substitution.applySubst(extensionalityAxiom of (x -> unorderedPair(∅(), ∅()), y -> ∅())))
andThen(Substitution.applySubst(x === unorderedPair(∅(), ∅())))
thenHave((!(x === ∅) /\ (x === unorderedPair(∅, ∅))) <=> (x === unorderedPair(∅, ∅))) by Tautology
thenHave(∀(x, (x === unorderedPair(∅, ∅)) <=> (!(x === ∅) /\ (x === unorderedPair(∅, ∅))))) by RightForall
thenHave(∃(y, ∀(x, (x === y) <=> (!(x === ∅) /\ (x === unorderedPair(∅, ∅)))))) by RightExists
}
show
// This definition is underspecified
val nonEmpty = DEF() --> The(x, !(x === ∅))(defineNonEmptySet)
show
// Simple tactic definition for LISA DSL
import lisa.automation.kernel.OLPropositionalSolver.*
// object SimpleTautology extends ProofTactic {
// def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
// val redF = reducedForm(f)
// if (redF == ⊤) {
// Restate(decisionsPos |- f :: decisionsNeg)
// } else if (redF == ⊥) {
// proof.InvalidProofTactic("Sequent is not a propositional tautology")
// } else {
// val atom = findBestAtom(redF).get
// def substInRedF(f: Formula) = redF.substituted(atom -> f)
// TacticSubproof {
// have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
// val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
// have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
// val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
// have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
// thenHave(decisionsPos |- f :: decisionsNeg) by Restate
// }
// }
// }
// def solveSequent(using proof: library.Proof)(bot: Sequent) =
// TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
// have(solveFormula(sequentToFormula(bot), Nil, Nil))
// thenHave(bot) by Restate.from
// }
// }
*/
/*
// Simple tactic definition for LISA DSL
import lisa.automation.kernel.OLPropositionalSolver.*
// object SimpleTautology extends ProofTactic {
// def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
// val redF = reducedForm(f)
// if (redF == ⊤) {
// Restate(decisionsPos |- f :: decisionsNeg)
// } else if (redF == ⊥) {
// proof.InvalidProofTactic("Sequent is not a propositional tautology")
// } else {
// val atom = findBestAtom(redF).get
// def substInRedF(f: Formula) = redF.substituted(atom -> f)
// TacticSubproof {
// have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
// val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
// have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
// val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
// have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
// thenHave(decisionsPos |- f :: decisionsNeg) by Restate
// }
// }
// }
// def solveSequent(using proof: library.Proof)(bot: Sequent) =
// TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
// have(solveFormula(sequentToFormula(bot), Nil, Nil))
// thenHave(bot) by Restate.from
// }
// }
*/
// val a = formulaVariable() // val a = formulaVariable()
// val b = formulaVariable() // val b = formulaVariable()
// val c = formulaVariable() // val c = formulaVariable()
......
lisa-examples/src/main/scala/ExampleKernel.scala 0 → 100644
+ 33
− 0
View file @ 265ed45e
import lisa.utils.K
import K.*
/**
* Discover some of the elements of the logical kernel of LISA.
*/
object ExampleKernel {
import lisa.kernel.proof.SequentCalculus.*
def main(args: Array[String]): Unit = {
val phi = formulaVariable()
val psi = formulaVariable()
val PierceLaw = SCProof(
Hypothesis(phi |- phi, phi),
Weakening(phi |- (phi, psi), 0),
RightImplies(() |- (phi, phi ==> psi), 1, phi, psi),
LeftImplies((phi ==> psi) ==> phi |- phi, 2, 0, (phi ==> psi), phi),
RightImplies(() |- ((phi ==> psi) ==> phi) ==> phi, 3, (phi ==> psi) ==> phi, phi)
)
val PierceLaw2 = SCProof(
RestateTrue(() |- ((phi ==> psi) ==> phi) ==> phi)
)
checkProof(PierceLaw, println)
checkProof(PierceLaw2, println)
val theory = new RunningTheory
val pierceThm: theory.Theorem = theory.makeTheorem("Pierce's Law", () |- ((phi ==> psi) ==> phi) ==> phi, PierceLaw, Seq.empty).get
}
}
lisa-examples/src/main/scala/MapProofDef.scala 0 → 100644
+ 106
− 0
View file @ 265ed45e
import lisa.automation.kernel.OLPropositionalSolver.*
import lisa.automation.kernel.SimpleSimplifier.*
import lisa.prooflib.BasicStepTactic.*
import lisa.prooflib.ProofTacticLib.*
import lisa.utils.FOLPrinter.*
import lisa.utils.KernelHelpers.checkProof
import lisa.utils.parsing.FOLPrinter
import lisa.utils.unification.UnificationUtils.*
object MapProofDef extends lisa.Main {
/*
val self = this
val x = variable
val y = variable
val xs = variable
val ys = variable
val f = variable
val Nil = ConstantFunctionLabel("Nil", 0)()
theory.addSymbol(ConstantFunctionLabel("Nil", 0))
val Cons = ConstantFunctionLabel("Cons", 2)
theory.addSymbol(Cons)
class TermProxy(t1:Term) {
infix def ::(t2: Term) = Cons(t2, t1)
infix def +++(t2: Term) = append(t1, t2)
def map(t2: Term) = self.map(t1, t2)
def mapTr(t2: Term, t3: Term) = self.mapTr(t1, t2, t3)
}
given Conversion[Term, TermProxy] = TermProxy(_)
given Conversion[VariableLabel, TermProxy] = v => TermProxy(v())
object append {
val append_ = ConstantFunctionLabel("append", 2)
theory.addSymbol(append_)
val NilCase = theory.addAxiom("append.NilCase", (Nil +++ xs) === xs).get
val ConsCase = theory.addAxiom("append.ConsCase", ((x :: xs) +++ ys) === Cons(x, append(xs, ys))).get
def apply(t1: Term, t2: Term) = append_(t1, t2)
}
object map {
val map = ConstantFunctionLabel("map", 2)
theory.addSymbol(map)
val NilCase = theory.addAxiom("map.NilCase", Nil.map(f) === Nil).get
val ConsCase = theory.addAxiom("map.ConsCase", (x :: xs).map(f) === (app(f, x) :: xs.map(f))).get
def apply(t1: Term, t2: Term) = map(t1, t2)
}
object mapTr {
val mapTr = ConstantFunctionLabel("mapTr", 3)
theory.addSymbol(mapTr)
val NilCase = theory.addAxiom("mapTr.NilCase", Nil.mapTr(f, xs) === xs).get
val ConsCase = theory.addAxiom("mapTr.ConsCase", (x :: xs).mapTr(f, ys) === xs.mapTr(f, ys +++ (app(f, x) :: Nil))).get
def apply(t1: Term, t2: Term, t3: Term) = mapTr(t1, t2, t3)
}
// some more DSL
val mapRules = Seq(
map.NilCase,
map.ConsCase,
mapTr.NilCase,
mapTr.ConsCase,
append.NilCase,
append.ConsCase
)
object Auto extends ProofTactic {
def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)
(args: proof.Fact | RunningTheory#Justification)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
val tac: proof.ProofTacticJudgement = Substitution.apply2(false, args)(premise)(bot)
tac match {
case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
case proof.InvalidProofTactic(m1) =>
val tac: proof.ProofTacticJudgement = Substitution.apply2(true, args)(premise)(bot)
tac match {
case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
case proof.InvalidProofTactic(m2) =>
val tac: proof.ProofTacticJudgement = Tautology.from(args.asInstanceOf, premise)(bot)
tac match {
case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
case proof.InvalidProofTactic(m3) => proof.InvalidProofTactic("Decomposition of Auto failure:\n" + m1 + "\n" + m2 + "\n" + m3)
}
}
}
}
def a(using lib: lisa.prooflib.Library, proof: lib.Proof)
(args: proof.Fact | RunningTheory#Justification)(bot: Sequent): proof.ProofTacticJudgement = {
val tac: proof.ProofTacticJudgement = Tautology.from(args.asInstanceOf)(bot)
tac match {
case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
case proof.InvalidProofTactic(m3) => proof.InvalidProofTactic("Decomposition of Auto failure:\n" + m3)
}
}
}
*/
}
lisa-examples/src/main/scala/MapProofTest.scala
+ 25
− 27
View file @ 265ed45e
import MapProofDef.{_, given}
import lisa.automation.kernel.OLPropositionalSolver.* import lisa.automation.kernel.OLPropositionalSolver.*
import lisa.kernel.fol.FOL.* import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory import lisa.kernel.proof.RunningTheory
...@@ -49,7 +50,7 @@ object MapProofTest extends lisa.Main { ...@@ -49,7 +50,7 @@ object MapProofTest extends lisa.Main {
val ConsAppend = forall(x, forall(xs, forall(ys, ((x :: xs) ++ ys) === (x :: (xs ++ ys))))) val ConsAppend = forall(x, forall(xs, forall(ys, ((x :: xs) ++ ys) === (x :: (xs ++ ys)))))
val AccOutNil = Theorem( val AccOutNil = Theorem(
MapTrNil |- Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs)) Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs))
) { ) {
assume(MapTrNil) assume(MapTrNil)
...@@ -60,16 +61,15 @@ object MapProofTest extends lisa.Main { ...@@ -60,16 +61,15 @@ object MapProofTest extends lisa.Main {
thenHave(Nil.mapTr(f, xs) === xs |- Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs))) by ApplyRules(Nil.mapTr(f, xs) === xs) thenHave(Nil.mapTr(f, xs) === xs |- Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs))) by ApplyRules(Nil.mapTr(f, xs) === xs)
thenHave(thesis) by LeftForall thenHave(thesis) by LeftForall
} }
show
// induction hypothesis // induction hypothesis
val IH1 = forall(y, forall(ys, xs.mapTr(f, y :: ys) === (y :: xs.mapTr(f, ys)))) val IH1 = forall(y, forall(ys, xs.mapTr(f, y :: ys) === (y :: xs.mapTr(f, ys))))
val AccOutCons = Theorem( val AccOutCons = Theorem(
(MapTrCons, ConsAppend, IH1) |- (x :: xs).mapTr(f, y :: ys) === (y :: (x :: xs).mapTr(f, ys)) IH1 |- (x :: xs).mapTr(f, y :: ys) === (y :: (x :: xs).mapTr(f, ys))
) { ) {
assume(MapTrCons)
assume(ConsAppend) assume(mapRules)
assume(IH1) assume(IH1)
// apply MapTrCons // apply MapTrCons
...@@ -84,23 +84,22 @@ object MapProofTest extends lisa.Main { ...@@ -84,23 +84,22 @@ object MapProofTest extends lisa.Main {
// apply IH1 // apply IH1
have(IH1) by Restate have(IH1) by Restate
thenHave(xs.mapTr(f, (y :: (ys ++ (app(f, x) :: Nil)))) === (y :: xs.mapTr(f, (ys ++ (app(f, x) :: Nil))))) by InstantiateForall(y, (ys ++ (app(f, x) :: Nil))) thenHave(xs.mapTr(f, (y :: (ys +++ (app(f, x) :: Nil)))) === (y :: xs.mapTr(f, (ys +++ (app(f, x) :: Nil))))) by InstantiateForall(y, (ys +++ (app(f, x) :: Nil)))
val consYXs = have((x :: xs).mapTr(f, (y :: ys)) === (y :: xs.mapTr(f, (ys ++ (app(f, x) :: Nil))))) by ApplyRules(lastStep)(consYYs) val consYXs = have((x :: xs).mapTr(f, (y :: ys)) === (y :: xs.mapTr(f, (ys ++ (app(f, x) :: Nil))))) by ApplyRules(lastStep)(consYYs)
// apply MapTrCons again // apply mapTr.ConsCase again
have(MapTrCons) by Restate have(mapTr.ConsCase) by Restate
thenHave((x :: xs).mapTr(f, ys) === xs.mapTr(f, (ys ++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, ys) thenHave((x :: xs).mapTr(f, ys) === xs.mapTr(f, (ys +++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, ys)
have(thesis) by ApplyRules(lastStep)(consYXs) have(thesis) by ApplyRules(lastStep)(consYXs)
} }
show show
val MapEqMapTrNil = Theorem( val MapEqMapTrNil = Theorem(
(MapNil, MapTrNil) |- Nil.map(f) === Nil.mapTr(f, Nil) mapRules |- Nil.map(f) === Nil.mapTr(f, Nil)
) { ) {
assume(MapNil) assume(mapRules)
assume(MapTrNil)
// apply MapTrNil // apply MapTrNil
val trNil = have(Nil.mapTr(f, Nil) === Nil) by InstantiateForall val trNil = have(Nil.mapTr(f, Nil) === Nil) by InstantiateForall
...@@ -111,30 +110,29 @@ object MapProofTest extends lisa.Main { ...@@ -111,30 +110,29 @@ object MapProofTest extends lisa.Main {
} }
show show
// the result of induction on the cases above
val AccOut = forall(xs, IH1)
// second induction hypothesis // second induction hypothesis
val IH2 = xs.map(f) === xs.mapTr(f, Nil) val IH2 = xs.map(f) === xs.mapTr(f, Nil)
val MapEqMapTrCons = Theorem( val MapEqMapCons = Theorem(
(MapCons, IH2, NilAppend, MapTrCons, ConsAppend, IH1) |- (x :: xs).map(f) === (x :: xs).mapTr(f, Nil) (mapRules :+ IH2 :+ AccOut) |- (x :: xs).map(f) === (x :: xs).mapTr(f, Nil)
) { ) {
assume(MapCons) assume(mapRules)
assume(IH2) assume(IH2)
assume(NilAppend) assume(AccOut)
assume(MapTrCons)
// assumptions from last proof
assume(ConsAppend)
assume(IH1)
// apply MapCons // apply map.ConsCase
have(MapCons) by Restate have(map.ConsCase)
val mCons = thenHave((x :: xs).map(f) === (app(f, x) :: xs.map(f))) by InstantiateForall(x, xs) val mCons = thenHave((x :: xs).map(f) === (app(f, x) :: xs.map(f))) by InstantiateForall(x, xs)
// apply IH2 // apply IH2
have(IH2) by Restate have(IH2) by Restate
val consTr = have((x :: xs).map(f) === (app(f, x) :: xs.mapTr(f, Nil))) by ApplyRules(lastStep)(mCons) val consTr = have((x :: xs).map(f) === (app(f, x) :: xs.mapTr(f, Nil))) by ApplyRules(lastStep)(mCons)
// apply AccOut TODO: expand this to be inductive // apply AccOut
have(IH1) by Restate have(IH1) by InstantiateForall
thenHave(xs.mapTr(f, (app(f, x) :: Nil)) === (app(f, x) :: xs.mapTr(f, Nil))) by InstantiateForall(app(f, x), Nil) thenHave(xs.mapTr(f, (app(f, x) :: Nil)) === (app(f, x) :: xs.mapTr(f, Nil))) by InstantiateForall(app(f, x), Nil)
val trCons = have((x :: xs).map(f) === xs.mapTr(f, (app(f, x) :: Nil))) by ApplyRules(lastStep)(consTr) val trCons = have((x :: xs).map(f) === xs.mapTr(f, (app(f, x) :: Nil))) by ApplyRules(lastStep)(consTr)
...@@ -142,9 +140,9 @@ object MapProofTest extends lisa.Main { ...@@ -142,9 +140,9 @@ object MapProofTest extends lisa.Main {
have((Nil ++ (app(f, x) :: Nil)) === (app(f, x) :: Nil)) by InstantiateForall have((Nil ++ (app(f, x) :: Nil)) === (app(f, x) :: Nil)) by InstantiateForall
val trApp = have((x :: xs).map(f) === xs.mapTr(f, (Nil ++ (app(f, x) :: Nil)))) by ApplyRules(lastStep)(trCons) val trApp = have((x :: xs).map(f) === xs.mapTr(f, (Nil ++ (app(f, x) :: Nil)))) by ApplyRules(lastStep)(trCons)
// apply MapTrCons // apply mapTr.ConsCase
have(MapTrCons) by Restate have(mapTr.ConsCase)
thenHave((x :: xs).mapTr(f, Nil) === xs.mapTr(f, (Nil ++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, Nil) thenHave((x :: xs).mapTr(f, Nil) === xs.mapTr(f, (Nil +++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, Nil)
have(thesis) by ApplyRules(lastStep)(trApp) have(thesis) by ApplyRules(lastStep)(trApp)
} }
......
lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+ 1
− 1
View file @ 265ed45e
...@@ -9,7 +9,7 @@ private[fol] trait CommonDefinitions { ...@@ -9,7 +9,7 @@ private[fol] trait CommonDefinitions {
/** /**
* A labelled node for tree-like structures. * A labelled node for tree-like structures.
*/ */
protected trait Label { trait Label {
val arity: Int val arity: Int
val id: Identifier val id: Identifier
} }
......
lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+ 0
− 8
View file @ 265ed45e
...@@ -135,12 +135,4 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD ...@@ -135,12 +135,4 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
override def schematicConnectorLabels: Set[SchematicConnectorLabel] = inner.schematicConnectorLabels override def schematicConnectorLabels: Set[SchematicConnectorLabel] = inner.schematicConnectorLabels
override def freeVariableFormulaLabels: Set[VariableFormulaLabel] = inner.freeVariableFormulaLabels override def freeVariableFormulaLabels: Set[VariableFormulaLabel] = inner.freeVariableFormulaLabels
} }
/**
* Binds multiple variables at the same time
*/
@deprecated
def bindAll(binder: BinderLabel, vars: Seq[VariableLabel], phi: Formula): Formula =
vars.foldLeft(phi)((f, v) => BinderFormula(binder, v, f))
} }
lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+ 19
− 19
View file @ 265ed45e
...@@ -10,7 +10,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -10,7 +10,7 @@ trait Substitutions extends FormulaDefinitions {
* @param body The term represented by the object, up to instantiation of the bound schematic variables in args. * @param body The term represented by the object, up to instantiation of the bound schematic variables in args.
*/ */
case class LambdaTermTerm(vars: Seq[VariableLabel], body: Term) { case class LambdaTermTerm(vars: Seq[VariableLabel], body: Term) {
def apply(args: Seq[Term]): Term = substituteVariables(body, (vars zip args).toMap) def apply(args: Seq[Term]): Term = substituteVariablesInTerm(body, (vars zip args).toMap)
} }
/** /**
...@@ -22,7 +22,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -22,7 +22,7 @@ trait Substitutions extends FormulaDefinitions {
*/ */
case class LambdaTermFormula(vars: Seq[VariableLabel], body: Formula) { case class LambdaTermFormula(vars: Seq[VariableLabel], body: Formula) {
def apply(args: Seq[Term]): Formula = { def apply(args: Seq[Term]): Formula = {
substituteVariables(body, (vars zip args).toMap) substituteVariablesInFormula(body, (vars zip args).toMap)
} }
} }
...@@ -50,9 +50,9 @@ trait Substitutions extends FormulaDefinitions { ...@@ -50,9 +50,9 @@ trait Substitutions extends FormulaDefinitions {
* @param m A map from variables to terms. * @param m A map from variables to terms.
* @return t[m] * @return t[m]
*/ */
def substituteVariables(t: Term, m: Map[VariableLabel, Term]): Term = t match { def substituteVariablesInTerm(t: Term, m: Map[VariableLabel, Term]): Term = t match {
case Term(label: VariableLabel, _) => m.getOrElse(label, t) case Term(label: VariableLabel, _) => m.getOrElse(label, t)
case Term(label, args) => Term(label, args.map(substituteVariables(_, m))) case Term(label, args) => Term(label, args.map(substituteVariablesInTerm(_, m)))
} }
/** /**
...@@ -62,12 +62,12 @@ trait Substitutions extends FormulaDefinitions { ...@@ -62,12 +62,12 @@ trait Substitutions extends FormulaDefinitions {
* @param m The map from schematic function symbols to lambda expressions Term(s) -> Term [[LambdaTermTerm]]. * @param m The map from schematic function symbols to lambda expressions Term(s) -> Term [[LambdaTermTerm]].
* @return t[m] * @return t[m]
*/ */
def instantiateTermSchemas(t: Term, m: Map[SchematicTermLabel, LambdaTermTerm]): Term = { def instantiateTermSchemasInTerm(t: Term, m: Map[SchematicTermLabel, LambdaTermTerm]): Term = {
require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity }) require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
t match { t match {
case Term(label: VariableLabel, _) => m.get(label).map(_.apply(Nil)).getOrElse(t) case Term(label: VariableLabel, _) => m.get(label).map(_.apply(Nil)).getOrElse(t)
case Term(label, args) => case Term(label, args) =>
val newArgs = args.map(instantiateTermSchemas(_, m)) val newArgs = args.map(instantiateTermSchemasInTerm(_, m))
label match { label match {
case label: ConstantFunctionLabel => Term(label, newArgs) case label: ConstantFunctionLabel => Term(label, newArgs)
case label: SchematicTermLabel => case label: SchematicTermLabel =>
...@@ -87,18 +87,18 @@ trait Substitutions extends FormulaDefinitions { ...@@ -87,18 +87,18 @@ trait Substitutions extends FormulaDefinitions {
* @param m A map from variables to terms * @param m A map from variables to terms
* @return t[m] * @return t[m]
*/ */
def substituteVariables(phi: Formula, m: Map[VariableLabel, Term], takenIds: Seq[Identifier] = Seq[Identifier]()): Formula = phi match { def substituteVariablesInFormula(phi: Formula, m: Map[VariableLabel, Term], takenIds: Seq[Identifier] = Seq[Identifier]()): Formula = phi match {
case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariables(_, m))) case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariablesInTerm(_, m)))
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariables(_, m))) case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariablesInFormula(_, m)))
case BinderFormula(label, bound, inner) => case BinderFormula(label, bound, inner) =>
val newSubst = m - bound val newSubst = m - bound
val newTaken = takenIds :+ bound.id val newTaken = takenIds :+ bound.id
val fv = m.values.flatMap(_.freeVariables).toSet val fv = m.values.flatMap(_.freeVariables).toSet
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id) ++ newTaken, bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id) ++ newTaken, bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)), newTaken) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)), newTaken)
BinderFormula(label, newBoundVariable, substituteVariables(newInner, newSubst, newTaken)) BinderFormula(label, newBoundVariable, substituteVariablesInFormula(newInner, newSubst, newTaken))
} else BinderFormula(label, bound, substituteVariables(inner, newSubst, newTaken)) } else BinderFormula(label, bound, substituteVariablesInFormula(inner, newSubst, newTaken))
} }
/** /**
...@@ -117,7 +117,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -117,7 +117,7 @@ trait Substitutions extends FormulaDefinitions {
val newTaken = takenIds :+ bound.id val newTaken = takenIds :+ bound.id
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ newTaken, bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ newTaken, bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)), newTaken) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)), newTaken)
BinderFormula(label, newBoundVariable, substituteFormulaVariables(newInner, m, newTaken)) BinderFormula(label, newBoundVariable, substituteFormulaVariables(newInner, m, newTaken))
} else BinderFormula(label, bound, substituteFormulaVariables(inner, m, newTaken)) } else BinderFormula(label, bound, substituteFormulaVariables(inner, m, newTaken))
} }
...@@ -132,14 +132,14 @@ trait Substitutions extends FormulaDefinitions { ...@@ -132,14 +132,14 @@ trait Substitutions extends FormulaDefinitions {
def instantiateTermSchemas(phi: Formula, m: Map[SchematicTermLabel, LambdaTermTerm]): Formula = { def instantiateTermSchemas(phi: Formula, m: Map[SchematicTermLabel, LambdaTermTerm]): Formula = {
require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity }) require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
phi match { phi match {
case PredicateFormula(label, args) => PredicateFormula(label, args.map(a => instantiateTermSchemas(a, m))) case PredicateFormula(label, args) => PredicateFormula(label, args.map(a => instantiateTermSchemasInTerm(a, m)))
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateTermSchemas(_, m))) case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateTermSchemas(_, m)))
case BinderFormula(label, bound, inner) => case BinderFormula(label, bound, inner) =>
val newSubst = m - bound val newSubst = m - bound
val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable))) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiateTermSchemas(newInner, newSubst)) BinderFormula(label, newBoundVariable, instantiateTermSchemas(newInner, newSubst))
} else BinderFormula(label, bound, instantiateTermSchemas(inner, newSubst)) } else BinderFormula(label, bound, instantiateTermSchemas(inner, newSubst))
} }
...@@ -165,7 +165,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -165,7 +165,7 @@ trait Substitutions extends FormulaDefinitions {
val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable))) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiatePredicateSchemas(newInner, m)) BinderFormula(label, newBoundVariable, instantiatePredicateSchemas(newInner, m))
} else BinderFormula(label, bound, instantiatePredicateSchemas(inner, m)) } else BinderFormula(label, bound, instantiatePredicateSchemas(inner, m))
} }
...@@ -192,7 +192,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -192,7 +192,7 @@ trait Substitutions extends FormulaDefinitions {
val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaFormulaFormula(arguments, body)) => body.freeVariables }).toSet val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaFormulaFormula(arguments, body)) => body.freeVariables }).toSet
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable))) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiateConnectorSchemas(newInner, m)) BinderFormula(label, newBoundVariable, instantiateConnectorSchemas(newInner, m))
} else BinderFormula(label, bound, instantiateConnectorSchemas(inner, m)) } else BinderFormula(label, bound, instantiateConnectorSchemas(inner, m))
} }
...@@ -216,7 +216,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -216,7 +216,7 @@ trait Substitutions extends FormulaDefinitions {
require(mTerm.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity }) require(mTerm.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
phi match { phi match {
case PredicateFormula(label, args) => case PredicateFormula(label, args) =>
val newArgs = args.map(a => instantiateTermSchemas(a, mTerm)) val newArgs = args.map(a => instantiateTermSchemasInTerm(a, mTerm))
label match { label match {
case label: SchematicVarOrPredLabel if mPred.contains(label) => mPred(label)(newArgs) case label: SchematicVarOrPredLabel if mPred.contains(label) => mPred(label)(newArgs)
case _ => PredicateFormula(label, newArgs) case _ => PredicateFormula(label, newArgs)
...@@ -235,7 +235,7 @@ trait Substitutions extends FormulaDefinitions { ...@@ -235,7 +235,7 @@ trait Substitutions extends FormulaDefinitions {
(mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet (mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet
if (fv.contains(bound)) { if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ mTerm.keys.map(_.id), bound.name)) val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ mTerm.keys.map(_.id), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable))) val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiateSchemas(newInner, mCon, mPred, newmTerm)) BinderFormula(label, newBoundVariable, instantiateSchemas(newInner, mCon, mPred, newmTerm))
} else BinderFormula(label, bound, instantiateSchemas(inner, mCon, mPred, newmTerm)) } else BinderFormula(label, bound, instantiateSchemas(inner, mCon, mPred, newmTerm))
} }
......
lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+ 2
− 2
View file @ 265ed45e
...@@ -150,7 +150,7 @@ object SCProofChecker { ...@@ -150,7 +150,7 @@ object SCProofChecker {
*/ */
case LeftForall(b, t1, phi, x, t) => case LeftForall(b, t1, phi, x, t) =>
if (isSameSet(b.right, ref(t1).right)) if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + substituteVariables(phi, Map(x -> t)), ref(t1).left + BinderFormula(Forall, x, phi))) if (isSameSet(b.left + substituteVariablesInFormula(phi, Map(x -> t)), ref(t1).left + BinderFormula(Forall, x, phi)))
SCValidProof(SCProof(step)) SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ") else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise") else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
...@@ -270,7 +270,7 @@ object SCProofChecker { ...@@ -270,7 +270,7 @@ object SCProofChecker {
*/ */
case RightExists(b, t1, phi, x, t) => case RightExists(b, t1, phi, x, t) =>
if (isSameSet(b.left, ref(t1).left)) if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + substituteVariables(phi, Map(x -> t)), ref(t1).right + BinderFormula(Exists, x, phi))) if (isSameSet(b.right + substituteVariablesInFormula(phi, Map(x -> t)), ref(t1).right + BinderFormula(Exists, x, phi)))
SCValidProof(SCProof(step)) SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ") else SCInvalidProof(SCProof(step), Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
else SCInvalidProof(SCProof(step), Nil, "Left-hand sides or conclusion and premise must be the same.") else SCInvalidProof(SCProof(step), Nil, "Left-hand sides or conclusion and premise must be the same.")
......
lisa-utils/src/main/scala/lisa/fol/Common.scala 0 → 100644
+ 762
− 0
View file @ 265ed45e
This diff is collapsed.
lisa-utils/src/main/scala/lisa/fol/FOL.scala 0 → 100644
+ 6
− 0
View file @ 265ed45e
package lisa.fol
object FOL extends Common with Sequents with Lambdas with Predef {
export FOLHelpers.{*, given}
}
lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala 0 → 100644
+ 136
− 0
View file @ 265ed45e
package lisa.fol
import lisa.fol.FOL.*
import lisa.kernel.fol.FOL.Identifier
import lisa.utils.FOLParser
import lisa.utils.K
import lisa.utils.LisaException
import scala.annotation.targetName
import scala.reflect.ClassTag
/**
* A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
* Usage:
* <pre>
* import utilities.Helpers.*
* </pre>
* or
* <pre>
* extends utilities.KernelHelpers.*
* </pre>
*/
object FOLHelpers {
export lisa.utils.KernelHelpers.{freshId, nFreshId, given_Conversion_String_Identifier, given_Conversion_Identifier_String, given_Conversion_Boolean_List_String_Option}
/////////////////
// FOL helpers //
/////////////////
/* Conversions */
// Conversions to lambdaExpression's
given [T <: LisaObject[T], R <: LisaObject[R]]: Conversion[R, LambdaExpression[T, R, 0]] = LambdaExpression[T, R, 0](Seq(), _, 0)
given [T <: LisaObject[T], R <: LisaObject[R]]: Conversion[(SchematicLabel[T], R), LambdaExpression[T, R, 1]] = a => LambdaExpression(Seq(a._1), a._2, 1)
given [T <: LisaObject[T], R <: LisaObject[R], N <: Arity]: Conversion[(SchematicLabel[T] ** N, R), LambdaExpression[T, R, N]] = a => {
val s = a._1.toSeq
LambdaExpression(s, a._2, s.length.asInstanceOf)
}
given [T <: LisaObject[T]]: Conversion[T, T *** 1] = _ *: EmptyTuple
given Conversion[Int, Arity] = _.asInstanceOf
/*
extension [I, O <: LisaObject[O]] (e: (I ** 0) |-> O) {
def apply() = e.apply(EmptyTuple)
}
*/
// helpers to create new schematic symbols, fetching the scala name of the variable.
def variable(using name: sourcecode.Name): Variable = Variable(name.value)
def function[N <: Arity: ValueOf](using name: sourcecode.Name): SchematicFunctionLabel[N] = SchematicFunctionLabel[N](name.value, valueOf[N])
def formulaVariable(using name: sourcecode.Name): VariableFormula = VariableFormula(name.value)
def predicate[N <: Arity: ValueOf](using name: sourcecode.Name): SchematicPredicateLabel[N] = SchematicPredicateLabel[N](name.value, valueOf[N])
def connector[N <: Arity: ValueOf](using name: sourcecode.Name): SchematicConnectorLabel[N] = SchematicConnectorLabel[N](name.value, valueOf[N])
////////////////////////////////////////
// Kernel to Front transformers //
////////////////////////////////////////
// TermLabel
def asFrontLabel(tl: K.TermLabel): TermLabel = tl match
case tl: K.ConstantFunctionLabel => asFrontLabel(tl)
case tl: K.SchematicTermLabel => asFrontLabel(tl)
def asFrontLabel[N <: Arity](cfl: K.ConstantFunctionLabel): ConstantFunctionLabelOfArity[N] = cfl.arity.asInstanceOf[N] match
case n: 0 => Constant(cfl.id)
case n: N => ConstantFunctionLabel[N](cfl.id, n)
def asFrontLabel(stl: K.SchematicTermLabel): SchematicTermLabel = stl match
case v: K.VariableLabel => asFrontLabel(stl)
case v: K.SchematicFunctionLabel => asFrontLabel(v)
def asFrontLabel[N <: Arity](sfl: K.SchematicFunctionLabel): SchematicFunctionLabel[N] =
SchematicFunctionLabel(sfl.id, sfl.arity.asInstanceOf)
def asFrontLabel(v: K.VariableLabel): Variable = Variable(v.id)
// Term
def asFront(t: K.Term): Term = asFrontLabel(t.label)(t.args.map(asFront))
// FormulaLabel
def asFrontLabel(fl: K.FormulaLabel): PredicateLabel | ConnectorLabel | BinderLabel = fl match
case fl: K.ConnectorLabel => asFrontLabel(fl)
case fl: K.PredicateLabel => asFrontLabel(fl)
case fl: K.BinderLabel => asFrontLabel(fl)
def asFrontLabel(pl: K.PredicateLabel): PredicateLabel = pl match
case pl: K.ConstantPredicateLabel => asFrontLabel(pl)
case pl: K.SchematicVarOrPredLabel => asFrontLabel(pl)
def asFrontLabel(cl: K.ConnectorLabel): ConnectorLabel = cl match
case cl: K.ConstantConnectorLabel => asFrontLabel(cl)
case cl: K.SchematicConnectorLabel => asFrontLabel(cl)
def asFrontLabel[N <: Arity](cpl: K.ConstantPredicateLabel): ConstantPredicateLabelOfArity[N] = cpl.arity.asInstanceOf[N] match
case n: 0 => ConstantFormula(cpl.id)
case n: N => ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
def asFrontLabel(sfl: K.SchematicFormulaLabel): SchematicVarOrPredLabel | SchematicConnectorLabel[?] =
sfl match
case v: K.VariableFormulaLabel => asFrontLabel(v)
case v: K.SchematicPredicateLabel => asFrontLabel(v)
case v: K.SchematicConnectorLabel => asFrontLabel(v)
def asFrontLabel(svop: K.SchematicVarOrPredLabel): SchematicVarOrPredLabel = svop match
case v: K.VariableFormulaLabel => asFrontLabel(v)
case v: K.SchematicPredicateLabel => asFrontLabel(v)
def asFrontLabel(v: K.VariableFormulaLabel): VariableFormula = VariableFormula(v.id)
def asFrontLabel[N <: Arity](spl: K.SchematicPredicateLabel): SchematicPredicateLabel[N] =
SchematicPredicateLabel(spl.id, spl.arity.asInstanceOf)
def asFrontLabel[N <: Arity](scl: K.SchematicConnectorLabel): SchematicConnectorLabel[N] =
SchematicConnectorLabel(scl.id, scl.arity.asInstanceOf)
def asFrontLabel(cpl: K.ConstantConnectorLabel): ConnectorLabel = cpl match
case K.Neg => Neg
case K.Implies => Implies
case K.Iff => Iff
case K.And => And
case K.Or => Or
def asFrontLabel(bl: K.BinderLabel): BaseBinderLabel = bl match {
case K.Forall => Forall
case K.Exists => Exists
case K.ExistsOne => ExistsOne
}
// Formula
def asFront(f: K.Formula): Formula = f match
case f: K.PredicateFormula => asFront(f)
case f: K.ConnectorFormula => asFront(f)
case f: K.BinderFormula => asFront(f)
def asFront(pf: K.PredicateFormula): Formula =
asFrontLabel(pf.label)(pf.args.map(asFront))
def asFront(cf: K.ConnectorFormula): Formula =
asFrontLabel(cf.label)(cf.args.map(asFront))
def asFront(bf: K.BinderFormula): BinderFormula =
asFrontLabel(bf.label)(asFrontLabel(bf.bound), asFront(bf.inner))
// Sequents
def asFront(s: K.Sequent): Sequent = Sequent(s.left.map(asFront), s.right.map(asFront))
// Lambdas
def asFrontLambda(l: K.LambdaTermTerm): LambdaExpression[Term, Term, ?] = LambdaExpression(l.vars.map(asFrontLabel), asFront(l.body), l.vars.size)
def asFrontLambda(l: K.LambdaTermFormula): LambdaExpression[Term, Formula, ?] = LambdaExpression(l.vars.map(asFrontLabel), asFront(l.body), l.vars.size)
def asFrontLambda(l: K.LambdaFormulaFormula): LambdaExpression[Formula, Formula, ?] = LambdaExpression(l.vars.map(asFrontLabel), asFront(l.body), l.vars.size)
}
lisa-utils/src/main/scala/lisa/fol/Lambdas.scala 0 → 100644
+ 100
− 0
View file @ 265ed45e
package lisa.fol
import lisa.kernel.fol.FOL.Identifier
import lisa.utils.K
import scala.reflect.ClassTag
import FOLHelpers.freshId
trait Lambdas extends Common {
/**
* Denotes a lambda expression, i.e. an expression with "holes".
* N is the number of arguments (-1 for arbitrary or unknown).
* T is the type of input of the lambda.
* R is the return type.
* For example, LambdaExpression[Term, Formula, 2] denotes an expression of type (Term**2 |-> Formula),
* i.e. an expression that can be substituted in place of a 2-variable predicate
*
* @param bounds The bound variable encoding the parameter of the lambda
* @param body The body of the lambda
* @param arity The number of parameters.
*/
case class LambdaExpression[T <: LisaObject[T], R <: LisaObject[R], N <: Arity](bounds: Seq[SchematicLabel[T]], body: R, arity: N) extends |->[T ** N, R] {
assert(arity == bounds.length)
private val seqBounds = bounds.toSeq
def apply(args: T ** N): R = body.substituteUnsafe((bounds zip args.toSeq).toMap)
def appUnsafe(args: Seq[T]): R = body.substituteUnsafe((bounds zip args.toSeq).toMap)
/**
* Substitute schematic symbols by values of corresponding type in the body of expressions. The variables of the expression are bound: This implies that
* 1. They are not substituted in the body even if they are in the substitution map, and
* 2. The bounds of the expression are renamed before substitution if they appear in the substitution.
*
* @param map
* @return
*/
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): LambdaExpression[T, R, N] = {
val newSubst = map -- seqBounds
val conflict = map.values.flatMap(_.freeSchematicLabels).toSet.intersect(bounds.asInstanceOf)
if (conflict.nonEmpty) {
val taken = (map.values.flatMap(_.allSchematicLabels).map(_.id) ++ map.keys.map(_.id)).toList
val newBounds = seqBounds.scanLeft[List[Identifier]](taken)((list, v: SchematicLabel[T]) => freshId(list, v.id) :: list).map(_.head).zip(seqBounds).map(v => v._2.rename(v._1))
val newBody = body.substituteUnsafe(seqBounds.zip(newBounds.map(_.liftLabel)).toMap)
LambdaExpression(newBounds, newBody.substituteUnsafe(newSubst), arity)
} else {
LambdaExpression(bounds, body.substituteUnsafe(newSubst), arity)
}
}
def freeSchematicLabels: Set[SchematicLabel[?]] = body.freeSchematicLabels -- seqBounds
def allSchematicLabels: Set[SchematicLabel[?]] = body.freeSchematicLabels
}
/**
* Construct a Lambda expression with a single variable
*/
def lambda[T <: LisaObject[T], R <: LisaObject[R]](bound: SchematicLabel[T], body: R): LambdaExpression[T, R, 1] = LambdaExpression[T, R, 1](Seq(bound), body, 1)
/**
* Construct a Lambda expression with multiple variables
*/
def lambda[T <: LisaObject[T], R <: LisaObject[R], N <: Arity, Tu <: Tuple](bounds: Tu, body: R)(using Tuple.Union[Tu] <:< SchematicLabel[T], Tuple.Size[Tu] =:= N): LambdaExpression[T, R, N] = {
val boundsSeq = bounds.asInstanceOf[SchematicLabel[T] *** N].toSeq
LambdaExpression[T, R, N](boundsSeq, body, boundsSeq.length.asInstanceOf)
}
def lambda[T <: LisaObject[T], R <: LisaObject[R]](bounds: Seq[SchematicLabel[T]], body: R): LambdaExpression[T, R, ?] = {
val boundsSeq = bounds.toSeq
LambdaExpression(boundsSeq, body, boundsSeq.length.asInstanceOf)
}
type LambdaTT[N <: Arity] = LambdaExpression[Term, Term, N]
type LambdaTF[N <: Arity] = LambdaExpression[Term, Formula, N]
type LambdaFF[N <: Arity] = LambdaExpression[Formula, Formula, N]
/**
* Recovers the underlying [[K.LambdaTermTerm]]
*/
extension [N <: Arity](ltt: LambdaExpression[Term, Term, N]) {
def underlyingLTT: K.LambdaTermTerm =
K.LambdaTermTerm(ltt.bounds.map(b => b.asInstanceOf[Variable].underlyingLabel), ltt.body.underlying)
}
/**
* Recovers the underlying [[K.LambdaTermFormula]]
*/
extension [N <: Arity](ltf: LambdaExpression[Term, Formula, N]) {
def underlyingLTF: K.LambdaTermFormula =
K.LambdaTermFormula(ltf.bounds.map(b => b.asInstanceOf[Variable].underlyingLabel), ltf.body.underlying)
}
/**
* Recovers the underlying [[K.LambdaFormulaFormula]]
*/
extension [N <: Arity](lff: LambdaExpression[Formula, Formula, N]) {
def underlyingLFF: K.LambdaFormulaFormula =
K.LambdaFormulaFormula(lff.bounds.map((b: SchematicLabel[Formula]) => b.asInstanceOf[VariableFormula].underlyingLabel), lff.body.underlying)
}
}
lisa-utils/src/main/scala/lisa/fol/Predef.scala 0 → 100644
+ 78
− 0
View file @ 265ed45e
package lisa.fol
import lisa.utils.K
trait Predef extends Common {
val equality: ConstantPredicateLabel[2] = ConstantPredicateLabel[2](K.Identifier("="), 2)
val === = equality
val ＝ = equality
extension (t: Term) {
infix def ===(u: Term): Formula = equality(t, u)
infix def ＝(u: Term): Formula = equality(t, u)
}
val top: ConstantFormula = ConstantFormula(K.Identifier("⊤"))
val ⊤ : top.type = top
val True: top.type = top
val bot: ConstantFormula = ConstantFormula(K.Identifier("⊥"))
val ⊥ : bot.type = bot
val False: bot.type = bot
case object Neg extends ConstantConnectorLabel[1] { val underlyingLabel = K.Neg; val arity = 1 }
val neg = Neg
val ¬ = Neg
val ! = Neg
case object And extends ConstantConnectorLabel[-1] { val underlyingLabel = K.And; val arity = -1 }
val and: And.type = And
val /\ : And.type = And
val ∧ : And.type = And
case object Or extends ConstantConnectorLabel[-1] { val underlyingLabel = K.Or; val arity = -1 }
val or: Or.type = Or
val \/ : Or.type = Or
val ∨ : Or.type = Or
case object Implies extends ConstantConnectorLabel[2] { val underlyingLabel = K.Implies; val arity = 2 }
val implies: Implies.type = Implies
val ==> : Implies.type = Implies
case object Iff extends ConstantConnectorLabel[2] { val underlyingLabel = K.Iff; val arity = 2 }
val iff: Iff.type = Iff
val <=> : Iff.type = Iff
case object Forall extends BaseBinderLabel {
val id = K.Identifier("∀")
val underlyingLabel: K.Forall.type = K.Forall
}
val forall: Forall.type = Forall
val ∀ : Forall.type = forall
case object Exists extends BaseBinderLabel {
val id = K.Identifier("∃")
val underlyingLabel: K.Exists.type = K.Exists
}
val exists: Exists.type = Exists
val ∃ : Exists.type = exists
case object ExistsOne extends BaseBinderLabel {
val id = K.Identifier("∃!")
val underlyingLabel: K.ExistsOne.type = K.ExistsOne
}
val existsOne: ExistsOne.type = ExistsOne
val ∃! : ExistsOne.type = existsOne
extension (f: Formula) {
def unary_! = Neg(f *: EmptyTuple)
infix inline def ==>(g: Formula): Formula = Implies(f, g)
infix inline def <=>(g: Formula): Formula = Iff(f, g)
infix inline def /\(g: Formula): Formula = And(List(f, g))
infix inline def ∧(g: Formula): Formula = And(List(f, g))
infix inline def \/(g: Formula): Formula = Or(List(f, g))
infix inline def ∨(g: Formula): Formula = Or(List(f, g))
}
}
lisa-utils/src/main/scala/lisa/fol/Sequents.scala 0 → 100644
+ 225
− 0
View file @ 265ed45e
package lisa.fol
//import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.fol.FOLHelpers.*
import lisa.prooflib.BasicStepTactic
import lisa.prooflib.Library
import lisa.prooflib.ProofTacticLib.ProofTactic
import lisa.utils.K
import scala.annotation.showAsInfix
trait Sequents extends Common with lisa.fol.Lambdas {
object SequentInstantiationRule extends ProofTactic
given ProofTactic = SequentInstantiationRule
case class Sequent(left: Set[Formula], right: Set[Formula]) extends LisaObject[Sequent] with Absolute {
def underlying: lisa.kernel.proof.SequentCalculus.Sequent = K.Sequent(left.map(_.underlying), right.map(_.underlying))
def allSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.allSchematicLabels)
def freeSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.freeSchematicLabels)
def substituteUnsafe(map: Map[SchematicLabel[?], ? <: LisaObject[?]]): Sequent = Sequent(left.map(_.substituteUnsafe(map)), right.map(_.substituteUnsafe(map)))
/*Ok for now but what when we have more*/
/**
* Substitute schematic symbols inside this, and produces a kernel proof.
* Namely, if "that" is the result of the substitution, the proof should conclude with "that.underlying",
* using the assumption "this.underlying" at step index -1.
*
* @param map
* @return
*/
def substituteWithProof(map: Map[SchematicLabel[_], _ <: LisaObject[_]]): (Sequent, Seq[K.SCProofStep]) = {
val mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]] =
map.collect[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]](p =>
p._1 match {
case sl: Variable => (sl, LambdaExpression[Term, Term, 0](Seq(), p._2.asInstanceOf[Term], 0))
case sl: SchematicFunctionLabel[?] =>
p._2 match {
case l: LambdaExpression[Term, Term, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[Variable]) & l.body.isInstanceOf[Term] =>
(p._1.asInstanceOf, l)
case s: TermLabel =>
val vars = nFreshId(Seq(s.id), s.arity).map(id => Variable(id))
(sl, LambdaExpression(vars, s(vars), s.arity))
}
}
)
val mPred: Map[SchematicPredicateLabel[?] | VariableFormula, LambdaExpression[Term, Formula, ?]] =
map.collect[SchematicPredicateLabel[?] | VariableFormula, LambdaExpression[Term, Formula, ?]](p =>
p._1 match {
case sl: VariableFormula => (sl, LambdaExpression[Term, Formula, 0](Seq(), p._2.asInstanceOf[Formula], 0))
case sl: SchematicPredicateLabel[?] =>
p._2 match {
case l: LambdaExpression[Term, Formula, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[Variable]) & l.body.isInstanceOf[Formula] => (sl, l)
case s: PredicateLabel =>
val vars = nFreshId(Seq(s.id), s.arity).map(id => Variable(id))
(sl, LambdaExpression(vars, s(vars), s.arity))
}
}
)
val mConn = map.collect[SchematicConnectorLabel[?], LambdaExpression[Formula, Formula, ?]](p =>
p._1 match {
case sl: SchematicConnectorLabel[?] =>
p._2 match {
case l: LambdaExpression[Formula, Formula, ?] @unchecked if (l.bounds.isEmpty || l.bounds.head.isInstanceOf[VariableFormula]) & l.body.isInstanceOf[Formula] => (sl, l)
case s: ConnectorLabel =>
val vars = nFreshId(Seq(s.id), s.arity).map(VariableFormula.apply)
(sl, LambdaExpression(vars, s(vars), s.arity))
}
}
)
(substituteUnsafe(map), substituteWithProofLikeKernel(mConn, mPred, mTerm))
}
/**
* Given 3 substitution maps like the kernel accepts, i.e. Substitution of Predicate Connector and Term schemas, do the substitution
* and produce the (one-step) kernel proof that the result is provable from the original sequent
*
* @param mCon The substitution of connector schemas
* @param mPred The substitution of predicate schemas
* @param mTerm The substitution of function schemas
* @return
*/
def substituteWithProofLikeKernel(
mCon: Map[SchematicConnectorLabel[?], LambdaExpression[Formula, Formula, ?]],
mPred: Map[SchematicPredicateLabel[?] | VariableFormula, LambdaExpression[Term, Formula, ?]],
mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]]
): Seq[K.SCProofStep] = {
val premiseSequent = this.underlying
val mConK = mCon.map((sl, le) => (sl.underlyingLabel, underlyingLFF(le)))
val mPredK = mPred.map((sl, le) =>
sl match {
case v: VariableFormula => (v.underlyingLabel, underlyingLTF(le))
case spl: SchematicPredicateLabel[?] => (spl.underlyingLabel, underlyingLTF(le))
}
)
val mTermK = mTerm.map((sl, le) =>
sl match {
case v: Variable => (v.underlyingLabel, underlyingLTT(le))
case sfl: SchematicFunctionLabel[?] => (sfl.underlyingLabel, underlyingLTT(le))
}
)
val botK = lisa.utils.KernelHelpers.instantiateSchemaInSequent(premiseSequent, mConK, mPredK, mTermK)
val smap = Map[SchematicLabel[?], LisaObject[?]]() ++ mCon ++ mPred ++ mTerm
Seq(K.InstSchema(botK, -1, mConK, mPredK, mTermK))
}
infix def +<<(f: Formula): Sequent = this.copy(left = this.left + f)
infix def -<<(f: Formula): Sequent = this.copy(left = this.left - f)
infix def +>>(f: Formula): Sequent = this.copy(right = this.right + f)
infix def ->>(f: Formula): Sequent = this.copy(right = this.right - f)
infix def ++<<(s1: Sequent): Sequent = this.copy(left = this.left ++ s1.left)
infix def --<<(s1: Sequent): Sequent = this.copy(left = this.left -- s1.left)
infix def ++>>(s1: Sequent): Sequent = this.copy(right = this.right ++ s1.right)
infix def -->>(s1: Sequent): Sequent = this.copy(right = this.right -- s1.right)
infix def ++(s1: Sequent): Sequent = this.copy(left = this.left ++ s1.left, right = this.right ++ s1.right)
infix def --(s1: Sequent): Sequent = this.copy(left = this.left -- s1.left, right = this.right -- s1.right)
infix def removeLeft(f: Formula): Sequent = this.copy(left = this.left.filterNot(isSame(_, f)))
infix def removeRight(f: Formula): Sequent = this.copy(right = this.right.filterNot(isSame(_, f)))
infix def removeAllLeft(s1: Sequent): Sequent = this.copy(left = this.left.filterNot(e1 => s1.left.exists(e2 => isSame(e1, e2))))
infix def removeAllLeft(s1: Set[Formula]): Sequent = this.copy(left = this.left.filterNot(e1 => s1.exists(e2 => isSame(e1, e2))))
infix def removeAllRight(s1: Sequent): Sequent = this.copy(right = this.right.filterNot(e1 => s1.right.exists(e2 => isSame(e1, e2))))
infix def removeAllRight(s1: Set[Formula]): Sequent = this.copy(right = this.right.filterNot(e1 => s1.exists(e2 => isSame(e1, e2))))
infix def removeAll(s1: Sequent): Sequent =
this.copy(left = this.left.filterNot(e1 => s1.left.exists(e2 => isSame(e1, e2))), right = this.right.filterNot(e1 => s1.right.exists(e2 => isSame(e1, e2))))
infix def addLeftIfNotExists(f: Formula): Sequent = if (this.left.exists(isSame(_, f))) this else (this +<< f)
infix def addRightIfNotExists(f: Formula): Sequent = if (this.right.exists(isSame(_, f))) this else (this +>> f)
infix def addAllLeftIfNotExists(s1: Sequent): Sequent = this ++<< s1.copy(left = s1.left.filterNot(e1 => this.left.exists(isSame(_, e1))))
infix def addAllRightIfNotExists(s1: Sequent): Sequent = this ++>> s1.copy(right = s1.right.filterNot(e1 => this.right.exists(isSame(_, e1))))
infix def addAllIfNotExists(s1: Sequent): Sequent =
this ++ s1.copy(left = s1.left.filterNot(e1 => this.left.exists(isSame(_, e1))), right = s1.right.filterNot(e1 => this.right.exists(isSame(_, e1))))
// OL shorthands
infix def +<?(f: Formula): Sequent = this addLeftIfNotExists f
infix def -<?(f: Formula): Sequent = this removeLeft f
infix def +>?(f: Formula): Sequent = this addRightIfNotExists f
infix def ->?(f: Formula): Sequent = this removeRight f
infix def ++<?(s1: Sequent): Sequent = this addAllLeftIfNotExists s1
infix def --<?(s1: Sequent): Sequent = this removeAllLeft s1
infix def ++>?(s1: Sequent): Sequent = this addAllRightIfNotExists s1
infix def -->?(s1: Sequent): Sequent = this removeAllRight s1
infix def --?(s1: Sequent): Sequent = this removeAll s1
infix def ++?(s1: Sequent): Sequent = this addAllIfNotExists s1
override def toString = left.mkString("; ") + " ⊢ " + right.mkString("; ")
}
val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
given Conversion[Formula, Sequent] = f => Sequent(Set.empty, Set(f))
def isSame(formula1: Formula, formula2: Formula): Boolean = {
K.isSame(formula1.underlying, formula2.underlying)
}
def isSameTerm(term1: Term, term2: Term): Boolean = {
K.isSameTerm(term1.underlying, term2.underlying)
}
def isSameSequent(sequent1: Sequent, sequent2: Sequent): Boolean = {
K.isSameSequent(sequent1.underlying, sequent2.underlying)
}
/**
* returns true if the first argument implies the second by the laws of ortholattices.
*/
def isImplying(formula1: Formula, formula2: Formula): Boolean = {
K.isImplying(formula1.underlying, formula2.underlying)
}
def isImplyingSequent(sequent1: Sequent, sequent2: Sequent): Boolean = {
K.isImplyingSequent(sequent1.underlying, sequent2.underlying)
}
def isSubset(s1: Set[Formula], s2: Set[Formula]): Boolean = {
K.isSubset(s1.map(_.underlying), s2.map(_.underlying))
}
def isSameSet(s1: Set[Formula], s2: Set[Formula]): Boolean =
K.isSameSet(s1.map(_.underlying), s2.map(_.underlying))
def contains(s: Set[Formula], f: Formula): Boolean = {
K.contains(s.map(_.underlying), f.underlying)
}
/**
* Represents a converter of some object into a set.
* @tparam S The type of elements in that set
* @tparam T The type to convert from
*/
protected trait FormulaSetConverter[T] {
def apply(t: T): Set[Formula]
}
given FormulaSetConverter[Unit] with {
override def apply(u: Unit): Set[Formula] = Set.empty
}
given FormulaSetConverter[EmptyTuple] with {
override def apply(t: EmptyTuple): Set[Formula] = Set.empty
}
given [H <: Formula, T <: Tuple](using c: FormulaSetConverter[T]): FormulaSetConverter[H *: T] with {
override def apply(t: H *: T): Set[Formula] = c.apply(t.tail) + t.head
}
given formula_to_set[T <: Formula]: FormulaSetConverter[T] with {
override def apply(f: T): Set[Formula] = Set(f)
}
given iterable_to_set[T <: Formula, I <: Iterable[T]]: FormulaSetConverter[I] with {
override def apply(s: I): Set[Formula] = s.toSet
}
private def any2set[A, T <: A](any: T)(using c: FormulaSetConverter[T]): Set[Formula] = c.apply(any)
extension [A, T1 <: A](left: T1)(using FormulaSetConverter[T1]) {
infix def |-[B, T2 <: B](right: T2)(using FormulaSetConverter[T2]): Sequent = Sequent(any2set(left), any2set(right))
infix def ⊢[B, T2 <: B](right: T2)(using FormulaSetConverter[T2]): Sequent = Sequent(any2set(left), any2set(right))
}
}
lisa-utils/src/main/scala/lisa/prooflib/Library.scala
+ 34
− 241
View file @ 265ed45e
...@@ -5,6 +5,7 @@ import lisa.kernel.proof.SCProofChecker ...@@ -5,6 +5,7 @@ import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SCProofCheckerJudgement import lisa.kernel.proof.SCProofCheckerJudgement
import lisa.kernel.proof.SequentCalculus import lisa.kernel.proof.SequentCalculus
import lisa.prooflib.ProofTacticLib.ProofTactic import lisa.prooflib.ProofTacticLib.ProofTactic
import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.{_, given} import lisa.utils.{_, given}
import scala.collection.mutable.Stack as stack import scala.collection.mutable.Stack as stack
...@@ -15,103 +16,49 @@ import scala.collection.mutable.Stack as stack ...@@ -15,103 +16,49 @@ import scala.collection.mutable.Stack as stack
* @param theory The inner RunningTheory * @param theory The inner RunningTheory
*/ */
abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.ProofsHelpers { abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.ProofsHelpers {
val theory: RunningTheory val theory: RunningTheory
given library: this.type = this given library: this.type = this
given RunningTheory = theory given RunningTheory = theory
export lisa.kernel.fol.FOL.{Formula, *}
val SC: SequentCalculus.type = lisa.kernel.proof.SequentCalculus
export lisa.kernel.proof.SequentCalculus.{Sequent, SCProofStep}
export lisa.kernel.proof.SCProof
export lisa.prooflib.TheoriesHelpers.{_, given}
import lisa.kernel.proof.RunningTheoryJudgement as Judgement
/**
* a type representing different types that have a natural representation as Sequent
*/
type Sequentable = theory.Justification | Formula | Sequent
var last: Option[theory.Justification] = None
/**
* A function intended for use to construct a proof:
* <pre> SCProof(steps(...), imports(...))</pre>
* Must contains [[SCProofStep]]'s
*/
inline def steps(sts: SCProofStep*): IndexedSeq[SCProofStep] = sts.toIndexedSeq
/**
* A function intended for use to construct a proof:
* <pre> SCProof(steps(...), imports(...))</pre>
* Must contains [[Justification]]'s, [[Formula]]'s or [[Sequent]], all of which are converted adequatly automatically.
*/
inline def imports(sqs: Sequentable*): IndexedSeq[Sequent] = sqs.map(sequentableToSequent).toIndexedSeq
// THEOREM Syntax
/** export lisa.kernel.proof.SCProof
* An alias to create a Theorem
*/
def makeTheorem(name: String, statement: Sequent, proof: SCProof, justifications: Seq[theory.Justification]): Judgement[theory.Theorem] =
theory.theorem(name, statement, proof, justifications)
/** val K = lisa.utils.K
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> val SC: SequentCalculus.type = K.SC
*/ private[prooflib] val F = lisa.fol.FOL
case class TheoremNameWithStatement(name: String, statement: Sequent) { import F.{given}
/** var last: Option[JUSTIFICATION] = None
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
def PROOF2(proof: SCProof)(using om: OutputManager): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
/** val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
def PROOF2(steps: IndexedSeq[SCProofStep])(using om: OutputManager): TheoremNameWithProof =
TheoremNameWithProof(name, statement, SCProof(steps))
def addSymbol(s: F.ConstantFunctionLabel[?] | F.ConstantPredicateLabel[?] | F.Constant): Unit = {
s match {
case s: F.ConstantFunctionLabel[?] => theory.addSymbol(s.underlyingLabel)
case s: F.ConstantPredicateLabel[?] => theory.addSymbol(s.underlyingLabel)
case s: F.Constant => theory.addSymbol(s.underlyingLabel)
}
knownDefs.update(s, None)
} }
/** def getDefinition(label: F.ConstantLabel[?]): Option[JUSTIFICATION] = knownDefs.get(label) match {
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> case None => throw new UserLisaException.UndefinedSymbolException("Unknown symbol", label, this)
*/ case Some(value) => value
case class TheoremName(name: String) {
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
infix def of(statement: Sequent): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
infix def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, lisa.utils.FOLParser.parseSequent(statement))
} }
/** /**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> * An alias to create a Theorem
*/
def THEOREM(name: String): TheoremName = TheoremName(name)
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/ */
case class TheoremNameWithProof(name: String, statement: Sequent, proof: SCProof)(using om: OutputManager) { def makeTheorem(name: String, statement: K.Sequent, proof: K.SCProof, justifications: Seq[theory.Justification]): K.Judgement[theory.Theorem] =
infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match { theory.theorem(name, statement, proof, justifications)
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[?] => wrongJudgement.showAndGet
}
/**
* Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
*/
infix def using(u: Unit): theory.Theorem = using()
}
// DEFINITION Syntax // DEFINITION Syntax
/** /**
* Allows to create a definition by shortcut of a function symbol: * Allows to create a definition by shortcut of a function symbol:
*/ */
def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] = { def makeSimpleFunctionDefinition(symbol: String, expression: K.LambdaTermTerm): K.Judgement[theory.FunctionDefinition] = {
import K.*
val LambdaTermTerm(vars, body) = expression val LambdaTermTerm(vars, body) = expression
val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicTermLabels.map(_.id)).toSet, "y")) val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicTermLabels.map(_.id)).toSet, "y"))
...@@ -122,106 +69,11 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro ...@@ -122,106 +69,11 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
/** /**
* Allows to create a definition by shortcut of a predicate symbol: * Allows to create a definition by shortcut of a predicate symbol:
*/ */
def simpleDefinition(symbol: String, expression: LambdaTermFormula): Judgement[theory.PredicateDefinition] = def makeSimplePredicateDefinition(symbol: String, expression: K.LambdaTermFormula): K.Judgement[theory.PredicateDefinition] =
theory.predicateDefinition(symbol, expression) theory.predicateDefinition(symbol, expression)
/* private def simpleFunctionDefinition(expression: K.LambdaTermTerm, out: K.VariableLabel): K.SCProof = {
import K.{*, given}
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
* or
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
case class FunSymbolDefine(symbol: String, vars: Seq[VariableLabel]) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
infix def as(t: Term)(using om: OutputManager): ConstantFunctionLabel = {
val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[?] => wrongJudgement.showAndGet
}
definition.label
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
*/
infix def as(f: Formula)(using om: OutputManager): ConstantPredicateLabel = {
val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[?] => wrongJudgement.showAndGet
}
definition.label
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
infix def asThe(out: VariableLabel): DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out)
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
case class DefinitionNameAndOut(symbol: String, vars: Seq[VariableLabel], out: VariableLabel) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
infix def suchThat(f: Formula): DefinitionWaitingProof = DefinitionWaitingProof(symbol, vars, out, f)
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
case class DefinitionWaitingProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
infix def PROOF(proof: SCProof): DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
case class DefinitionWithProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula, proof: SCProof) {
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
infix def using(justifications: theory.Justification*)(using om: OutputManager): ConstantFunctionLabel = {
val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match {
case Judgement.ValidJustification(just) =>
last = Some(just)
just
case wrongJudgement: Judgement.InvalidJustification[?] => wrongJudgement.showAndGet
}
definition.label
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
infix def using(u: Unit)(using om: OutputManager): ConstantFunctionLabel = using()
}
/**
* Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
*/
def DEFINE(symbol: String, vars: VariableLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars)
*/
/**
* For a definition of the type f(x) := term, construct the required proof ?!y. y = term.
*/
private def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): SCProof = {
val x = out val x = out
val LambdaTermTerm(vars, body) = expression val LambdaTermTerm(vars, body) = expression
val xeb = x === body val xeb = x === body
...@@ -232,82 +84,23 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro ...@@ -232,82 +84,23 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
val s3 = SC.RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body) val s3 = SC.RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
val s4 = SC.Restate(() |- existsOne(x, xeb), 3) val s4 = SC.Restate(() |- existsOne(x, xeb), 3)
val v = Vector(s0, s1, s2, s3, s4) val v = Vector(s0, s1, s2, s3, s4)
SCProof(v) K.SCProof(v)
} }
//////////////////////////////////////////
// Tools for proof development //
//////////////////////////////////////////
given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
/** /**
* Allows to fetch a Justification (Axiom, Theorem or Definition) by it's name or symbol: * Prints a short representation of the given theorem or definition
* <pre>thm"fundamentalTheoremOfAlgebra", ax"comprehensionAxiom", defi"+"
*/ */
implicit class StringToJust(val sc: StringContext) { def show(using om: OutputManager)(thm: JUSTIFICATION) = {
if (thm.withSorry) om.output(thm.repr, Console.YELLOW)
def thm(args: Any*): theory.Theorem = getTheorem(sc.parts.mkString("")) else om.output(thm.repr, Console.GREEN)
def ax(args: Any*): theory.Axiom = getAxiom(sc.parts.mkString(""))
def defi(args: Any*): theory.Definition = getDefinition(sc.parts.mkString(""))
} }
/**
* Fetch a Theorem by its name.
*/
def getTheorem(name: String): theory.Theorem =
theory.getTheorem(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No theorem with name \"$name\" was found.")
}
/**
* Fetch an Axiom by its name.
*/
def getAxiom(name: String): theory.Axiom =
theory.getAxiom(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No axiom with name \"$name\" was found.")
}
/**
* Fetch a Definition by its symbol.
*/
def getDefinition(name: String): theory.Definition =
theory.getDefinition(name) match {
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
}
/** /**
* Prints a short representation of the last theorem or definition introduced * Prints a short representation of the last theorem or definition introduced
*/ */
def show(using om: OutputManager): theory.Justification = last match { def show(using om: OutputManager): Unit = last match {
case Some(value) => value.show case Some(value) => show(value)
case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.") case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
} }
/**
* Converts different class that have a natural interpretation as a Sequent
*/
private def sequentableToSequent(s: Sequentable): Sequent = s match {
case j: theory.Justification => theory.sequentFromJustification(j)
case f: Formula => () |- f
case s: Sequent => s
}
given convJustSequent[C <: Iterable[Sequentable], D](using bf: scala.collection.BuildFrom[C, Sequent, D]): Conversion[C, D] = cc => {
val builder = bf.newBuilder(cc)
cc.foreach(builder += sequentableToSequent(_))
builder.result
}
given convStrInt[C <: Iterable[String], D](using bf: scala.collection.BuildFrom[C, Int, D]): Conversion[C, D] = cc => {
val builder = bf.newBuilder(cc)
cc.foreach(builder += _.size)
builder.result
}
} }
lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala
+ 3
− 2
View file @ 265ed45e
package lisa.prooflib package lisa.prooflib
import lisa.prooflib.TheoriesHelpers.show import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.{_, given} import lisa.utils.{_, given}
import java.io.PrintWriter import java.io.PrintWriter
import java.io.StringWriter import java.io.StringWriter
abstract class OutputManager { abstract class OutputManager {
given OutputManager = this given OutputManager = this
def output(s: String): Unit = stringWriter.write(s + "\n") def output(s: String): Unit = stringWriter.write(s + "\n")
...@@ -27,7 +28,7 @@ abstract class OutputManager { ...@@ -27,7 +28,7 @@ abstract class OutputManager {
case Some(value) => output(lisa.utils.ProofPrinter.prettyProof(value)) case Some(value) => output(lisa.utils.ProofPrinter.prettyProof(value))
case None => () case None => ()
} }
e.underlying.show output(e.underlying.repr)
finishOutput(e) finishOutput(e)
} }
......
lisa-utils/src/main/scala/lisa/prooflib/ProofTacticLib.scala
+ 4
− 96
View file @ 265ed45e
package lisa.prooflib package lisa.prooflib
import lisa.kernel.proof import lisa.fol.FOL as F
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheoryJudgement
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustificationException
import lisa.kernel.proof.SequentCalculus.*
import lisa.prooflib.* import lisa.prooflib.*
import lisa.utils.KernelHelpers.* import lisa.utils.K
import lisa.utils.Printer import lisa.utils.Printer
import lisa.utils.UserLisaException import lisa.utils.UserLisaException
...@@ -28,14 +23,14 @@ object ProofTacticLib { ...@@ -28,14 +23,14 @@ object ProofTacticLib {
} }
trait ProofSequentTactic { trait ProofSequentTactic {
def apply(using lib: Library, proof: lib.Proof)(bot: Sequent): proof.ProofTacticJudgement def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement
} }
trait ProofFactTactic { trait ProofFactTactic {
def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact): proof.ProofTacticJudgement def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact): proof.ProofTacticJudgement
} }
trait ProofFactSequentTactic { trait ProofFactSequentTactic {
def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement
} }
class UnapplicableProofTactic(val tactic: ProofTactic, proof: Library#Proof, errorMessage: String)(using sourcecode.Line, sourcecode.File) extends UserLisaException(errorMessage) { class UnapplicableProofTactic(val tactic: ProofTactic, proof: Library#Proof, errorMessage: String)(using sourcecode.Line, sourcecode.File) extends UserLisaException(errorMessage) {
...@@ -68,91 +63,4 @@ object ProofTacticLib { ...@@ -68,91 +63,4 @@ object ProofTacticLib {
lisa.utils.ProofPrinter.prettyProof(failure.proof) lisa.utils.ProofPrinter.prettyProof(failure.proof)
} }
/*
/**
* A proof step lacking a bottom/conclusion sequent. Once given a conclusion sequent, it can become a ProofTactic.
*/
trait ProofTacticWithoutBot extends ProofTactic{
def apply(using proof:Library#Proof)(a:Any*)(bot:Sequent): proof.ProofTacticJudgement
}
/**
* Represent a ProofTactic lacking the list of its premises, for partial application.
*/
trait ProofTacticWithoutPrem[N <: Arity](val numbPrem: N){
val proof:ProofOfProofTacticLib
type P = proof.type
val nameWP: String = this.getClass.getSimpleName
/**
* An abstract function transforming the ProofTacticWithoutPrem innto a SCProofStep in pure Sequent Calculus.
*/
def asSCProof(givenPremises:Seq[proof.Fact]): proof.ProofTacticJudgement
/**
* Gives the premises of the ProofTactic, as a partial application towards the SC transformation.
*/
def asProofTactic(premises: Seq[proof.Fact]): ProofTactic{val proof:P} =
(new ProofTactic{
override val proof: P = ProofTacticWithoutPrem.this.proof
override val name: String = nameWP
override def asSCProof: proof.ProofTacticJudgement = ProofTacticWithoutPrem.this.asSCProof(premises)
}).asInstanceOf
/**
* Alias for [[asProofTactic]]
*/
def by(premises: Seq[proof.Fact]): ProofTactic{val proof:P} = asProofTactic(premises)
}
/**
* A ProofTactic without premises nor targeted bottom sequent.
* Contains a tactic to reconstruct a partial Sequent Calculus proof if given those elements and the current proof.
*/
trait ProofTacticWithoutBotNorPrem[N <: Arity](val numbPrem:N){
val proof:ProofOfProofTacticLib
type P = proof.type
val nameWBNP: String = this.getClass.getSimpleName
/**
* Contains a tactic to reconstruct a partial Sequent Calculus proof if given
* a list of premises, a targeted bottom sequent and the current proof.
*/
def asSCProof(bot: Sequent, premises: Seq[proof.Fact]): proof.ProofTacticJudgement
def asProofTacticWithoutBot(premises: Seq[proof.Fact]): ProofTacticWithoutBot{val proof:P} =
(new ProofTacticWithoutBot[N]{
override val proof: P = ProofTacticWithoutBotNorPrem.this.proof
override val name: String = nameWBNP
override def asSCProof(bot: Sequent): proof.ProofTacticJudgement = ProofTacticWithoutBotNorPrem.this.asSCProof(bot, premises)
}).asInstanceOf
def apply(premises: proof.Fact*): ProofTacticWithoutBot{val proof:PP} = asProofTacticWithoutBot(premises)
}
/**
* Intermediate datatype corresponding to a [[ProofTacticWithoutBotNorPrem]] once a sequence of premises has been given to it.
*/
class ProofTacticWithoutBotWithPrem[N <: Arity] protected[ProofTacticLib] (
val underlying: ProofTacticWithoutBotNorPrem[N],
givenPremises: Seq[underlying.proof.Fact],
override val nameWB: String
) extends ProofTacticWithoutBot {
val proof : underlying.proof.type = underlying.proof
val numbPrem: N = underlying.numbPrem
/**
* Contains a tactic to reconstruct a partial Sequent Calculus proof if given
* a targeted bottom sequent and the current proof.
*/
def asSCProof(bot: Sequent): proof.ProofTacticJudgement = {
underlying.asSCProof(bot, givenPremises)
}
}
*/
} }
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment