Email Gateway (Nov 20 2020 at 08:38): Email Gateway (Nov 20 2020 at 08:38):From: Peter Reitinger <peter.reitinger@gmail.com>
Hm also ich wollte nur helfen. Aber anscheinend ist dies unerwünscht...
---------- Forwarded message ---------
Von: <cl-isabelle-users-owner@lists.cam.ac.uk>
Date: Mi., 18. Nov. 2020, 08:44
Subject: Bug in Isabelle 2019/2020
To: <peter.reitinger@gmail.com>
Only subscribers may post messages to this list. If you believe that
you are a subscriber, please check that you are using the subscribed
e-mail address.
---------- Forwarded message ----------
From: Peter Reitinger <peter.reitinger@gmail.com>
To: isabelle-users@cl.cam.ac.uk
Cc:
Bcc:
Date: Wed, 18 Nov 2020 08:44:27 +0100
Subject: Bug in Isabelle 2019/2020
Hello,
I would like to report a bug in Isabelle.
The attached theory file produces unexpected behavior during the
simplification of an obviously true equation.
These are the imports:
imports Main "HOL-Word.Word"
Essentially it is as it cannot proof for a function f that f x = f y
follows from x = y which is absolutely irritating. ;-)
I hope you can find out what is wrong here?
Best regards
Peter Reitinger
In case the bug should not repeat at your installation setup, these are the
proof states of variant a and b respectively.
a:
proof (prove)
goal (1 subgoal):
to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x))
Metis: Falling back on "metis (full_types)"...
Metis: Falling back on "metis (mono_tags)"...
Failed to apply proof method⌂:
goal (1 subgoal):
to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x))
b:
proof (prove)
goal (1 subgoal):
Especially proof state in b after apply (simp add:...) is extremely
confusing.
Show_bug.thy
Email Gateway (Nov 20 2020 at 09:37):From: Manuel Eberl <eberlm@in.tum.de>
Ich weiß nicht, wie die Policy auf der isabelle-users-Mailingliste ist.
Mir war zumindest nicht klar, dass man da subscribed sein muss, um
posten zu können.
So oder so ist das aber kein Bug, sondern völlig erwartetes Verhalten,
und wie ich mir schon dachte liegt es an Polymorphismus:
"to_bl (word_cat (y::4 word) (x::8 word)) =
to_bl (of_bl (to_bl y @ to_bl x))"
Wenn man hier [[show_sorts]] anmacht (z.B. mit "declare [[show_sorts]]"
im theory toplevel oder mit "note [[show_sorts]]" im Isar-Beweis oder
mit "using [[show_sorts]]" im apply-Beweis) sieht man da folgendes:
variables:
x :: 8 word
y :: 4 word
type variables:
'a, 'b :: len0
Dass da zwei Typvariablen 'a und 'b sind (die für die Längen
irgendwelcher Wörter stehen) klingt schon einmal ungut. Man kann
Isabelle auch direkt fragen, warum die linke und rechte Seite nicht
gleich sind, indem man "rule refl" anwendet und unification tracing
anschaltet:
using [[unify_trace_failure]]
apply (rule refl)
Da bekommt man dann die Fehlermeldung
The following types do not unify:
'a::len0 word ⇒ bool list
'b::len0 word ⇒ bool list
Ich hab mir den Term dann etwas genauer angesehen und das Problem ist
die Funktion word_cat:
word_cat :: "'a::len0 word ⇒ 'b::len0 word ⇒ 'c::len0 word"
Diese Funktion macht aus zwei Wörtern beliebiger Länge ein Wort
beliebiger Länge. Gleichzeitig macht das "to_bl", das darauf dann
angewandt wird, aus einem Wort beliebiger Länge eine Liste von booleans.
Dadurch kann dann die Typinferenz von Isabelle nicht mehr herleiten,
dass die Wörter links und rechts von dem "=" gleiche Länge haben sollen.
Also am besten das Ergebnis von "word_cat" immer mit einer Typannotation
versehen. (das gleiche gilt für of_bl, eigentlich alle Funktionen, deren
Rückgabetyp eine zusätzliche Typvariable enthält).
Übermäßiger Polymorphismus ist manchmal etwas haarig, und da das
Typsystem von Isabelle relativ simpel ist sind manche Operationen leider
deutlich polymorpher als man sie gerne hätte…
Viele Grüße
Manuel
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 20 2020 at 09:39):From: Manuel Eberl <eberlm@in.tum.de>
Oops, sorry about that!
Due to a combination of circumstances, somebody wrote a message to me
personally to the isabelle-dev mailing list and I clicked "reply" and
then this happened. Please ignore this.
Manuel
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 19 2024 at 08:19 UTC