search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Substitution tactic crashes when assumptions are not complete #215

Open SimonGuilloud opened 7 months ago

SimonGuilloud commented 7 months ago 
  val f = function[1]
  val x = variable
  val y = variable
  val P = formulaVariable
  val Q = predicate[1]
  val thm6 = Theorem(() |- ()) {
    val s1 = have (P |- (f(x) === f(y)) ) by Sorry
    assume(Q(f(x)))
    thenHave( Q(f(y)) ) by Substitution.ApplyRules(s1)

yields

8 Cut                      ( ∧(Q(f(x))), Q(f(x)), P ) ⊢ ∨(Q(f(y)))
[info]     lib.thenHave(bot) by BasicStepTactic.Weakening
[info]    Proof tactic Weakening used in.(Substitution.scala:402) did not succeed:
[info]    Conclusion cannot be trivially derived from premise.