Email Gateway (Aug 22 2022 at 18:26): Email Gateway (Aug 22 2022 at 18:26):From: Domagoj Stolfa <ds815@cam.ac.uk>
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
signature.asc
Email Gateway (Aug 22 2022 at 18:27):From: Lars Hupel <hupel@in.tum.de>
This appears to be a problem with "auto".
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):
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
Email Gateway (Aug 22 2022 at 18:27):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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
Last updated: Apr 25 2024 at 20:15 UTC