Email Gateway (Aug 19 2022 at 16:57): Email Gateway (Aug 19 2022 at 16:57):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
This is just an observation about the "simplified" attribute. Maybe it
is well-known and its just me who wasn't aware of it.
Suppose I have a lemma like
consts foo :: "'a list ⇒ 'b list ⇒ 'a list list"
lemma foo:
"i < length ys ==>
foo xs ys ! i = take (ys ! i) (drop (listsum (take i ys)) xs)"
sorry
and now I want a special version for when "ys" is actually "map size
ys". So I do
thm foo [of _ "map size ys" for ys, simplified]
Now in the result the assumption "?i < length (map size ?ys2)" is
simplified to "?i < length ?ys2". However, "map size ?ys2 ! ?i" is not
simplified to "size (?ys2 ! i)" (which I expected in presence of "?i <
length ?ys2").
Conclusion: The simplifier treats schematic variables in conditions
differently than free variables (which is no surprise). Is there a way
to obtain the result I expected without having to restate the whole lemma?
cheers
chris
Email Gateway (Aug 19 2022 at 16:59):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Christian.
You were half-correct about what was going on here. Both type-schematics
and term-schematics obstruct the simplifier. After a lot of fiddling I
discovered that you get the lemma you want like this:
lemmas foo4 = foo [of i "map size ys", simplified] for i and ys :: "('b
:: size) list"
OK, a little on how I got there. Turning on simplifier tracing causes
the simplifier to trace this issue with the previous simplification attempt:
"[1]Cannot add premise as rewrite rule because it contains (type) unknowns:"
(I used "declare [[simp_trace = true]]" but I think there might also be
a more modern way.)
OK, so the simplifier can't assume something that contains either a
term-unknown or a type-unknown. Turning on "[[show_types = true]]" also
helps here.
To start with, we instantiate all the term variables. I'm also using the
"for" form of "lemmas" rather than within the attribute, because this
leaves the variables fixed for the execution of the subsequent attributes.
lemmas foo2 = foo [of i "map size ys" xs, simplified] for i ys xs
OK, the simplifier still complains about the type-unknown that was
introduced by typing "map size ys". This wouldn't happen, if, for
instance, we used "Suc" instead of "size":
lemmas foo3 = foo [of i "map Suc ys" xs, simplified] for i ys xs
The simplification happens on foo3. This gave me hope, but for a while I
couldn't figure out how to get the right lemma other than opening and
closing a context to fix ys to an appropriate type. Finally I realised
that the analogous syntax works with lemmas, giving me the form I
mentioned first.
OK, hope that helps. Good luck,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC