Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Future theorem equality: bad prop for alpha-et...

Email Gateway (Apr 17 2024 at 19:46):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Dear all,

Attached you can find an example that works in Isabelle/jEdit, builds
with a single thread (passing the -o threads=1 option) but does not
build using multi-threaded builds.

The problem here is that function future_result in thm.ML compares
the original proposition to its future counterpart using
alpha-equivalence, not alpha-eta-equivalence:

val _ = prop aconv orig_prop orelse err "bad prop"

I propose to change this line to use alpha-eta-equivalence:

val _ = Envir.aeconv (prop, orig_prop) orelse err "bad prop";

A corresponding patch is attached. To reproduce the error, unzip the
attached session and run isabelle build -vbD <path_to_session>.

The following error is shown:

Thm_Eq FAILED (see also "isabelle build_log -H Error Thm_Eq")
*** exception THM 0 raised (line 832 of "thm.ML"): future_result: bad prop
Unfinished session(s): Thm_Eq

Using a single-threaded build (isabelle build -vbD <path_to_session> -o threads=1) or opening the attached theory in Isabelle/jEdit works as
expected.

This refers to Isabelle rev. b73df63e0f52 (current development version).

Best wishes,

Kevin

PS. The attached example might seem a bit artificial, but the same
problem is triggered in a different context in a formalisation of mine.

future_thm_eq_aeconv.patch
Future_Thm_Eq.zip

Email Gateway (Apr 17 2024 at 19:53):

From: Peter Lammich <lammich@in.tum.de>
I remember problems with PARALLEL_ALLGOALS, that also behaved
differently in sequential and parallel builds ... there, I got the reply
that I was using it outside its specification anyway... and thus it is
acceptable for it to fail or not depending on your machine/build config.
But your example looks like it should be valid in any case.

Email Gateway (Apr 17 2024 at 20:07):

From: Makarius <makarius@sketis.net>
On 17/04/2024 21:38, Kevin Kappelmann wrote:

The problem here is that function future_result in thm.ML compares the
original proposition to its future counterpart using alpha-equivalence, not
alpha-eta-equivalence:

Alpha-equivalence is what the inference kernel usually does. Deviating from
that needs very thorough investigations and argumentation based on the history
of the sources etc. "I prefer to have it differently" is not sufficient.

The following error is shown:

Thm_Eq FAILED (see also "isabelle build_log -H Error Thm_Eq") *** exception THM 0 raised (line 832 of "thm.ML"): future_result: bad prop Unfinished session(s): Thm_Eq

Using a single-threaded build (isabelle build -vbD <path_to_session> -o threads=1) or opening the attached theory in Isabelle/jEdit works as expected.

This refers to Isabelle rev. b73df63e0f52 (current development version).

I've briefly tested it with the last 4-5 official releases, and they are all
the same in this respect.

Thus this feature-request needs to be postponed after the Isabelle2024
release: incidently, I plan to re-open some old proof object / proof term
questions then (but not now).

PS. The attached example might seem a bit artificial, but the same problem is
triggered in a different context in a formalisation of mine.

The example is indeed vacuous. It is possible to make the system break down in
many ways.

Can you show your real applications? (Right now I am busy working towards
Isabelle2024, though.)

Makarius

Email Gateway (Apr 18 2024 at 11:48):

From: Makarius <makarius@sketis.net>
(While waiting for Isabelle2024-RC2 to build ...)

Note that the "implementation" manual section "4.2. Tactics" explicitly states
some semantic well-formedness conditions, including the remark:

"Some of these conditions are checked by higher-level goal infrastructure
(§6.3); others are not checked explicitly, and violating them merely results
in ill-behaved tactics experienced by the user".

So my guess from a distance is that the application uses tactics or Isar proof
methods that are not well-formed in that sense. (The above example is an
example for that, because it changes the main conclusion at will.)

Makarius

Email Gateway (Apr 24 2024 at 15:29):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I changed the tactic in question to produce results that are
alpha-equivalent and not just alpha-eta equivalent. This fixes the
problem in my case.

In general though, the single-threaded and multi-threaded build should
use the same notion of equality. Currently, the single-threaded build
seems to accept theorems up to alpha-beta-eta equivalence while the
multi-threaded build seems to accept up to alpha-beta equivalence, as
the theory below illustrates.

Best wishes,

Kevin

theory Thm_Eq
   imports Pure
begin

declare [[eta_contract=false]]

axiomatization P :: "(prop ⇒ prop) ⇒ prop" and Q :: "prop ⇒ prop"
where PQ: "PROP P Q"

(*works in all cases*)
lemma beta_PQ: "PROP (λx. x) (P Q)"
   apply (tactic ‹fn thm => Seq.single (Goal.protect 0 @{thm PQ})›)
   done

(*only works with threads=1*)
lemma eta_PQ: "PROP P (λx. Q x)"
   apply (tactic ‹fn thm => Seq.single (Goal.protect 0 @{thm PQ})›)
   done

(*only works with threads=1*)
lemma beta_eta_PQ: "PROP (λx. x) (P (λx. Q x))"
   apply (tactic ‹fn thm => Seq.single (Goal.protect 0 @{thm PQ})›)
   done

end

Last updated: May 05 2024 at 04:19 UTC