Inconsistent behaviour with table and def

[ghost]

I want to change the definitions of allDeMorgan and existsDeMorgan from CNFTheorems.thy so that their results are memoized. However, the code mysteriously breaks if I replace def with table. See the metis branch.

[phlegmaticprogrammer]

What kind of exception do you get? You cannot memoize everything, for example theorems cannot be memoized, but terms can (by that I mean the arguments to the function, obviously).

[ghost]

The exception isn't helpful. It's just comb getting applied to the wrong arguments.

I thought the whole point of introducing "table" was so that skolem theorems didn't have to reproven per type. I was memoising those theorems.

[phlegmaticprogrammer]

I'll check it out. You can memoise any result of a function call, no problem, but the arguments of a function must be of a type which can be compared. So the argument of a table function cannot be a theorem, but the result can.

[ghost]

In this case, the arguments to the function are types. The result is a theorem. But I'm getting inconsistent behaviour.

[phlegmaticprogrammer]

[error] /Users/stevenobua/myrepos/proofpeer-proofscript/src/main/scala/proofpeer/proofscript/automation/Automation.scala:173: value top is not a member of List[Int] [error] proofscriptOfLiteral(cursor.top)) ++ [error] ^ [error] /Users/stevenobua/myrepos/proofpeer-proofscript/src/main/scala/proofpeer/proofscript/automation/Automation.scala:174: value path is not a member of List[Int] [error] cursor.path.toSeq.map(n => IntValue(BigInt(n))): _*) [error] ^ [error] /Users/stevenobua/myrepos/proofpeer-proofscript/src/main/scala/proofpeer/proofscript/automation/Automation.scala:187: wrong number of arguments for pattern kernel.Resolve[Any,Any,Any](pos: kernel.Thm,neg: kernel.Thm) [error] case kernel.Resolve(atm,pos,neg) => [error] ^ [error] three errors found error Compilation failed

[phlegmaticprogrammer]

I got above errors when trying to compile proofscript with branch metis ?

[ghost]

Try switching to the "movable" branch of proofpeer-metis and republishing.

[phlegmaticprogrammer]

So just to recap our offline discussion, the problem seems to be that table memoizes the theorem in the context in which it is first called, and later on, when called from a different context, the theorem is lifted into that context. Thats pretty unintuitive.

[phlegmaticprogrammer]

I have hacked your script in the following way:

val here = context

table existsDeMorgan ty =
  context<here>
    theorem t: '∀P. (¬(∃x:‹ty›. P x)) = (∀x. ¬(P x))'
      val x = fresh "x"
      val P = fresh "P"
      let '‹P› : ‹ty› → ℙ'
      theorem left: '(¬(∃x:‹ty›. ‹P› x)) → (∀x. ¬(‹P› x))'
        assume asm:'¬(∃x:‹ty›. ‹P› x)'
        let '‹x›:‹ty›'
        theorem notPx:
          assume px:'‹P› ‹x›'
          theorem pExists:
            val y = fresh "y"
            val asm = let '‹y› = ‹x›'
            convRule (onceTreeConv (rewrConv1 (sym asm)), px)
          modusponens (pExists, matchmp (notDefEx, asm))
        matchmp (impliesNot, notPx)
      theorem right:
        assume asm:'∀x:‹ty›. ¬(‹P› x)'
        theorem notExP:
          assume exP:'∃x:‹ty›. ‹P› x'
          val px = choose '‹x›:‹ty›' exP
          matchmp (notDefEx, instantiate (asm,'‹x›'), px)
        matchmp (impliesNot, notExP)
      equivalence (left,right)
    return t

table allDeMorgan ty =
  context<here>
    theorem t: '∀P. (¬(∀x:‹ty›. P x)) = (∃x. ¬(P x))'
      val P = fresh "P"
      let '‹P› : ‹ty› → ℙ'
      val existsDeMorganInst =
        instantiate(existsDeMorgan ty,'x ↦ ¬(‹P› x)')
      seqConv [randConv (randConv (absConv (rewrConv1 (gsym negInvolve)))),
               onceTreeConv (rewrConv1 (gsym existsDeMorganInst)),
               rewrConv [negInvolve]] '¬(∀x. ‹P› x)'
    return t

That leads to the following error:

start compiling theory '\bootstrap\metis' ...
Going through METIS
Interpreted clauses
  no output
failed compiling theory '\bootstrap\metis':
  * Assertion does not hold
    in scripts/bootstrap/metis.thy at row 289, column 7
    in scripts/bootstrap/metis.thy at row 288, column 8 (ic applied to: ["axiom", {[true, ['elementof', ['x_3', 0, 1], 1]], [true, ['elementof', ['x_3', 0, 1], 0]], [true, ['equals : (𝒰 → 𝒰 → ℙ) → (𝒰 → 𝒰 → ℙ) → ℙ', 0, 1]]}])

But this seems ok, because it is the error that you get previously with using def instead of table, I think?

[phlegmaticprogrammer]

If the above hack does what you want, then it might make sense to think about how to add language features that deal with this phenomenon, for example:

• one could add syntax for making it easier to say in what context tables and defs are defined, like def<ctx> ... and table<ctx> where <ctx> would be evaluated at definition time, not at call time. The syntax def<?> and table<?> could be used to explicitly say that the current dynamic context should be used, and the syntax def can then be short for def<?> and table could be short for table<context>.
• more simply, we change only the semantics of table for now, so that table means table<context> without actually introducing the general <...> construct for defs and tables
• ... ?

[phlegmaticprogrammer]

So I think for now I will just do the following: just as you can postfix context which <...> to specify in which context it is executed, so you can postfix def and table. That means in the use case that started this issue, the definition of for example existsDeMorgan would be changed as follows:

table<context> existsDeMorgan ty = ...

[phlegmaticprogrammer]

That is part of master now.