Stream: Beginner Questions

Topic: enumerate all chars and prove exhaustiveness

Chengsong Tan (Mar 01 2022 at 17:59):

Hi community,
I have defined the function all_chars n by converting all natural numbers in the range
[0...n] to chars by the char_of function:

Screenshot-2022-03-01-at-17.56.02.png

How do I prove that by all_chars 256 I have enumerated all possible char values in Isabelle?
This is a bit awkward as it is not constructor type. I tried case_tac and induct with no effect.

Thanks a lot in advance!

Mathias Fleury (Mar 01 2022 at 18:10):

[..256] is a list of int not nats.

Sledgehammer provided me with a proof of a very similar lemma:

  lemma "set (map char_of [0..<(257)]) = UNIV"
    apply (auto simp: )
    by (metis atLeastLessThan_iff bot_nat_0.extremum char_of_char eval_nat_numeral(3) imageI less_Suc_eq nat_of_char_less_256)

Chengsong Tan (Mar 01 2022 at 18:21):

Mathias Fleury said:

Thank you for the reply!
Nice solution, how did you come up with this version of the lemma so sledgehammer actually solves it?
Is there a "nicer" way to prove this, it sounds so simple and should be solvable with some helper lemmas? But where does one
start on such proofs? It feels uncomfortable to be not able to use induction and other strategies but have to rely on sledgehammer to bruteforce it.

Mathias Fleury (Mar 01 2022 at 18:26):

I started as you did: I did a apply (cases c) and wanted to unfold all values (i.e., enumerate all 256 values: it is slow but should work). But that failed because the type was an int...

Mathias Fleury (Mar 01 2022 at 18:27):

So I changed that and called sledgehammer…

Chengsong Tan (Mar 01 2022 at 18:30):

Mathias Fleury said:

So I changed that and called sledgehammer…

Can you think of a nicer way to enumerate chars? I am out of ideas....

Screenshot-2022-03-01-at-18.33.14.png
Something like this wouldn't even parse.......

Mathias Fleury (Mar 01 2022 at 18:38):

The problems comes from the syntax [..256] not the CHR…

Mathias Fleury (Mar 01 2022 at 18:39):

Oh and BTW

 lemma "set (map char_of [0..<(256::nat)]) = UNIV"
    apply (auto simp: )
    by (metis atLeastLessThan_iff bot_nat_0.extremum char_of_char imageI nat_of_char_less_256)

Mathias Fleury (Mar 01 2022 at 18:39):

the 256 bound is not reached

Chengsong Tan (Mar 01 2022 at 18:40):

Mathias Fleury said:

Oh and BTW

 lemma "set (map char_of [0..<(256::nat)]) = UNIV"
    apply (auto simp: )
    by (metis atLeastLessThan_iff bot_nat_0.extremum char_of_char imageI nat_of_char_less_256)

Yes because we start from 0 instead of 1

Chengsong Tan (Mar 01 2022 at 18:45):

Screenshot-2022-03-01-at-18.46.59.png
And somehow it was indeed CHR causing a parsing error.....can someone explain this Screenshot-2022-03-01-at-18.47.27.png ?

Mathias Fleury (Mar 01 2022 at 18:54):

CHR is using the parsing translation and does not make sense without argument

Last updated: Dec 21 2024 at 16:20 UTC