Email Gateway (Jul 29 2023 at 14:09): Email Gateway (Jul 29 2023 at 14:09):From: David Fuenmayor <davfuenmayor@gmail.com>
Dear Isabelle experts,
I was under the false impression that I can just name type variables as I
want ('a, 'x, 'w, 't, etc.) and get away with it everywhere. As it happens
I cannot enforce a convention that uses letters other than the
predetermined ones ('a, 'b, 'c, ...).
From what I see (see attached file) this has to do with two aspects:
1) Type inference using letters 'a, 'b, etc. by default (disregarding, e.g.
the ones used in the involved definitions)
2) Type variable letters in proof steps have to coincide with those already
in the type of the goal.
I understand that this is surely more of a feature than a bug. Still, this
makes teaching Isabelle a bit more difficult. Thanks for understanding.
David
Email Gateway (Jul 30 2023 at 13:21):From: Nicolas Meric <cl-isabelle-users@lists.cam.ac.uk>
Hi David,
why don't you just specify the type of your variable in the lemma prop?
lemma "iDistr (φ::'w set ⇒ 'w set) ⟹ Distr φ"
Nicolas
Email Gateway (Jul 30 2023 at 18:23):From: David Fuenmayor <davfuenmayor@gmail.com>
As I said, I don't think this is a solution (at least not from an "user
experience" perspective). I struggle to see why I cannot follow a
reasonable naming convention for type variables (without having to give up
any niceties like type inference).
As a general comment, I understand that this might sound too nitpicky an
issue. As an "Isabelle evangelist" I often struggle with
explaining/justifying some behaviors which, having an understandable
explanation to the well-versed Isabelle user, may look surprising
<https://en.wikipedia.org/wiki/Principle_of_least_astonishment> to some
laymen (e.g. my students and me ;).
Email Gateway (Jul 31 2023 at 07:30):From: Peter Lammich <lammich@in.tum.de>
While I understand that not "normalizing" the type variable names
(currently happens already in the definition command) may yield better
readability, you should not refer to implicitly inferred type variables
by name. I.e., if you use "'a" or "'w" in your proof, its name should be
explicitly fixed. Otherwise, you create very unstable proofs if the
type-inference has to change the name, i.e., there being two constants
with type 'w in scope.
Note that you can also use lemma "..." for \phi :: "'w set"
Alternatively, you use a context or locale, with
fixes \phi :: "'w set"
Last updated: Apr 28 2024 at 16:17 UTC