Stream: Isabelle/ML

Topic: Unification issues with OF

view this post on Zulip Paul Bachmann (Jun 17 2021 at 23:02):

I am trying to use the OF combinator with the abstraction theorem from Pure, i.e. (⋀x. ?f x ≡ ?g x) ⟹ λx. ?f x ≡ λx. ?g x. But trying to instantiate the abstraction theorem with the theorem ⋀x. f x ≡ g x yields a unification error (OF: no unifiers). Unification tracing reveals that the clash occurs between Pure.all =/= Pure.eq, but unifying the terms of the theorems manually works fine. Is OF doing something to the theorems that I am not aware of and if so, how can I make the instantiation work?

view this post on Zulip Mathias Fleury (Jun 18 2021 at 08:18):

We need more details to understand your problem. The following works:

lemma H1: ‹(⋀x. f x ≡ g x) ⟹ λx. f x ≡ λx. g x›
  by auto

  assumes H2: ‹⋀x. f x ≡ g x›

thm H1[OF H2]

ML ‹@{thm H1} OF @{thms H2}›

view this post on Zulip Mathias Fleury (Jun 18 2021 at 08:19):

Remark however that you don't get exactly the theorem you want because of HO unification

view this post on Zulip Mathias Fleury (Jun 18 2021 at 08:26):

The HO unification is probably your problem, but we need more details (don't forget to @{print} intermediate results if you are using ML)

view this post on Zulip Paul Bachmann (Jun 18 2021 at 09:23):

The problem seems to be that the theorem that I want to use as H2 has, in ML, the form Const ("Pure.all", "(?'a1 ⇒ prop) ⇒ prop") $ Abs ("x", "?'a1", ...) while your H2 theorem has the bound variable replacd by a Var. I need this because I explicitly want the x variable to be the bound variable in the lambda term of the conclusion of H1 and my f and g terms might be more complicated and might contain more variables. However, I could also try using the version with a Var in H2, but as you suspected, the unification result I get from that is not exactly what I want, since I simply want f and g in H1 to be instantiated with f and g from H2.

view this post on Zulip Manuel Eberl (Jun 18 2021 at 09:54):

I think the problem is that instantiation with OF can only instantiate schematic variables, not variables bound by a Pure.all. This is usually not a problem because all theorems you can normally get your hands on have schematic variables instead of outermost-level-universally-meta-quantified variables anyway.

view this post on Zulip Manuel Eberl (Jun 18 2021 at 09:55):

If you really do have a theorem with outermost-level Pure.all and want to instantiate these variables, you will have to do an explicit elimination of the universal quantifier using e.g. the corresponding functions from the Thm module.

view this post on Zulip Lukas Stevens (Jun 18 2021 at 10:00):

In general, you should probably keep it to schematic variables if possible.

Last updated: Dec 07 2023 at 12:30 UTC