Higher-order reasoning is incomplete

[rafoo]

In the attach problem, the lemma "f = g" is required to prove the goal hence showing that Zipperposition is incomplete on higher-order problems.

zf_bug.zf.txt

[c-cube]

Not sure if @benti can cook us a version of Zipperposition that is complete on this fragment :-)

[c-cube]

So the problem seems to be the completion of positive equalities. From f = g the prover deduces f x = g x… and throws it away immediately after demodulating it to g x = g x!

[abentkamp]

My stuff doesn't work with lambdas, but if you replace

def f : a -> a := fun x. x.
def g : a -> a := fun x. x.

by

lemma (forall X. f X = X).
lemma (forall X. g X = X).

(i.e. perform lambda-lifting), then I'm pretty sure that the extensional caluli I have would be able to solve it.

[c-cube]

Yeah, I'm working on it, never mind :)

[c-cube]

for some reason, right now, it doesn't (I do exactly this completion).

[c-cube]

should be fixed in 1.6 by @benti and @petarvukmirovic and @gh-salt 's work.