Discrepancy getting quantified theorems from contexts

[ghost]

The first proof works, but the second does not. Any ideas why?

theory Foo
extends root

theorem '∀x. x = x'
  val (ctx,x,_) = destabs 'x ↦ x'
  val foo
  context <ctx>
    foo = reflexive x
  foo

theorem '∀x. ⊤ = ⊤'
  val (ctx,x,_) = destabs 'x ↦ ⊤'
  val foo
  context <ctx>
    foo = reflexive '⊤'
  foo

[phlegmaticprogrammer]

Yes. In both cases foo at the end of the respective proofs gets lifted into the current context. In the second proof, the result of that lifting is ⊤ = ⊤ which does not match the theorem you want to prove. In the first case, the result of the lift is '∀x. x = x', which does match. Does that help?

[phlegmaticprogrammer]

I have introduced a new lift function which allows to call lifting explicitly and optionally pass the second parameter preserve_structure which decides about the nature of the lifting. In the above, you can replace the final foo with lift(foo, true) and the proof goes through. As it stands, just writing foo is the same as lift foo which is the same as lift(foo, false).

[ghost]

Hopefully the new lift function is all I need. Otherwise, I don't think I can get my abstraction conversion to work robustly.

[phlegmaticprogrammer]

I would be interested to see if you really need to use the lift function for that. If you do, maybe it would make sense to make lift(thm, true) the standard lift instead of lift(thm, false). What do you think would be a better default?

[phlegmaticprogrammer]

I just made a quick experiment and changed the default for lift from lift(, false) to lift(, true) and everything still works fine. But note that in your match example, the resulting theorem is now

'∀ x_2 : ℙ. ∀ x_1 : ℙ. ∀ x : ℙ. (y ∧ x_1) ∧ (P z)'

instead of

'∀ x. y ∧ x ∧ P z'

[ghost]

Hmm...I'm not sure I want that.

Without the new lift, I don't know how to do the abstraction conversion correctly. The problem is that I want to be able to convert things like

(x ↦ ⊤ ∨ ⊤)

to

(x ↦ ⊤)

My code, as it is, won't do this.

[phlegmaticprogrammer]

Ok, I'll leave everything as it is, and I think in general the rule is to use lift as sparsely as possible

[ghost]

Okay, I've still got issues, but maybe there's a subtle bug in my own code that's causing me to misunderstand the interactions here.

theory Bugs
extends root Conversions

context
  show absConv (tm => [reflexive tm]) 'x ↦ ⊤'

context
  show absConv idConv 'x ↦ ⊤'

context
  show absConv (subsConv [reflexive '⊤']) 'x ↦ ⊤'

The first two work as expected. In the third one, I lose the quantifier in the body of absConv, and again, cannot call abstract.

[ghost]

Guess I don't need all those "contexts" btw.

[phlegmaticprogrammer]

well, I don't really know what these conversions do, so cannot really comment on that; in general, if you use lift with flag true explicitly, you will not "lose" any quantifiers. But then again, you should not rely on lifting assumptions in the first place, but explicitly state via theorem what you are trying to prove if this is possible at all; this way what lift does should actually play no role at all

[ghost]

I don't expect you to be able to debug it, but I would like to know if you think the behaviour is possible. The error occurs here:

def absConv conv =
  tm =>
    match destabs tm
      case [ctx,x,bod] =>
        val cthms
        context <ctx>
          cthms = conv bod
        for cthm in cthms do
          show (lift (cthm,true))
          abstract (lift (cthm,true))
      case _ => []

In some cases, the theorem which is passed to "show" contains no quantifier. I would expect it to always be quantifying over the x obtained from destabs. If you are sure I don't lose any quantifiers, then something smells fishy.

[phlegmaticprogrammer]

If you do conv bond, that theorem might not be in context ctx, depending on what exactly conv does. So if you want to be sure that cthms is in that context, lift it into it there explicitly.

[ghost]

After discussion, all appears to be working now.

[phlegmaticprogrammer]

Cool; by the way, could you add a couple of test cases to your code; basically, whenever you use show during experimenting, later on these shows should disappear and be replaced by asserts. That way, the more code we produce, we automatically get tests for free.

[phlegmaticprogrammer]

One last thought, when using lift like we discussed, then there is no need to use lift(thm, true); instead you can just use lift thm, as you don't care about the transformation of thm, but just that it is in the right context