[isabelle] Possible bug in Finite_Map

[Domagoj Stolfa]

Hi all:

I've tried naively writing a function that filters some values in the codomain of an fmap. It resulted in a function that looks a little bit like:

fun filter_types_clause :: "(var, (ty × nat)) fmap ⇒ (var, (ty × nat)) fmap" where
"filter_types_clause m = fmfilter
(λx .
(let r = fmlookup m x in
case r of None ⇒ False
| Some res ⇒ let scp = snd res in
if scp = 2 √ scp = 3
then True
else False))
m"


However, Isabelle wasn't happy with the function and outputted the following error:

exception THM 0 raised (line 86 of "goal.ML"):
Proof failed.
1. ⋀ma. fmfilter
(λx. case fmlookup ma x of None ⇒ False
| Some res ⇒ let scp = snd res in (scp = 2 √ scp = 3 ⟶ True) ∧ (¬ (scp = 2 √ scp = 3) ⟶ False))
ma =
fmfilter
(λx. Let (fmlookup ma x)
(case_option False
(λres. let scp = snd res in (scp = 2 √ scp = 3 ⟶ True) ∧ (¬ (scp = 2 √ scp = 3) ⟶ False))))
ma
(⋀ma. fmfilter
(λx. case fmlookup ma x of None ⇒ False
| Some res ⇒ let scp = snd res in (scp = 2 √ scp = 3 ⟶ True) ∧ (¬ (scp = 2 √ scp = 3) ⟶ False))
ma =
fmfilter
(λx. Let (fmlookup ma x)
(case_option False
(λres. let scp = snd res in (scp = 2 √ scp = 3 ⟶ True) ∧ (¬ (scp = 2 √ scp = 3) ⟶ False))))
ma) ⟹
((⋀a. Wellfounded.accp filter_types_clause_rel a ⟹ ∃!y. filter_types_clause_graph a y) &&&
(⋀P x. (⋀m. x = m ⟹ P) ⟹ P))
[filter_types_clause_graph ≡ ??.tinyd.filter_types_clause_graph]


Writing the function without the first let, and instead putting the expression (fmlookup m x) in the case expression eliminates the bug. Moreover, writing it as a definition instead of a function in the above form also gets rid of the problem (as it's non-recursive to begin with). After talking to Lars (who also suggested writing it down as a definition instead of a function), we seem to have reached a conclusion that it may be a bug in Finite_Map -- could anyone confirm/reproduce this? The "var" type is a String.literal and "ty" is just a sum type with four constructors, ty_int, ty_array, ty_bool and ty_unit.

The version of Isabelle is 2018 and I've been running it on Mac OS X.

Thanks!

—
Domagoj

[Lars Hupel]

This appears to be a problem with "auto".

fun filter_types_clause :: "(var, (ty × nat)) fmap ⇒ (var, (ty × nat)) fmap" where
"filter_types_clause m = fmfilter
(λx .
(let r = fmlookup m x in
case r of None ⇒ False
| Some res ⇒ let scp = snd res in
if scp = 2 ∨ scp = 3
then True
else False))
m"

Here is a smaller reproducer:

"filter_types_clause m = fmfilter
(λx .
(let r = fmlookup m x in
case r of Some res ⇒ snd res = 2))
m"

When defining this function "function (sequential)", "pat_completeness"
discharges the first subgoal as it should. But "auto", instead of
solving the remaining one, produces this goal state:

goal (1 subgoal):
1. ⋀ma.
fmfilter (λx. case fmlookup ma x of Some res ⇒ snd res = 2) ma =
fmfilter (λx. Let (fmlookup ma x) (case_option undefined (λres. snd
res = 2))) ma

For some reason, it unfolds the "Let" in the first half of the equation,
but not in the second half.

Without the let simproc, it works:

declare [[simproc del: let_simp]]

Maybe someone who knows how that simproc works could take a look.

Cheers
Lars

[Andreas Lochbihler]

Hi Lars,

I briefly looked into this. To me, let_simp does not seem to be the culprit. From looking
at simp_trace and simp_debug, It seems as if there is an unfortunate interaction between
the congruence rule for fmfilter and the case_option simp rules. For if I delete the
fmfilter_cong congruence rule, the proof succeeds.

Andreas

Post by Lars Hupel
This appears to be a problem with "auto".

fun filter_types_clause :: "(var, (ty × nat)) fmap ⇒ (var, (ty × nat)) fmap" where
"filter_types_clause m = fmfilter
(λx .
(let r = fmlookup m x in
case r of None ⇒ False
| Some res ⇒ let scp = snd res in
if scp = 2 ∨ scp = 3
then True
else False))
m"

"filter_types_clause m = fmfilter
(λx .
(let r = fmlookup m x in
case r of Some res ⇒ snd res = 2))
m"
When defining this function "function (sequential)", "pat_completeness"
discharges the first subgoal as it should. But "auto", instead of
1. ⋀ma.
fmfilter (λx. case fmlookup ma x of Some res ⇒ snd res = 2) ma =
fmfilter (λx. Let (fmlookup ma x) (case_option undefined (λres. snd
res = 2))) ma
For some reason, it unfolds the "Let" in the first half of the equation,
but not in the second half.
declare [[simproc del: let_simp]]
Maybe someone who knows how that simproc works could take a look.
Cheers
Lars