Skip to content

Commit

Permalink
Some tests pass.
Browse files Browse the repository at this point in the history
  • Loading branch information
@SimonGuilloud
SimonGuilloud committed Oct 20, 2024
1 parent c9f37c6 commit 6e06964
Show file tree
Hide file tree
Showing 12 changed files with 171 additions and 359 deletions.
35 changes: 15 additions & 20 deletions lisa-kernel/src/main/scala/lisa/kernel/fol/OLEquivalenceChecker.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,10 @@ private[fol] trait OLEquivalenceChecker extends Syntax {
@deprecated("Use isSame instead", "0.8")
def isSameTerm(term1: Expression, term2: Expression): Boolean = isSame(term1, term2)
def isSame(e1: Expression, e2: Expression): Boolean = {
if (e1.containsFormulas != e2.containsFormulas) false
else if (!e1.containsFormulas) e1 == e2
else {
val nf1 = computeNormalForm(simplify(e1))
val nf2 = computeNormalForm(simplify(e2))
latticesEQ(nf1, nf2)
}
val nf1 = computeNormalForm(simplify(e1))
val nf2 = computeNormalForm(simplify(e2))
latticesEQ(nf1, nf2)

}

/**
Expand Down Expand Up @@ -469,17 +466,15 @@ private[fol] trait OLEquivalenceChecker extends Syntax {

def latticesEQ(e1: SimpleExpression, e2: SimpleExpression): Boolean =
if (e1.uniqueKey == e2.uniqueKey) true
else if (e1.containsFormulas && e2.containsFormulas) {
if (e1.sort == Formula) latticesLEQ(e1, e2) && latticesLEQ(e2, e1)
else (e1, e2) match {
case (s1: SimpleBoundVariable, s2: SimpleBoundVariable) => s1 == s2
case (s1: SimpleVariable, s2: SimpleVariable) => s1 == s2
case (s1: SimpleConstant, s2: SimpleConstant) => s1 == s2
case (SimpleApplication(f1, arg1, polarity1), SimpleApplication(f2, arg2, polarity2)) =>
polarity1 == polarity2 && latticesEQ(f1, f2) && latticesEQ(arg1, arg2)
case (SimpleLambda(x1, body1), SimpleLambda(x2, body2)) =>
latticesEQ(body1, body2)
case (_, _) => false
}
} else e1 == e2
else if (e1.sort == Formula) latticesLEQ(e1, e2) && latticesLEQ(e2, e1)
else (e1, e2) match {
case (s1: SimpleBoundVariable, s2: SimpleBoundVariable) => s1 == s2
case (s1: SimpleVariable, s2: SimpleVariable) => s1 == s2
case (s1: SimpleConstant, s2: SimpleConstant) => s1 == s2
case (SimpleApplication(f1, arg1, polarity1), SimpleApplication(f2, arg2, polarity2)) =>
polarity1 == polarity2 && latticesEQ(f1, f2) && latticesEQ(arg1, arg2)
case (SimpleLambda(x1, body1), SimpleLambda(x2, body2)) =>
latticesEQ(body1, body2)
case (_, _) => false
}
}
88 changes: 21 additions & 67 deletions lisa-kernel/src/main/scala/lisa/kernel/fol/Syntax.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,72 +132,6 @@ private[fol] trait Syntax {
def allVariables: Set[Variable] = body.allVariables
}

/*
object Equality {
def unapply (e: Expression): Option[(Expression, Expression)] = e match {
case Application(Application(`equality`, arg1), arg2) => Some((arg1, arg2))
case _ => None
}
def apply(arg1: Expression, arg2: Expression): Expression = equality(arg1)(arg2)
}
object Neg {
def unapply (e: Expression): Option[Expression] = e match {
case Application(`neg`, arg) => Some(arg)
case _ => None
}
def apply(arg: Expression): Expression = neg(arg)
}
object Implies {
def unapply (e: Expression): Option[(Expression, Expression)] = e match {
case Application(Application(`implies`, arg1), arg2) => Some((arg1, arg2))
case _ => None
}
def apply(arg1: Expression, arg2: Expression): Expression = implies(arg1)(arg2)
}
object Iff {
def unapply (e: Expression): Option[(Expression, Expression)] = e match {
case Application(Application(`iff`, arg1), arg2) => Some((arg1, arg2))
case _ => None
}
def apply(arg1: Expression, arg2: Expression): Expression = iff(arg1)(arg2)
}
object And {
def unapply (e: Expression): Option[(Expression, Expression)] = e match {
case Application(Application(`and`, arg1), arg2) => Some((arg1, arg2))
case _ => None
}
def apply(args: Iterable[Expression]): Expression = args.reduceLeft(and(_)(_))
}
object Or {
def unapply (e: Expression): Option[(Expression, Expression)] = e match {
case Application(Application(`or`, arg1), arg2) => Some((arg1, arg2))
case _ => None
}
def apply(args: Iterable[Expression]): Expression = args.reduceLeft(and(_)(_))
}
object Forall {
def unapply (e: Expression): Option[(Variable, Expression)] = e match {
case Application(`forall`, Lambda(v, body)) => Some((v, body))
case _ => None
}
def apply(v: Variable, body: Expression): Expression = forall(Lambda(v, body))
}
object Exists {
def unapply (e: Expression): Option[(Variable, Expression)] = e match {
case Application(`exists`, Lambda(v, body)) => Some((v, body))
case _ => None
}
def apply(v: Variable, body: Expression): Expression = exists(Lambda(v, body))
}
object Epsilon {
def unapply (e: Expression): Option[(Variable, Expression)] = e match {
case Application(`epsilon`, Lambda(v, body)) => Some((v, body))
case _ => None
}
def apply(v: Variable, body: Expression): Expression = epsilon(Lambda(v, body))
}
*/

val equality = Constant(Identifier("="), Term -> (Term -> Formula))
val top = Constant(Identifier("⊤"), Formula)
Expand Down Expand Up @@ -229,12 +163,32 @@ private[fol] trait Syntax {
case c: Constant => c
case Application(f, arg) => Application(substituteVariables(f, m), substituteVariables(arg, m))
case Lambda(v, t) =>
Lambda(v, substituteVariables(t, m - v))
val newSubst = m - v
val fv = m.values.flatMap(_.freeVariables).toSet
if (fv.contains(v)) {
val newBound = Variable(freshId(fv.view.map(_.id) ++ m.keys.view.map(_.id), v.id), v.sort)
Lambda(newBound, substituteVariables(t, newSubst + (v -> newBound)))
}
else Lambda(v, substituteVariables(t, m - v))
}

def flatTypeParameters(t: Sort): List[Sort] = t match {
case Arrow(a, b) => a :: flatTypeParameters(b)
case _ => List()
}

def betaReduce(e: Expression): Expression = e match {
case Application(f, arg) => {
val f1 = betaReduce(f)
val a2 = betaReduce(arg)
f1 match {
case Lambda(v, body) => betaReduce(substituteVariables(body, Map(v -> a2)))
case _ => Application(f1, betaReduce(a2))
}
}
case Lambda(v, inner) =>
Lambda(v, betaReduce(inner))
case _ => e
}

}
57 changes: 8 additions & 49 deletions lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -381,58 +381,17 @@ object SCProofChecker {
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Conclusion cannot be trivially derived from premise.")


/**
* <pre>
* Γ |- φ[(λy. e)t/x], Δ
* ---------------------------
* Γ |- φ[e[t/y]/x], Δ
* </pre>
*/
case RightBeta(b, t1, phi, lambda, t, x) =>
val Lambda(y, e) = lambda
if (phi.sort != Formula)
SCInvalidProof(SCProof(step), Nil, "φ must be a formula, but it is a " + phi.sort)
else if (y.sort != t.sort)
SCInvalidProof(SCProof(step), Nil, "t must have the same type as y, but they are " + t.sort + " and " + y.sort)
else if (e.sort != x.sort)
SCInvalidProof(SCProof(step), Nil, "e must have the same type as x, but they are " + e.sort + " and " + x.sort)
else if (isSameSet(b.left, ref(t1).left)) {
val redex = lambda(t)
val normalized = substituteVariables(e, Map(y -> t))
val phi_redex = substituteVariables(phi, Map(x -> redex))
val phi_normalized = substituteVariables(phi, Map(x -> normalized))
if (isSameSet(b.right + phi_redex, ref(t1).right + phi_normalized) || isSameSet(b.right + phi_normalized, ref(t1).right + phi_redex))
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Right-hand side of the conclusion + φ[(λy. e)t/x] must be the same as right-hand side of the premise + φ[e[t/y]/x] (or the opposite)")
} else SCInvalidProof(SCProof(step), Nil, "Left-hand sides or conclusion and premise must be the same.")


/**
* <pre>
* Γ, φ[(λy. e)t/x] |- Δ
* ---------------------------
* Γ, φ[e[t/y]/x] |- Δ
* </pre>
*/
case LeftBeta(b, t1, phi, lambda, t, x) =>
val Lambda(y, e) = lambda
if (phi.sort != Formula)
SCInvalidProof(SCProof(step), Nil, "φ must be a formula, but it is a " + phi.sort)
else if (y.sort != t.sort)
SCInvalidProof(SCProof(step), Nil, "t must have the same type as y, but they are " + t.sort + " and " + y.sort)
else if (e.sort != x.sort)
SCInvalidProof(SCProof(step), Nil, "e must have the same type as x, but they are " + e.sort + " and " + x.sort)
else if (isSameSet(b.right, ref(t1).right)) {
val redex = lambda(t)
val normalized = substituteVariables(e, Map(y -> t))
val phi_redex = substituteVariables(phi, Map(x -> redex))
val phi_normalized = substituteVariables(phi, Map(x -> normalized))
if (isSameSet(b.left + phi_redex, ref(t1).left + phi_normalized) || isSameSet(b.left + phi_normalized, ref(t1).left + phi_redex))
SCValidProof(SCProof(step))
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of the conclusion + φ[(λy. e)t/x] must be the same as left-hand side of the premise + φ[e[t/y]/x] (or the opposite)")
} else SCInvalidProof(SCProof(step), Nil, "Right-hand sides or conclusion and premise must be the same.")

case Beta(b, t1) =>
if (isSame(betaReduce(sequentToFormula(b)), betaReduce(sequentToFormula(ref(t1))))) {
SCValidProof(SCProof(step))
} else SCInvalidProof(SCProof(step), Nil, "The conclusion is not beta-OL-equivalent to the premise.")

// Equality Rules
/*
Expand Down Expand Up @@ -510,9 +469,9 @@ object SCProofChecker {
SCInvalidProof(SCProof(step), Nil, "The variable x1...xn must not be free in the second premise other than as parameters of the equality.")
} else SCValidProof(SCProof(step))
}
else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_).")
else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the conclusion + φ(s) must be the same as left-hand side of the premises + φ(t).")
}
else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premises must be the same as the right-hand side of the conclusion + s=t.")
}

/*
Expand Down Expand Up @@ -591,9 +550,9 @@ object SCProofChecker {
SCInvalidProof(SCProof(step), Nil, "The variable x1...xn must not be free in the second premise other than as parameters of the equality.")
} else SCValidProof(SCProof(step))
}
else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_).")
else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the conclusion the same as the left-hand sides of the premises.")
}
else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premises + φ(t) must be the same as right-hand sides of the premises + φ(s) + s=t.")
}


Expand Down
18 changes: 5 additions & 13 deletions lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,17 +257,9 @@ object SequentCalculus {
* Γ |- φ[e[t/y]/x], Δ
* </pre>
*/
case class LeftBeta(bot: Sequent, t1: Int, phi: Expression, lambda: Lambda, t: Expression, x: Variable) extends SCProofStep { val premises = Seq(t1) }
case class Beta(bot: Sequent, t1: Int) extends SCProofStep { val premises = Seq(t1) }


/**
* <pre>
* Γ, φ[(λy. e)t/x] |- Δ
* ---------------------------
* Γ, φ[e[t/y]/x] |- Δ
* </pre>
*/
case class RightBeta(bot: Sequent, t1: Int, phi: Expression, lambda: Lambda, t: Expression, x: Variable) extends SCProofStep { val premises = Seq(t1) }

// Equality Rules
/**
Expand Down Expand Up @@ -297,7 +289,7 @@ object SequentCalculus {
* equals elements must have type ... -> ... -> Term
*/
//case class LeftSubstEq(bot: Sequent, t1: Int, equals: List[(LambdaTermTerm, LambdaTermTerm)], lambdaPhi: (Seq[SchematicTermLabel], Formula)) extends SCProofStep { val premises = Seq(t1) }
case class LeftSubstEq(bot: Sequent, t1: Int, t2: Int, s: Expression, t: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1) }
case class LeftSubstEq(bot: Sequent, t1: Int, t2: Int, s: Expression, t: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1, t2) }

/**
* <pre>
Expand All @@ -307,7 +299,7 @@ object SequentCalculus {
* </pre>
* equals elements must have type ... -> ... -> Term
*/
case class RightSubstEq(bot: Sequent, t1: Int, t2: Int, s: Expression, t: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1) }
case class RightSubstEq(bot: Sequent, t1: Int, t2: Int, s: Expression, t: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1, t2) }

/**
* <pre>
Expand All @@ -317,7 +309,7 @@ object SequentCalculus {
* </pre>
* equals elements must have type ... -> ... -> Formula
*/
case class LeftSubstIff(bot: Sequent, t1: Int, t2: Int, psi: Expression, tau: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1) }
case class LeftSubstIff(bot: Sequent, t1: Int, t2: Int, psi: Expression, tau: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1, t2) }

/**
* <pre>
Expand All @@ -327,7 +319,7 @@ object SequentCalculus {
* </pre>
* equals elements must have type ... -> ... -> Formula
*/
case class RightSubstIff(bot: Sequent, t1: Int, t2: Int, psi: Expression, tau: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1) }
case class RightSubstIff(bot: Sequent, t1: Int, t2: Int, psi: Expression, tau: Expression, vars: Seq[Variable], lambdaPhi: (Variable, Expression)) extends SCProofStep { val premises = Seq(t1, t2) }

// Rule for schemas

Expand Down
30 changes: 12 additions & 18 deletions lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ object KernelHelpers {
/* Prefix syntax */

extension (s: Sort) {
def >>:(t: Sort) : Sort = Arrow(t, s)
def >>:(t: Sort) : Sort = Arrow(s, t)
}

val Equality = equality
Expand Down Expand Up @@ -52,12 +52,13 @@ object KernelHelpers {
val ε = epsilon



extension (binder: forall.type) {
@targetName("forallApply")
def apply(bound: Variable, inner: Expression): Expression = binder(Lambda(bound, inner))
@targetName("forallUnapply")
def unapply(e: Expression): Option[(Variable, Expression)] = e match {
case Application(forall, Lambda(x, inner)) => Some((x, inner))
case Application(`forall`, Lambda(x, inner)) => Some((x, inner))
case _ => None
}
}
Expand All @@ -66,7 +67,7 @@ object KernelHelpers {
def apply(bound: Variable, inner: Expression): Expression = binder(Lambda(bound, inner))
@targetName("existsUnapply")
def unapply(e: Expression): Option[(Variable, Expression)] = e match {
case Application(exists, Lambda(x, inner)) => Some((x, inner))
case Application(`exists`, Lambda(x, inner)) => Some((x, inner))
case _ => None
}
}
Expand All @@ -75,7 +76,7 @@ object KernelHelpers {
def apply(bound: Variable, inner: Expression): Expression = binder(Lambda(bound, inner))
@targetName("epsilonUnapply")
def unapply(e: Expression): Option[(Variable, Expression)] = e match {
case Application(epsilon, Lambda(x, inner)) => Some((x, inner))
case Application(`epsilon`, Lambda(x, inner)) => Some((x, inner))
case _ => None
}
}
Expand Down Expand Up @@ -204,18 +205,6 @@ object KernelHelpers {
def fullRepr: String = s"${s.left.map(_.fullRepr).mkString(", ")} |- ${s.right.map(_.fullRepr).mkString(", ")}"
}

def betaReduce(e: Expression): Expression = e match {
case Application(f, arg) =>
val f1 = betaReduce(f)
val a2 = betaReduce(arg)
f1 match
case Lambda(v, body) => betaReduce(substituteVariables(body, Map(v -> a2)))
case _ => Application(f1, betaReduce(a2))
case Lambda(v, inner) =>
Lambda(v, betaReduce(inner))
case _ => e
}

/**
* Represents a converter of some object into a set.
* @tparam S The type of elements in that set
Expand Down Expand Up @@ -497,6 +486,12 @@ object KernelHelpers {
}
}


extension (judg: SCProofCheckerJudgement) {
def repr: String = prettySCProof(judg)
}


/**
* output a readable representation of a proof.
*/
Expand Down Expand Up @@ -606,8 +601,7 @@ object KernelHelpers {
case LeftImplies(_, t1, t2, _, _) => pretty("Left ⇒", t1, t2)
case LeftIff(_, t1, _, _) => pretty("Left ⇔", t1)
case Weakening(_, t1) => pretty("Weakening", t1)
case LeftBeta(_, t1, _, _, _, _) => pretty("Left β", t1)
case RightBeta(_, t1, _, _, _, _) => pretty("Right β", t1)
case Beta(_, t1) => pretty("Beta", t1)
case LeftRefl(_, t1, _) => pretty("L. Refl", t1)
case RightRefl(_, _) => pretty("R. Refl")
case LeftSubstEq(_, t1, t2, _, _, _, _) => pretty("L. SubstEq", t1, t2)
Expand Down
Loading

0 comments on commit 6e06964

Please sign in to comment.