Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Name clash in "let" definitions


view this post on Zulip Email Gateway (Oct 29 2020 at 09:31):

From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Isabelle developers,

I just discovered what seems to be a name clash when using "let"
definitions in the following, minimized lemma.

lemma
fixes xs :: "('a × 'b) list" and P :: "'a × 'b ⇒ bool"
shows False
proof -
let ?x0 = "takeWhile P xs"
let ?x = "map fst ?x0"
let ?y = "map snd ?x0"
(*
Type unification failed

Type error in application: incompatible operand type

Operator: map snd :: (??'a × ??'b) list ⇒ ??'b list
Operand: ?x :: 'a list
*)
oops

The name ?x0 seems to be a synonym for ?x. My expectation was that ?x0
and ?x would be two different names for different constants, with
possibly different types).

I confirmed this behaviour with Isabelle/a9aaef9fcf86+ and Isabelle 2020.

Regards,
Martin Desharnais

view this post on Zulip Email Gateway (Oct 29 2020 at 09:50):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Martin,

This behaviour is documented and intended that way. From the Isar-ref
document, Section 3.2:

» ?x and ?x0 and ?x.0 all refer to the same unknown, with basename x and
index 0.«

Regards,
Mathias

view this post on Zulip Email Gateway (Oct 29 2020 at 10:19):

From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Mathias,

Thanks for the clarification. I should have investigated more thoroughly
before posting.

Sorry for disturbing,
Martin

view this post on Zulip Email Gateway (Oct 29 2020 at 11:02):

From: Peter Lammich <lammich@in.tum.de>
If you should need to refer to the variable name "x0" with index 0, you
can always write ?x0.0, e.g.

lemma foo: "x0 + (0::int) = x0" by simp

thm foo[where ?x0.0=2]


Last updated: Sep 25 2021 at 09:17 UTC