Term bug

[ghost]

theory Foo
extends \root

context
  let 'f:𝒰 → 𝒰 → 𝒰 → ℙ'
  val tm = '∀x_1. ∀x_2. ∀x_3. (x_1 ↦ x_2 ↦ f x_1 x_2 x_3) x_2 x_1'
  show reflexive tm

  assert '∀x_1. ∀x_2. ∀x_3. (x_1 ↦ x_2 ↦ f x_1 x_2 x_3) x_2 x_1'
         == '∀x_1. ∀x_2. ∀x_3. (x_1 ↦ x_4 ↦ f x_1 x_4 x_3) x_2 x_1'

The output here is

  ** show (\bugs\foo:7): '(∀ x_1. ∀ x_2. ∀ x_3. (x_3 ↦ ((f x_2) x_3) x_3) x_1) = (∀ x_1. ∀ x_2. ∀ x_3. (x_3 ↦ ((f x_2) x_3) x_3) x_1)' : Theorem
failed compiling theory '\bugs\foo':
  * Assertion does not hold

Notice that in the show, the body of the lambda has been borked. The last two arguments to f are the same, while they originally differed.

This error comes up in simple equality checks, as witnessed by the assertion which should hold here, since all I've done is renamed the variable x_2 in the lambda to x_4.

These errors seem to arise with variables of the form "x_i". My guess is that in the reduction of

(x_1 ↦ x_2 ↦ f x_1 x_2 x_3) x_2 x_1

the bound variable x_2 is renamed to avoid a clash, and x_3 is chosen. This should not happen, since x_3 is already bound, so we're getting a variable capture.

I haven't been able to exploit a soundness bug from this, but it has caused one of my METIS reconstructions to fail. Surprised how late on that is.

[phlegmaticprogrammer]

It is probably a bug in the new eta expansion function, I'll check it out.

[phlegmaticprogrammer]

There was also a bug in the new beta eta expansion function (reflexive tm should be in long eta beta normal form, but wasn't), but the bug you pointed out actually lingered in KernelImpl.substVar which is code about a year old :-) Good catch!