Abstraction

[ghost]

In proofscript, is it currently possible to prove '∀y z. y = z → (x ↦ y) = (x ↦ z)'? The "obvious" strategy doesn't work

theorem '∀y z. y = z → (x ↦ y) = (x ↦ z)'
  let 'y'
  let 'z'
  assume asm:'y = z'
  theorem lemma:'∀x. y = z'
    asm
  lemma

because the x gets thrown out when asm is lifted out of the proof of lemma. abstract lemma

[phlegmaticprogrammer]

how about proceeding with:

theorem '∀y z. y = z → (x ↦ y) = (x ↦ z)'
  let 'y'
  let 'z'
  assume asm:'y = z'
  theorem '(x ↦ y) = (x ↦ z)'
     ....

Shouldn't that somehow work?

[ghost]

Not sure how that helps. I need to use the function abstract which takes a universally quantified theorem. I'm not sure how to get that theorem.

[phlegmaticprogrammer]

Your original idea works; in your snippet, you should actually get an error message that your proof is wrong?

theorem '∀y z. y = z → (x ↦ y) = (x ↦ z)'
  let 'y'
  let 'z'
  assume asm:'y = z'
  theorem lemma:'∀x. y = z'
    let 'x'
    asm
  abstract lemma

By the way: Can't wait until we can have these kinds on discussions in a ProofScript enabled discussion board on proofpeer.net :-)

[ghost]

I get an error message, yeah. The problem, I understand, is that when asm gets lifted out of the proof of lemma, the x is automatically thrown out because it's not used in the proof. Here's a hack that works:

theory Foo extends root

theory Foo
extends root

theorem lemma:'∀P:𝒰 → 𝒰 → 𝒰. ∀ y z. y = z → (x ↦ P x y) = (x ↦ P x z)'
  let 'P:𝒰 → 𝒰 → 𝒰'
  let 'y'
  let 'z'
  assume asm:'y = z'
  theorem lemma:'∀x. P x y = P x z'
    let 'x'
    combine (reflexive 'P x', asm)
  abstract lemma

theorem '∀y z. y = z → (x ↦ y) = (x ↦ z)'
  instantiate (lemma, 'x y ↦ y')

Here, in the first proof, I make sure that x appears in the body of the quantifier.

[ghost]

Ah, my mistake all along. I'd missed the let 'x' in the subproof. Ugh.