Lifting

[ghost]

As I understand, universal quantifiers whose bound variable is unused in the body of a theorem are, by default, dropped by lifting. This doesn't appear to generally be the case with existentials. Am I right here, and is there a good reason for the difference?

For instance, I'm trying to prove

theorem right: '(∃f. ∀x. ‹p› x (f x)) → (∀x. ∃y. ‹p› x y)'
  assume asm:'∃f. ∀x. ‹p› x (f x)'
  let x:'‹fresh "x"›: ‹b›'
  choose ch:'‹fresh "f"›' asm
  val fx = rand (instantiate (ch,x): Term)
  let ydef:'y = ‹fx›'
  convRule (randConv (subsConv (gsym ydef)), instantiate (ch,x))

The final line yields the theorem ‹p› x y, but the lifted theorem isn't matched, since it contains ∃f. ... in the consequent. I seem to be able to fix this easily enough by writing:

theorem right: '(∃f. ∀x. ‹p› x (f x)) → (∀x. ∃y. ‹p› x y)'
  assume asm:'∃f. ∀x. ‹p› x (f x)'
  let x:'‹fresh "x"›: ‹b›'  
  theorem '∃y. ‹p› x y'
    choose ch:'‹fresh "f"›' asm
    val fx = rand (instantiate (ch,x): Term)
    let ydef:'y = ‹fx›'
    convRule (randConv (subsConv (gsym ydef)), instantiate (ch,x))

This behaviour looks odd to me, though. Why is the existential dropped here but not in the original?

[phlegmaticprogrammer]

There are only two modes of lifting currently: structure preserving and smart. In structure preserving mode, nothing is simplified or thrown away, in smart mode prenex normal form is maintained and superfluous quantifiers are thrown away.

This is reflected in the error message you get, neither the structure preserving lifting nor the smart lifting results in the theorem you stated.

Now, when you introduced the intermediate theorem in the second version, you made it possible to do smart lifting for the second part and structured lifting for the first part.

Maybe it would be nice to have a way of stating which theorem you are currently proving without introducing a nested theorem block, for example like this:

theorem right: '(∃f. ∀x. ‹p› x (f x)) → (∀x. ∃y. ‹p› x y)'
  assume asm:'∃f. ∀x. ‹p› x (f x)'
  let x:'‹fresh "x"›: ‹b›'
  goal '∃y. ‹p› x y'
  choose ch:'‹fresh "f"›' asm
  val fx = rand (instantiate (ch,x): Term)
  let ydef:'y = ‹fx›'
  convRule (randConv (subsConv (gsym ydef)), instantiate (ch,x))

Using such intermediate goals would probably also improve the readability of the proof.