Odd behaviour of combine

[ghost]

I want to write a general gsym derived rule which applies sym to the body of a quantified formula. So the idea is that if you have a theorem ⊢ ∀x y. x = y, and you apply gsym to it, you get ⊢ ∀x y. y = x.

Here's my first shot at an implementation:

def sym ('‹x› = ‹y›' as thm) =
  modusponens (reflexive '‹x›',combine (reflexive '(z ↦ z = ‹x›)', thm))

def
  gsym '‹x› = ‹y›' as thm = sym thm
  gsym '∀x. ‹p› x' =
    val [ctx,x,eq] = destabs p
    context <ctx>
      return (gsym eq)

This doesn't work, with proofscript complaining that antecedents don't match in modusponens . But the problem appears to be with combine. If I do:

def sym ('‹x› = ‹y›' as thm) =
  val eqx = reflexive '(z ↦ z = ‹x›)'
  assert (combine (eqx,thm) <> eqx)
  modusponens (reflexive '‹x›',combine (reflexive '(z ↦ z = ‹x›)', thm))

def
  gsym '‹x› = ‹y›' as thm = sym thm
  gsym '∀x. ‹p› x' =
    val [ctx,x,eq] = destabs p
    context <ctx>
      return (gsym eq)

context
  assume asm:'∀x y. x = y'
  show gsym asm

The call to combine succeeds, but the assertion fails. That can't be right, surely?

[phlegmaticprogrammer]

This was a bug in the error detection of combine, this is fixed in commit 59d66ae16e2dca9767a8a8a24be276639b6d6277.

The above example then fails correctly in combine, because you are passing a term to sym, not a theorem.