Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer in Locale Context?

view this post on Zulip Email Gateway (Jun 20 2022 at 13:30):

From: Steven Obua <obua@practal.com>
Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.

I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:

"cvc4": Prover error: exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term
It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.

Cheers,

Steven

view this post on Zulip Email Gateway (Jun 20 2022 at 16:11):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Do you have an example theory where this happens?

Mathias

view this post on Zulip Email Gateway (Jun 20 2022 at 17:49):

From: Steven Obua <obua@practal.com>
Hi Mathias,

sorry, I don't have an example that I can easily share now. I tried to construct one, see below, where the lemma inside of the context cannot be sledgehammered, but the same lemma outside can. But in this smaller example it works, in my larger real-life theory it fails.

I am not doubting that sledgehammer works in principle in locales, I am just wondering if it is generally known currently that there can be problems, or if I am just running into some weird special cases.

Cheers,

Steven

theory TestSledge imports Main
begin

typedecl 'a algebra
typedecl signature

consts Algebra :: "'a algebra"
consts Sig :: "'a algebra ⇒ signature"

type_synonym variable = string

datatype nterm = VarApp variable "nterm list"

axiomatization nt_frees :: "signature ⇒ nterm ⇒ variable set" where
nt_frees_ax: "nt_frees sig (VarApp x ts) = {x} ∪ ⋃ { nt_frees sig t | t. t ∈ set ts }"

locale AA =
fixes U :: "'a algebra" ("𝔄")

context AA
begin

abbreviation S :: "signature" ("𝒮") where "S ≡ Sig 𝔄"
abbreviation frees :: "nterm ⇒ variable set" where "frees t ≡ nt_frees 𝒮 t"

lemma
assumes "frees (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "frees (ts ! i) ⊆ X"
sledgehammer
oops

end

lemma
assumes "nt_frees (Sig U) (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "nt_frees (Sig U) (ts ! i) ⊆ X"
sledgehammer
oops

end

On Mon, Jun 20, 2022, at 5:11 PM, Mathias Fleury wrote:

Do you have an example theory where this happens?

Mathias

On 20/06/2022 15:26, Steven Obua wrote:

Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.

I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:

"cvc4": Prover error: exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term

It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.

Cheers,

Steven

view this post on Zulip Email Gateway (Jun 20 2022 at 22:32):

From: Gerwin Klein <kleing@unsw.edu.au>
Hi Steven,

we've definitely had (many) cases where sledgehammer fails to find a proof in a larger locale context, but does find a proof outside the locale. I usually do not get an error message -- it's just timing out, because there are more facts in the context. I'd say that is completely expected behaviour.

"bad SMT term" sounds to me like a genuine error case, though, and not expected.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Jun 23 2022 at 13:31):

From: Steven Obua <obua@practal.com>
Hi Gerwin,

My locale context is very small so far, so I wouldn't think that is an issue here. But it works now mostly for me, the problems seem to occur, when they occur, only with the provers cvc4, z3 and verit.

Cheers,

Steven

On Mon, Jun 20, 2022, at 11:31 PM, Gerwin Klein wrote:

Hi Steven,

we've definitely had (many) cases where sledgehammer fails to find a proof in a larger locale context, but does find a proof outside the locale. I usually do not get an error message -- it's just timing out, because there are more facts in the context. I'd say that is completely expected behaviour.

"bad SMT term" sounds to me like a genuine error case, though, and not expected.

Cheers,
Gerwin

On 21 Jun 2022, at 03:48, Steven Obua <obua@practal.com> wrote:

Hi Mathias,

sorry, I don't have an example that I can easily share now. I tried to construct one, see below, where the lemma inside of the context cannot be sledgehammered, but the same lemma outside can. But in this smaller example it works, in my larger real-life theory it fails.

I am not doubting that sledgehammer works in principle in locales, I am just wondering if it is generally known currently that there can be problems, or if I am just running into some weird special cases.

Cheers,

Steven

theory TestSledge imports Main
begin

typedecl 'a algebra
typedecl signature

consts Algebra :: "'a algebra"
consts Sig :: "'a algebra ⇒ signature"

type_synonym variable = string

datatype nterm = VarApp variable "nterm list"

axiomatization nt_frees :: "signature ⇒ nterm ⇒ variable set" where
nt_frees_ax: "nt_frees sig (VarApp x ts) = {x} ∪ ⋃ { nt_frees sig t | t. t ∈ set ts }"

locale AA =
fixes U :: "'a algebra" ("𝔄")

context AA
begin

abbreviation S :: "signature" ("𝒮") where "S ≡ Sig 𝔄"
abbreviation frees :: "nterm ⇒ variable set" where "frees t ≡ nt_frees 𝒮 t"

lemma
assumes "frees (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "frees (ts ! i) ⊆ X"
sledgehammer
oops

end

lemma
assumes "nt_frees (Sig U) (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "nt_frees (Sig U) (ts ! i) ⊆ X"
sledgehammer
oops

end

On Mon, Jun 20, 2022, at 5:11 PM, Mathias Fleury wrote:

Do you have an example theory where this happens?

Mathias

On 20/06/2022 15:26, Steven Obua wrote:

Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.
I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:

"cvc4": Prover error: exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term

It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.

Cheers,

Steven

view this post on Zulip Email Gateway (Jun 24 2022 at 05:45):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Steven,

On 23/06/2022 15:30, Steven Obua wrote:

Hi Gerwin,

But it works now mostly for me, the problems seem to occur, when they
occur, only with the provers cvc4, z3 and verit.

Given that these are the only SMT solver called by default from
Isabelle, this makes a lot of sense that you face that error only with them.

Without example (I can look at big theories), it is impossible to debug
the problem.

Cheers,

Mathias

Cheers,

Steven

On Mon, Jun 20, 2022, at 11:31 PM, Gerwin Klein wrote:

Hi Steven,

we've definitely had (many) cases where sledgehammer fails to find a
proof in a larger locale context, but does find a proof outside the
locale. I usually do not get an error message -- it's just timing
out, because there are more facts in the context. I'd say that is
completely expected behaviour.

"bad SMT term" sounds to me like a genuine error case, though, and
not expected.

Cheers,
Gerwin

On 21 Jun 2022, at 03:48, Steven Obua <obua@practal.com

<mailto:obua@practal.com>> wrote:

Hi Mathias,

sorry, I don't have an example that I can easily share now. I tried
to construct one, see below, where the lemma inside of the context
cannot be sledgehammered, but the same lemma outside can. But in
this smaller example it works, in my larger real-life theory it fails.

I am not doubting that sledgehammer works in principle in locales, I
am just wondering if it is generally known currently that there can
be problems, or if I am just running into some weird special cases.

Cheers,

Steven

theory TestSledge imports Main
begin

typedecl 'a algebra
typedecl signature

consts Algebra :: "'a algebra"
consts Sig :: "'a algebra ⇒ signature"

type_synonym variable = string

datatype nterm = VarApp variable "nterm list"

axiomatization nt_frees :: "signature ⇒ nterm ⇒ variable set" where
  nt_frees_ax: "nt_frees sig (VarApp x ts) =  {x} ∪ ⋃ { nt_frees sig
t | t. t ∈ set ts }"

locale AA =
  fixes U :: "'a algebra" ("𝔄")

context AA
begin

abbreviation S :: "signature" ("𝒮") where "S ≡ Sig 𝔄"
abbreviation frees :: "nterm ⇒ variable set" where "frees t ≡
nt_frees 𝒮 t"

lemma
  assumes "frees (VarApp x ts) ⊆ X"
  assumes "i < length ts"
  shows "frees (ts ! i) ⊆ X"
  sledgehammer
  oops

end

lemma
  assumes "nt_frees (Sig U) (VarApp x ts) ⊆ X"
  assumes "i < length ts"
  shows "nt_frees (Sig U) (ts ! i) ⊆ X"
  sledgehammer
  oops

end

On Mon, Jun 20, 2022, at 5:11 PM, Mathias Fleury wrote:

Do you have an example theory where this happens?

Mathias

On 20/06/2022 15:26, Steven Obua wrote:

Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just
now trying to also use locales, as in my use case there are just
overwhelming arguments for it.
I am using the Isabelle/December 2021 distribution, but most of
the time when I am trying to use sledgehammer within a locale
context, I will get a message like this:

|"cvc4": Prover error: exception TERM raised (line 457 of
"~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term |

It is the same message for other provers as well. Is this
something that is a well-known problem? Without using locales I
had such a problem only come up when my theory name was confused
with some HOL theory name, and renaming my theory was a
workaround. Is there something similar at play here? Is there an
easy fix? Because I use sledgehammer a lot, so not being able to
use it within a locale would be a severe blow against using locales.

Cheers,

Steven

view this post on Zulip Email Gateway (Jun 24 2022 at 14:39):

From: Steven Obua <obua@practal.com>
Hi Mathias,

I would not expect anyone to debug without an example, actually I would not expect anyone to debug!

In case someone feels the inclination to do so, though, I have now made my theories publicly available. They are not very big (and I hope it stays that way!). It is work in progress and still early stages.

An example of the error situation can be found at
https://github.com/practal/AL-in-HOL/blob/f4557af8109501450009777d03741b9efe56d885/Valuation.thy#L167

If you insert a call to sledgehammer there, you will get error messages of the type I talked about, see pictures below. I don't know though if outside of the locale the provers would succeed instead, or just timeout as well.

Cheers,

Steven

On Fri, Jun 24, 2022, at 6:45 AM, Mathias Fleury wrote:

Hi Steven,

On 23/06/2022 15:30, Steven Obua wrote:

Hi Gerwin,

But it works now mostly for me, the problems seem to occur, when they occur, only with the provers cvc4, z3 and verit.
Given that these are the only SMT solver called by default from Isabelle, this makes a lot of sense that you face that error only with them.

Without example (I can look at big theories), it is impossible to debug the problem.

Cheers,

Mathias

Cheers,

Steven

On Mon, Jun 20, 2022, at 11:31 PM, Gerwin Klein wrote:

Hi Steven,

we've definitely had (many) cases where sledgehammer fails to find a proof in a larger locale context, but does find a proof outside the locale. I usually do not get an error message -- it's just timing out, because there are more facts in the context. I'd say that is completely expected behaviour.

"bad SMT term" sounds to me like a genuine error case, though, and not expected.

Cheers,
Gerwin

On 21 Jun 2022, at 03:48, Steven Obua <obua@practal.com> wrote:

Hi Mathias,

sorry, I don't have an example that I can easily share now. I tried to construct one, see below, where the lemma inside of the context cannot be sledgehammered, but the same lemma outside can. But in this smaller example it works, in my larger real-life theory it fails.

I am not doubting that sledgehammer works in principle in locales, I am just wondering if it is generally known currently that there can be problems, or if I am just running into some weird special cases.

Cheers,

Steven

theory TestSledge imports Main
begin

typedecl 'a algebra
typedecl signature

consts Algebra :: "'a algebra"
consts Sig :: "'a algebra ⇒ signature"

type_synonym variable = string

datatype nterm = VarApp variable "nterm list"

axiomatization nt_frees :: "signature ⇒ nterm ⇒ variable set" where
nt_frees_ax: "nt_frees sig (VarApp x ts) = {x} ∪ ⋃ { nt_frees sig t | t. t ∈ set ts }"

locale AA =
fixes U :: "'a algebra" ("𝔄")

context AA
begin

abbreviation S :: "signature" ("𝒮") where "S ≡ Sig 𝔄"
abbreviation frees :: "nterm ⇒ variable set" where "frees t ≡ nt_frees 𝒮 t"

lemma
assumes "frees (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "frees (ts ! i) ⊆ X"
sledgehammer
oops

end

lemma
assumes "nt_frees (Sig U) (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "nt_frees (Sig U) (ts ! i) ⊆ X"
sledgehammer
oops

end

On Mon, Jun 20, 2022, at 5:11 PM, Mathias Fleury wrote:

Do you have an example theory where this happens?

Mathias

On 20/06/2022 15:26, Steven Obua wrote:

Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.
I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:

"cvc4": Prover error: exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term

It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.

Cheers,

Steven

image.png
image.png

view this post on Zulip Email Gateway (Jun 24 2022 at 17:03):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Steven,

In your definition of eval, unfold the let op = and the SMT
translation will work.

I am still looking for the reason for this though. There seem to be some
interaction between lambdas and lets.

Mathias
image.png
image.png

view this post on Zulip Email Gateway (Jun 24 2022 at 17:51):

From: Steven Obua <obua@practal.com>
Hi Mathias,

thank you for finding this! Even if the bug cannot be fixed easily, it is definitely very helpful to know how to not run into it in the first place.

Cheers,

Steven

On Fri, Jun 24, 2022, at 6:02 PM, Mathias Fleury wrote:

Hi Steven,

In your definition of eval, unfold the let op = and the SMT translation will work.

I am still looking for the reason for this though. There seem to be some interaction between lambdas and lets.

Mathias

On 24/06/2022 16:37, Steven Obua wrote:

Hi Mathias,

I would not expect anyone to debug without an example, actually I would not expect anyone to debug!

In case someone feels the inclination to do so, though, I have now made my theories publicly available. They are not very big (and I hope it stays that way!). It is work in progress and still early stages.

An example of the error situation can be found at
https://github.com/practal/AL-in-HOL/blob/f4557af8109501450009777d03741b9efe56d885/Valuation.thy#L167

If you insert a call to sledgehammer there, you will get error messages of the type I talked about, see pictures below. I don't know though if outside of the locale the provers would succeed instead, or just timeout as well.

Cheers,

Steven

On Fri, Jun 24, 2022, at 6:45 AM, Mathias Fleury wrote:

Hi Steven,

On 23/06/2022 15:30, Steven Obua wrote:

Hi Gerwin,

But it works now mostly for me, the problems seem to occur, when they occur, only with the provers cvc4, z3 and verit.
Given that these are the only SMT solver called by default from Isabelle, this makes a lot of sense that you face that error only with them.

Without example (I can look at big theories), it is impossible to debug the problem.

Cheers,

Mathias

Cheers,

Steven

On Mon, Jun 20, 2022, at 11:31 PM, Gerwin Klein wrote:

Hi Steven,

we've definitely had (many) cases where sledgehammer fails to find a proof in a larger locale context, but does find a proof outside the locale. I usually do not get an error message -- it's just timing out, because there are more facts in the context. I'd say that is completely expected behaviour.

"bad SMT term" sounds to me like a genuine error case, though, and not expected.

Cheers,
Gerwin

On 21 Jun 2022, at 03:48, Steven Obua <obua@practal.com> wrote:

Hi Mathias,

sorry, I don't have an example that I can easily share now. I tried to construct one, see below, where the lemma inside of the context cannot be sledgehammered, but the same lemma outside can. But in this smaller example it works, in my larger real-life theory it fails.

I am not doubting that sledgehammer works in principle in locales, I am just wondering if it is generally known currently that there can be problems, or if I am just running into some weird special cases.

Cheers,

Steven

theory TestSledge imports Main
begin

typedecl 'a algebra
typedecl signature

consts Algebra :: "'a algebra"
consts Sig :: "'a algebra ⇒ signature"

type_synonym variable = string

datatype nterm = VarApp variable "nterm list"

axiomatization nt_frees :: "signature ⇒ nterm ⇒ variable set" where
nt_frees_ax: "nt_frees sig (VarApp x ts) = {x} ∪ ⋃ { nt_frees sig t | t. t ∈ set ts }"

locale AA =
fixes U :: "'a algebra" ("𝔄")

context AA
begin

abbreviation S :: "signature" ("𝒮") where "S ≡ Sig 𝔄"
abbreviation frees :: "nterm ⇒ variable set" where "frees t ≡ nt_frees 𝒮 t"

lemma
assumes "frees (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "frees (ts ! i) ⊆ X"
sledgehammer
oops

end

lemma
assumes "nt_frees (Sig U) (VarApp x ts) ⊆ X"
assumes "i < length ts"
shows "nt_frees (Sig U) (ts ! i) ⊆ X"
sledgehammer
oops

end

On Mon, Jun 20, 2022, at 5:11 PM, Mathias Fleury wrote:

Do you have an example theory where this happens?

Mathias

On 20/06/2022 15:26, Steven Obua wrote:

Hi,

I am a happy user of Isabelle/Isar and Sledgehammer, but am just now trying to also use locales, as in my use case there are just overwhelming arguments for it.
I am using the Isabelle/December 2021 distribution, but most of the time when I am trying to use sledgehammer within a locale context, I will get a message like this:

"cvc4": Prover error: exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term

It is the same message for other provers as well. Is this something that is a well-known problem? Without using locales I had such a problem only come up when my theory name was confused with some HOL theory name, and renaming my theory was a workaround. Is there something similar at play here? Is there an easy fix? Because I use sledgehammer a lot, so not being able to use it within a locale would be a severe blow against using locales.

Cheers,

Steven

image.png
image.png

view this post on Zulip Email Gateway (Jun 24 2022 at 17:54):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Steven,

I found the bug: there is missing recursive call of expand at
https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Tools/SMT/smt_translate.ML#l216.
So lets inside lets are not expanded.

If testboard does not complain about my patch, I will push it.

Thanks for reporting the bug!

Mathias
image.png
image.png

Last updated: Jan 04 2025 at 20:18 UTC