New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Substitution tactic crashes when assumptions are not complete #215

Open

SimonGuilloud opened this issue Mar 4, 2024 · 0 comments

Collaborator

SimonGuilloud commented Mar 4, 2024

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.

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment