Email Gateway (Aug 19 2022 at 13:08): Email Gateway (Aug 19 2022 at 13:08):From: Alessandro Coglio <coglio@kestrel.edu>
In the following artificial example
datatype T = A | B | C
fun f :: "T ⇒ T ⇒ bool"
where
"f A A ⟷ True" |
"f B B ⟷ True" |
"f C C ⟷ True" |
"f _ _ ⟷ False"
‘fun’ gives a warning about duplicate rewrite rules
Ignoring duplicate rewrite rule:
f C B ≡ False
Ignoring duplicate rewrite rule:
f B C ≡ False
Ignoring duplicate rewrite rule:
f C B ≡ False
Ignoring duplicate rewrite rule:
f B C ≡ False
and ‘thm f.simps’ shows 9 distinct rules plus 2 duplicates
f A A = True
f B B = True
f C C = True
f B A = False
f B C = False +
f C A = False
f C B = False ++
f A B = False
f C B = False ++
f A C = False
f B C = False +
I suppose that the duplicate rules are harmless, but is this the expected/intended behavior?
Rephrasing as
fun f :: "T ⇒ T ⇒ bool"
where
"f A A ⟷ True" |
"f A _ ⟷ False" |
"f B B ⟷ True" |
"f B _ ⟷ False" |
"f C C ⟷ True" |
"f C _ ⟷ False"
avoids the issue but is more verbose.
I’m using Isabelle 2013-2.
Thank you in advance.
smime.p7s
Email Gateway (Aug 19 2022 at 13:08):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Mon, 30 Dec 2013 00:49:37 +0100, Alessandro Coglio
<coglio@kestrel.edu> a écrit:
In the following artificial example
datatype T = A | B | C
fun f :: "T ⇒ T ⇒ bool"
where
"f A A ⟷ True" |
"f B B ⟷ True" |
"f C C ⟷ True" |
"f _ _ ⟷ False"‘fun’ gives a warning about duplicate rewrite rules
Ignoring duplicate rewrite rule:
f C B ≡ False
Ignoring duplicate rewrite rule:
f B C ≡ False
Ignoring duplicate rewrite rule:
f C B ≡ False
Ignoring duplicate rewrite rule:
f B C ≡ False
I'm also noticing something else strange aside: with the last two cases,
the output pan says “f” is a free variable while it says it's fixed with
the first two cases.
[…]
Rephrasing as
fun f :: "T ⇒ T ⇒ bool"
where
"f A A ⟷ True" |
"f A _ ⟷ False" |
"f B B ⟷ True" |
"f B _ ⟷ False" |
"f C C ⟷ True" |
"f C _ ⟷ False"avoids the issue but is more verbose.
I don't know how close is the artificial case to the real case, still what
about this one:
fun f :: "T ⇒ T ⇒ bool"
where "f x y ⟷ x = y"
Then…
thm f.simps
…just says:
f ?x ?y = (?x = ?y)
Email Gateway (Aug 19 2022 at 13:08):From: Alessandro Coglio <coglio@kestrel.edu>
The real case has two different datatypes as arguments to f, additional conditions on constructor arguments, etc. I’ve reduced it to what may be a minimal example. The issue doesn’t arise with just two constructors.
smime.p7s
Email Gateway (Aug 19 2022 at 13:08):From: Tobias Nipkow <nipkow@in.tum.de>
This is the normal behaviour. Overlapping patterns need to be disambiguated.
Minimizing the number of unambiguous patterns is complex (in the complexity
theoretic sense) and not attempted by "fun". See
Alexander Krauss. Pattern minimization problems over recursive data types. In
James Hook and Peter Thiemann, editors, International Conference on Functional
Programming (ICFP 2008). ACM, 2008.
http://www21.in.tum.de/~krauss/
Tobias
Last updated: May 01 2024 at 20:18 UTC