Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol

lisa-sets2/src/main/scala/lisa/automation/Substitution.scala

@@ -206,14 +206,14 @@ object Substitution:
             // rewrite to destruct sequent
             thenHave(postLeft ++ leftFormulas ++ rightFormulas |- postRight) by Restate
 
-            val dpremise = lastStep.bot
+            val postRewriteSequent = lastStep.bot
 
             // discharge assumptions
-            discharges.foldLeft(dpremise):
+            discharges.foldLeft(postRewriteSequent):
               case (premise, (rule, source)) =>
                 val sseq = proof.getSequent(source)
                 val form = rule.toFormula
-                val nextSequent = premise.left - form ++ sseq.left |- premise.right ++ sseq.right - form
+                val nextSequent = premise.left.filterNot(isSame(_, form)) ++ sseq.left |- premise.right ++ sseq.right.filterNot(isSame(_, form))
                 have(nextSequent) by Cut.withParameters(form)(source, lastStep)
                 nextSequent
 

lisa-sets2/src/main/scala/lisa/maths/Quantifiers.scala

@@ -6,6 +6,7 @@ import lisa.utils.K.repr
 import lisa.automation.atp.Goeland
 import lisa.utils.prooflib.Library
 import lisa.utils.Printing
+import lisa.utils.prooflib.ProofTacticLib.ProofFactSequentTactic
 
 /**
  * Implements theorems about first-order logic.
@@ -289,44 +290,46 @@ object Quantifiers extends lisa.Main {
    *  Γ ⊢ ∀x.∀y. ... ∀z. φ, Δ
    * </pre>
    */
-  def quantifyAll(using lib: Library, proof: lib.Proof)(premiseStep: proof.Fact)(conclusion: Sequent) =
-    def isQuantifiedOf(target: Expr[Formula], pivot: Expr[Formula], vars: List[Variable[Term]] = Nil): Option[List[Variable[Term]]] =
-      target match
-        case ∀(x, inner) =>
-          if isSame(inner, pivot) then Some(vars) else isQuantifiedOf(inner, pivot, x :: vars)
-        case _ => None
-    val premise = proof.getSequent(premiseStep)
-    val difference = premise.right -- conclusion.right
-
-    if difference.isEmpty then Restate(using lib, proof)(premiseStep)(conclusion)
-    else if difference.size > 1 then proof.InvalidProofTactic(s"There must be only one formula to quantify over between the premise and the conclusion. Found: \n${Printing.printList(difference)}")
-    else
-      val rdifference = conclusion.right -- premise.right
-      if rdifference.size != 1 then proof.InvalidProofTactic(s"There must be only one formula to quantify over between the premise and the conclusion. Found: \n${Printing.printList(rdifference)}")
+  object quantifyAll extends ProofFactSequentTactic:
+    def apply(using lib: Library, proof: lib.Proof)(premiseStep: proof.Fact)(conclusion: Sequent) =
+      def isQuantifiedOf(target: Expr[Formula], pivot: Expr[Formula], vars: List[Variable[Term]] = Nil): Option[List[Variable[Term]]] =
+        target match
+          case ∀(x, inner) =>
+            val next = x :: vars
+            if isSame(inner, pivot) then Some(next) else isQuantifiedOf(inner, pivot, next)
+          case _ => None
+      val premise = proof.getSequent(premiseStep)
+      val difference = premise.right -- conclusion.right
+
+      if difference.isEmpty then Restate(using lib, proof)(premiseStep)(conclusion)
+      else if difference.size > 1 then proof.InvalidProofTactic(s"There must be only one formula to quantify over between the premise and the conclusion. Found: \n${Printing.printList(difference)}")
       else
-        val pivot = difference.head
-        val target = rdifference.head
-        val varsOption = isQuantifiedOf(target, pivot)
-
-        if varsOption.isEmpty then proof.InvalidProofTactic("Could not find a formula to quantify over in the conclusion.")
+        val rdifference = conclusion.right -- premise.right
+        if rdifference.size != 1 then proof.InvalidProofTactic(s"There must be only one formula to quantify over between the premise and the conclusion. Found: \n${Printing.printList(rdifference)}")
         else
-          val vars = varsOption.get
-          val conflicts = vars.toSet -- premise.left.flatMap(_.freeVars)
+          val pivot = difference.head
+          val target = rdifference.head
+          val varsOption = isQuantifiedOf(target, pivot)
 
-          if conflicts.nonEmpty then proof.InvalidProofTactic(s"Variables ${conflicts.mkString(", ")} to be quantified appear in the LHS of the conclusion.")
+          if varsOption.isEmpty then proof.InvalidProofTactic("Could not find a formula to quantify over in the conclusion.")
           else
-            // safe, proceed
-            TacticSubproof:
-              val vars = varsOption.get
-              lib.have(premise) by Restate.from(premiseStep)
+            val vars = varsOption.get
+            val conflicts = vars.toSet `intersect` premise.left.flatMap(_.freeVars)
+
+            if conflicts.nonEmpty then proof.InvalidProofTactic(s"Variable(s) ${conflicts.mkString(", ")} to be quantified appear in the LHS of the conclusion.")
+            else
+              // safe, proceed
+              TacticSubproof:
+                val vars = varsOption.get
+                lib.have(premise) by Restate.from(premiseStep)
 
-              val base = premise ->> pivot
+                val base = premise ->> pivot
 
-              vars.foldLeft(pivot): (pivot, v) =>
-                val quant = ∀(v, pivot)
-                lib.thenHave(base +>> quant) by RightForall.withParameters(pivot, v)
-                quant
+                vars.foldLeft(pivot): (pivot, v) =>
+                  val quant = ∀(v, pivot)
+                  lib.thenHave(base +>> quant) by RightForall.withParameters(pivot, v)
+                  quant
 
-              lib.thenHave(conclusion) by Restate
+                lib.thenHave(conclusion) by Restate
 
 }

lisa-sets2/src/main/scala/lisa/maths/settheory/Comprehension.scala

@@ -24,8 +24,8 @@ object Comprehension extends lisa.Main:
   val definition: THM = Theorem(∀(x, x ∈ s.filter(φ) <=> (x ∈ s /\ φ(x)))):
     have(∀(x, x ∈ y <=> (x ∈ s /\ φ(x))) |- ∀(x, x ∈ y <=> (x ∈ s /\ φ(x)))) by Hypothesis
     thenHave(∀(x, x ∈ y <=> (x ∈ s /\ φ(x))) |- ∀(x, x ∈ ε(t, ∀(x, x ∈ t <=> (x ∈ s /\ φ(x)))) <=> (x ∈ s /\ φ(x)))) by RightEpsilon
-    thenHave(∀(x, x ∈ y <=> (x ∈ s /\ φ(x))) |- ∀(x, x ∈ s.filter(φ) <=> (x ∈ s /\ φ(x)))) by Substitution.Apply(filter.definition)
+    thenHave(∀(x, x ∈ y <=> (x ∈ s /\ φ(x))) |- ∀(x, x ∈ s.filter(φ) <=> (x ∈ s /\ φ(x)))) by Substitution.Apply(filter.definition of (t := s))
     thenHave(∃(y, ∀(x, x ∈ y <=> (x ∈ s /\ φ(x)))) |- ∀(x, x ∈ s.filter(φ) <=> (x ∈ s /\ φ(x)))) by LeftExists
-    have(thesis) by Cut(existence, lastStep)
+    have(thesis) by Cut.withParameters(∃(t, ∀(x, (x ∈ t) <=> (x ∈ s /\ φ(x)))))(existence of (t := s), lastStep)
 
 end Comprehension

lisa-sets2/src/main/scala/lisa/maths/settheory/Equality.scala

@@ -8,6 +8,6 @@ object Equality extends lisa.Main:
 
   val transitivity = Theorem((x === y, y === z) |- (x === z)):
     have((x === y, y === z) |- (x === y)) by Hypothesis
-    thenHave(thesis) by InstSchema(y := z)
+    thenHave(thesis) by RightSubstEq.withParameters(Seq(y -> z), Seq(y) -> (x === y))
 
 end Equality

lisa-sets2/src/main/scala/lisa/maths/settheory/Replacement.scala

@@ -11,10 +11,11 @@ object Replacement extends lisa.Main:
   val t = variable[Term]
   val s = variable[Term]
   val A = variable[Term]
+  val B = variable[Term]
   val f = variable[Term >>: Term]
   val P = variable[Term >>: Term >>: Formula]
 
-  val map = DEF(lambda(t, lambda(f, ε(s, ∀(x, (x ∈ s) <=> ∃(y, y ∈ t /\ (y === f(x))))))))
+  val map = DEF(lambda(t, lambda(f, ε(s, ∀(y, (y ∈ s) <=> ∃(x, x ∈ t /\ (y === f(x))))))))
 
   private val replacement: map.type = map
 
@@ -26,9 +27,9 @@ object Replacement extends lisa.Main:
    * The existence of the image of a set under a function. Or, the functional
    * form of the replacement schema.
    */
-  val existence = Theorem(∃(s, ∀(x, (x ∈ s) <=> ∃(y, y ∈ t /\ (y === f(x)))))):
+  val existence = Theorem(∃(s, ∀(y, (y ∈ s) <=> ∃(x, x ∈ t /\ (y === f(x)))))):
     val inst = replacementSchema of (A := t, P := lambda(x, lambda(y, y === f(x))))
-    val conditional = have(∀(x, x ∈ t ==> ∀(y, ∀(z, ((y === f(x)) /\ (z === f(x))) ==> (y === z)))) |- ∃(s, ∀(x, (x ∈ s) <=> ∃(y, y ∈ t /\ (y === f(x)))))) by Weakening(inst)
+    val conditional = have(∀(x, x ∈ t ==> ∀(y, ∀(z, ((y === f(x)) /\ (z === f(x))) ==> (y === z)))) |- ∃(s, ∀(y, (y ∈ s) <=> ∃(x, x ∈ t /\ (y === f(x)))))) by Weakening(inst)
 
     val eqTautology =
       have(((y === f(x)) /\ (z === f(x))) ==> (y === z)) by Weakening(Equality.transitivity of (x := y, y := f(x), z := z))
@@ -44,12 +45,12 @@ object Replacement extends lisa.Main:
    *
    * `∀(x, x ∈ s.map(f) <=> ∃(y, y ∈ s /\ x === f(y)))`
    */
-  val definition: THM = Theorem(∀(x, x ∈ s.map(f) <=> ∃(y, y ∈ s /\ (x === f(y))))):
-    have(∀(x, x ∈ y <=> ∃(y, y ∈ s /\ (x === f(y)))) |- ∀(x, x ∈ y <=> ∃(y, y ∈ s /\ (x === f(y))))) by Hypothesis
-    thenHave(∀(x, x ∈ y <=> ∃(y, y ∈ s /\ (x === f(y)))) |- ∀(x, x ∈ ε(t, ∀(x, x ∈ t <=> ∃(y, y ∈ s /\ (x === f(y))))) <=> ∃(y, y ∈ s /\ (x === f(y))))) by RightEpsilon
-    thenHave(∀(x, x ∈ y <=> ∃(y, y ∈ s /\ (x === f(y)))) |- ∀(x, x ∈ s.map(f) <=> ∃(y, y ∈ s /\ (x === f(y))))) by Substitution.Apply(map.definition)
-    thenHave(∃(y, ∀(x, x ∈ y <=> ∃(y, y ∈ s /\ (x === f(y))))) |- ∀(x, x ∈ s.map(f) <=> ∃(y, y ∈ s /\ (x === f(y))))) by LeftExists
-    have(thesis) by Cut(existence, lastStep)
+  val definition: THM = Theorem(∀(y, y ∈ s.map(f) <=> ∃(x, x ∈ s /\ (y === f(x))))):
+    have(∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x)))) |-     ∀(y, y ∈ t                                                 <=> ∃(x, x ∈ s /\ (y === f(x))))) by Hypothesis
+    thenHave(∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x)))) |- ∀(y, y ∈ ε(t, ∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x))))) <=> ∃(x, x ∈ s /\ (y === f(x))))) by RightEpsilon.withParameters(∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x)))), t, t)
+    thenHave(∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x)))) |- ∀(y, y ∈ s.map(f) <=> ∃(x, x ∈ s /\ (y === f(x))))) by Substitution.Apply(map.definition of (t := s))
+    thenHave(∃(t, ∀(y, y ∈ t <=> ∃(x, x ∈ s /\ (y === f(x))))) |- ∀(y, y ∈ s.map(f) <=> ∃(x, x ∈ s /\ (y === f(x))))) by LeftExists
+    have(thesis) by Cut(existence of (t := s), lastStep)
 
   /**
    * The replacement property of a [[map]]ped set.

lisa-utils/src/main/scala/lisa/utils/fol/Syntax.scala

@@ -9,6 +9,7 @@ import scala.annotation.nowarn
 import scala.annotation.showAsInfix
 import scala.annotation.targetName
 import scala.util.Sorting
+import lisa.utils.KernelHelpers.freshId
 
 trait Syntax {
 
@@ -178,6 +179,7 @@ trait Syntax {
 
   object Variable {
     def unsafe(id: String, sort: K.Sort): Variable[?] = Variable(id)(using unsafeSortEvidence(sort))
+    def unsafe(id: Identifier, sort: K.Sort): Variable[?] = Variable(id)(using unsafeSortEvidence(sort))
   }
 
 
@@ -273,7 +275,14 @@ trait Syntax {
   case class Abs[T1, T2](v: Variable[T1], body: Expr[T2]) extends Expr[Arrow[T1, T2]] {
     val sort: K.Sort = K.Arrow(v.sort, body.sort)
     val underlying: K.Lambda = K.Lambda(v.underlying, body.underlying)
-    def substituteUnsafe(m: Map[Variable[?], Expr[?]]): Abs[T1, T2] = Abs(v, body.substituteUnsafe(m - v))
+    def substituteUnsafe(m: Map[Variable[?], Expr[?]]): Abs[T1, T2] = 
+      lazy val frees = m.values.flatMap(_.freeVars).toSet
+      if m.keySet.contains(v) || frees.contains(v) then
+        // rename
+        val v1: Variable[T1] = Variable.unsafe(freshId(frees.map(_.id), v.id), v.sort).asInstanceOf
+        new Abs(v1, body.substituteUnsafe(Map(v -> v1))).substituteUnsafe(m)
+      else
+        new Abs(v, body.substituteUnsafe(m))
     override def substituteWithCheck(m: Map[Variable[?], Expr[?]]): Abs[T1, T2] =
       super.substituteWithCheck(m).asInstanceOf[Abs[T1, T2]]
     override def substitute(pairs: SubstPair*): Abs[T1, T2] = 

lisa-utils/src/main/scala/lisa/utils/prooflib/BasicStepTactic.scala

@@ -1000,7 +1000,7 @@ object BasicStepTactic {
    * </pre>
    *
    * Note that if Δ contains φ[(εx. φ)/x] as well, the parameter inference will
-   * fail. Use [[RightEpsilon.withParameters]] instead.
+   * fail. In that case, use [[RightEpsilon.withParameters]] instead.
    */
   object RightEpsilon extends ProofTactic with ProofFactSequentTactic {
     def collectEpsilons(in: F.Expr[?]): Set[F.Expr[F.Term]] = 
@@ -1042,7 +1042,6 @@ object BasicStepTactic {
 
         val newBindingOption = epsilons.collectFirstDefined: 
           case eps @ F.ε(x, phi) =>
-            val asTerm = (eps : F.Expr[F.Term])
             val substituted = phi.substitute(x := eps) 
             if F.isSame(substituted, target) then Some(eps) else None
           case _ => None