Stream: Beginner Questions

Topic: String inequality with show

view this post on Zulip Maximilian Vollath (Feb 13 2025 at 14:09):

I'm trying to generate unique strings and thought the best way might be using Show. However, I'm having a hard time understanding the implementation and got stuck here:

theory String_Shenanigans
imports Main "Show.Show_Instances"
begin

lemma
  fixes a :: nat and b :: nat
  assumes "a ≠ b"
  shows "show a ≠ show b"
  oops

end

view this post on Zulip Maximilian Schäffeler (Feb 17 2025 at 20:38):

I don't know whether there's a better way to achieve your goal of generating unique strings than via show.
However, I tried to prove it myself just for fun, so here you go:

Proofs

view this post on Zulip terru (Feb 18 2025 at 15:56):

if it's not important how the strings look like, how about just replicate a CHR''a''? Then even simp can prove they are distinct:

lemma "a ≠ b ⟹ replicate a CHR ''a'' ≠ replicate b CHR ''a''"
  by simp

view this post on Zulip Maximilian Vollath (Mar 03 2025 at 16:16):

@Maximilian Schäffeler That's awesome, thank you!

view this post on Zulip Maximilian Vollath (Mar 03 2025 at 16:18):

terru said:

if it's not important how the strings look like, how about just replicate a CHR''a''?

That's what I ended up doing as a band-aid, you're right. I just wanted it to look cleaner.

Last updated: Mar 09 2025 at 12:28 UTC