ProofScript performance problem

[phlegmaticprogrammer]

Given the terms x =

(((((∀ x. ¬ (x ∈ ∅)) ∧ (one = (𝒫 ∅))) ∧ (∀ x. ∀ y. ((x ∈ (𝒫 y)) ∨ (¬ (x ⊂ y))) ∧ ((¬ (x ∈ (𝒫 y))) ∨ (x ⊂ y)))) ∧ (∀ x. ∀ y. ((x ⊂ y) ∨ (¬ (∀ z ∈ x. z ∈ y))) ∧ ((¬ (x ⊂ y)) ∨ (∀ z ∈ x. z ∈ y)))) ∧ (∀ x_4. ∀ y_1. ((x_4 = y_1) ∨ (∃ x_2. ¬ ((x_1 ↦ (x_1 ∈ x_4) = (x_1 ∈ y_1)) x_2))) ∧ ((¬ (x_4 = y_1)) ∨ (∀ z. ((z ∈ x_4) ∨ (¬ (z ∈ y_1))) ∧ ((¬ (z ∈ x_4)) ∨ (z ∈ y_1)))))) ∧ (∃ x_2. ¬ ((x_1 ↦ (x_1 ∈ one) = (x_1 = ∅)) x_2))      

and y =

∀ x_6. ∀ x_5. ∃ x_3. ∃ y. ∀ x. ((x_2 ↦ (((¬ ((x_3 ∈ x_6) = (x_3 ∈ x_5))) ∨ (x_6 = x_5)) ∧ ((((x_2 ∈ x_6) ∨ (¬ (x_2 ∈ x_5))) ∧ ((¬ (x_2 ∈ x_6)) ∨ (x_2 ∈ x_5))) ∨ (¬ (x_6 = x_5)))) ∧ (((((x_6 ∈ (𝒫 x_5)) ∨ (¬ (x_6 ⊂ x_5))) ∧ ((¬ (x_6 ∈ (𝒫 x_5))) ∨ (x_6 ⊂ x_5))) ∧ ((¬ (x_6 ∈ ∅)) ∧ (one = (𝒫 ∅)))) ∧ (((x_6 ⊂ x_5) ∨ (¬ (∀ z ∈ x_6. z ∈ x_5))) ∧ ((¬ (x_6 ⊂ x_5)) ∨ (∀ z ∈ x_6. z ∈ x_5))))) x) ∧ ((x ↦ ¬ ((y ∈ one) = (y = ∅))) x)

and t =

((((((∀ x. ¬ (x ∈ ∅)) ∧ (one = (𝒫 ∅))) ∧ (∀ x. ∀ y. ((x ∈ (𝒫 y)) ∨ (¬ (x ⊂ y))) ∧ ((¬ (x ∈ (𝒫 y))) ∨ (x ⊂ y)))) ∧ (∀ x. ∀ y. ((x ⊂ y) ∨ (¬ (∀ z ∈ x. z ∈ y))) ∧ ((¬ (x ⊂ y)) ∨ (∀ z ∈ x. z ∈ y)))) ∧ (∀ x_4. ∀ y_1. ((x_4 = y_1) ∨ (∃ x_2. ¬ ((x_1 ↦ (x_1 ∈ x_4) = (x_1 ∈ y_1)) x_2))) ∧ ((¬ (x_4 = y_1)) ∨ (∀ z. ((z ∈ x_4) ∨ (¬ (z ∈ y_1))) ∧ ((¬ (z ∈ x_4)) ∨ (z ∈ y_1)))))) ∧ (∃ x_2. ¬ ((x_1 ↦ (x_1 ∈ one) = (x_1 = ∅)) x_2))) = (∀ x_6. ∀ x_5. ∃ x_3. ∃ y. ∀ x. ((x_2 ↦ (((¬ ((x_3 ∈ x_6) = (x_3 ∈ x_5))) ∨ (x_6 = x_5)) ∧ ((((x_2 ∈ x_6) ∨ (¬ (x_2 ∈ x_5))) ∧ ((¬ (x_2 ∈ x_6)) ∨ (x_2 ∈ x_5))) ∨ (¬ (x_6 = x_5)))) ∧ (((((x_6 ∈ (𝒫 x_5)) ∨ (¬ (x_6 ⊂ x_5))) ∧ ((¬ (x_6 ∈ (𝒫 x_5))) ∨ (x_6 ⊂ x_5))) ∧ ((¬ (x_6 ∈ ∅)) ∧ (one = (𝒫 ∅)))) ∧ (((x_6 ⊂ x_5) ∨ (¬ (∀ z ∈ x_6. z ∈ x_5))) ∧ ((¬ (x_6 ⊂ x_5)) ∨ (∀ z ∈ x_6. z ∈ x_5))))) x) ∧ ((x ↦ ¬ ((y ∈ one) = (y = ∅))) x))

the code

timeit
  theorem foo:'‹x› = ‹y›'
    t
  foo

needs 455ms to execute, which seems a bit slow.

[phlegmaticprogrammer]

I have split up the timing like this:

val s 
timeit
  s = '‹x› = ‹y›'
timeit
  theorem foo: s
    th
  foo

The first timing gives 481ms, the second one 10ms, so the main problem is with the statement

  s = '‹x› = ‹y›'

The reason for this inefficiency seems clear, it is because x and y are first converted into preterms, then the preterm ‹x› = ‹y› is formed, then this preterm is converted to a term, which involves type inference for the whole preterm again.

The solution to this seems to me to add an additional constructor for preterms which wraps a term. That's going to take some work.

[phlegmaticprogrammer]

I have dealt with this particular performance problem, the first timing is now 5ms, the second one 9ms. There are plenty of other performance issues, but let's deal with those when we hit them.