Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] size_change raises DUP

Email Gateway (Aug 19 2022 at 11:29):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,

I ran into a case where size_change raises the exception DUP. As this is a low-level
exception that normally should not propagate to the user, I consider this as a bug report.
Here's the reduced example:

datatype foo = A | B foo | C foo foo | D foo foo

function F :: "foo => unit set set"
where
"F A = {{()}}"
| "F (C _ _) = {}"
| "F (D _ _) = {}"
| "F (B A) = {{()}}"
| "F (B (B f)) = F f"
| "F (B (D f f')) = F (C (B f) (B f'))"
| "F (B (C f f')) = F (B f') Un F (B f')"
by pat_completeness simp_all
termination apply size_change (* raises DUP *)
by(relation
"measure (foo_rec 0 (%_. op + 1) (%_ _ n m. n + m + 1) (%_ _ n m. 2 * n + 2 * m + 3))")
simp_all

*** exception DUP (Const ("Set.Collect", "((Scratch.foo, Scratch.foo) Product_Type.prod =>
HOL.bool) => (Scratch.foo, Scratch.foo) Product_Type.prod Set.set") $ Abs ("uu_",
"(Scratch.foo, Scratch.foo) Product_Type.prod", Const ("HOL.Ex", "(Scratch.foo =>
HOL.bool) => HOL.bool") $ Abs ("f", "Scratch.foo", Const ("HOL.Ex", "(Scratch.foo =>
HOL.bool) => HOL.bool") $ Abs ("f'", "Scratch.foo", Const ("HOL.conj", "HOL.bool =>
HOL.bool => HOL.bool") $ (Const ("HOL.eq", "(Scratch.foo, Scratch.foo) Product_Type.prod
=> (Scratch.foo, Scratch.foo) Product_Type.prod => HOL.bool") $ Bound 2 $ (Const
("Product_Type.Pair", "Scratch.foo => Scratch.foo => (Scratch.foo, Scratch.foo)
Product_Type.prod") $ (Const ("Scratch.foo.B", "Scratch.foo => Scratch.foo") $ Bound 0) $
(Const ("Scratch.foo.B", "Scratch.foo => Scratch.foo") $ (Const ("Scratch.foo.C",
"Scratch.foo => Scratch.foo => Scratch.foo") $ Bound 1 $ Bound 0)))) $ Const ("HOL.True",
"HOL.bool"))))) raised (line 261 of "General/table.ML")
*** At command "apply"

Exception trace for exception - DUP raised in General/table.ML line 261

Termination.mk_dgraph(2)
Termination.decompose_tac(1)(2)
Termination.CALLS(3)
Tactical.THEN_ALL_NEW(4)
Seq.maps(2)(1)
Seq.append(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.append(2)copy(1)(1)
Seq.first_result(2)result(3)
Seq.first_result(2)
Toplevel.proofs'(1)(1)(1)
End of trace

Best,
Andreas

Email Gateway (Aug 19 2022 at 11:30):

From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,

Thanks for the report. It seems that the graph decomposition cannot cope
with the same recursive call occurring twice... (But the issue only
occurs when graph decomposition actually happens since the plain scnp
method does not succeed). Here is a more minimal example:

function f :: "nat => nat"
where "f x = f x + f x"
by auto
termination apply size_change

I'll look for a fix...

Alex

Last updated: Apr 18 2024 at 16:19 UTC