Email Gateway (Aug 19 2022 at 15:34): Email Gateway (Aug 19 2022 at 15:34):From: Jakob von Raumer <javra@web.de>
Hello everyone,
am I just bad at using find_theorems or is there no lemma that remdups_adj
really yields lists with no adjacent entries being equal? If it's really
missing, here's my somewhat lengthy proof:
https://gist.github.com/javra/68c7f852a060d7cb6036
Best regards
Jakob
Email Gateway (Aug 19 2022 at 15:35):From: Tobias Nipkow <nipkow@in.tum.de>
Important lemma. I have just added a more succinct proof of it due to Manuel
Eberl http://shodan.linuxd.org/paste/oyIsOBq1 to List.thy.
Thanks to both of you!
Tobias
Email Gateway (Aug 19 2022 at 15:35):From: Jakob von Raumer <javra@web.de>
Wow, thank you! I really have to learn to search for short proofs (or in
this case, remember to use the right induction lemmas). Another lemma,
which is useful for working not with inductively defined lists but by
indexing lists is the following: Adjacencies are preserved by remdups_adj
in the sense that for each index in the reduced list there's an index in
the original list so that the list entries coincide at this entry and their
respective successors: https://gist.github.com/javra/11b9a6770cab2e17559d
(I could work on a shorter proof the next days).
Best regards
Jakob
Email Gateway (Aug 19 2022 at 15:35):From: Lars Noschinski <noschinl@in.tum.de>
Sometimes, I find working on shorter proofs a nice exercise to
understand the system and for getting more out of the automation.
Note that the "0 < length xs" assumption on your lemma is not needed (it
is already implied by "j + 1 < length xs").
Email Gateway (Aug 19 2022 at 15:35):From: Tobias Nipkow <nipkow@in.tum.de>
It seems to me that we need an abstract nonrecursive characterisation of
remdups_adj from which specific lemmas follow easily. Is the following correct?
remdups_adj xs = ys <->
EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
& (ALL i < size xs. xs!i = ys!(f i)
& (xs!i = xs!(i+1) <-> f i = f(i+1)))
It should be sound (-->), but is it complete (<--)?
Tobias
Email Gateway (Aug 19 2022 at 15:35):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
At least there needs to be one more implication added, since
otherwise the reference to xs!(i+1) is critical.
remdups_adj xs = ys <->
EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
& (ALL i < size xs. xs!i = ys!(f i)
& (i + 1 < size xs --> (xs!i = xs!(i+1) <-> f i = f(i+1))))
Otherwise, it looks good (soundness and completeness can easily be proven
for lists upto length 1, but the inductive case became quite tedious in my proof attempt)
René
Email Gateway (Aug 19 2022 at 15:35):From: Lars Noschinski <noschinl@in.tum.de>
I've got a (lenghty, but otherwise straightforward) proof of
completeness for the modified theorem.
Scratch.thy
Email Gateway (Aug 19 2022 at 15:36):From: René Thiemann <rene.thiemann@uibk.ac.at>
And since I already proved soundness (also in a lengthy version), I copied my proof into Lars
file, which now contains the equivalence proof.
Cheers,
René
Scratch.thy
Email Gateway (Aug 19 2022 at 15:36):From: Lars Noschinski <noschinl@in.tum.de>
A little bit of cleanup, but no significant shortening.
Scratch.thy
Last updated: Apr 25 2024 at 20:15 UTC