Certain tactics and steps rely on external imports, but these operations will not produce sequents with assumptions. Consider for example:
// over yonder
val ab = have(A |- B) by Magic
val bc = have(B |- C) by Magic
// new running proof
assume(D)
have(A |- C) by Cut(ab, bc)
// internally this becomes:
// have({D, A} |- C) by Cut(ab, bc)
// which obviously fails :(
This was found in the case of instantiating definitions, where a definition cannot be instantiated in the presence of assumptions as it is a weakened sequent.
Solutions:
make all tactics allow weakened premises. This could sometimes have counterintuitive results (but I will have to work to find a good example).
handle assumption tracking more carefully. This brings a lot of complexity to the system, and may be detrimental to predictability.
Is this a bug? Should I mark it as such? I think it is :thinking:
Certain tactics and steps rely on external imports, but these operations will not produce sequents with assumptions. Consider for example:
This was found in the case of instantiating definitions, where a definition cannot be instantiated in the presence of assumptions as it is a weakened sequent.
Solutions:
Is this a bug? Should I mark it as such? I think it is :thinking: