Yiran Duan (Feb 06 2025 at 15:09): Yiran Duan (Feb 06 2025 at 15:09):Hi! I'm using the keyword abbreviation for some frequently used complex constants in my code, in the hope to improve readability of the code. But the abbreviations are automatically expanded in proof state, making it hard to read. Is there a way to disable the expansion of abbreviations in the proof state? Or, what is the best practice in such case?
Yiran Duan (Feb 06 2025 at 15:43):I have tried with definition instead of abbreviation, and add the definition to the simpset of proof or unfold the definition wherever needed, but I don't think this is the best solution because I would need to do that very frequently, however as I understand, definition's are not supposed to be unfolded anywhere.
Mathias Fleury (Feb 06 2025 at 16:08):abbreviations are not unfolded. They are folded in during printing. Hence, if they disappear in the output, it means that they could not be folded in
Yiran Duan (Feb 06 2025 at 16:27):Mathias Fleury said:
abbreviations are not unfolded. They are folded in during printing. Hence, if they disappear in the output, it means that they could not be folded in
Thank you! I wonder why they could not be folded in. I compared the strings printed in the proof state and the abbreviated constant expression itself, they are exactly the same. I have no knowledge how the printing works. Is there anything I can do to make them possible to be folded in during printing?
Mathias Fleury (Feb 06 2025 at 16:30):copy paste the part that you want to be folded A, put it into a lemma of A = abbreviation and see if they are really equal. You should find a minor difference (like a typing or something like that)
Yiran Duan (Feb 06 2025 at 21:09):I tried such lemmas, they can be proven by e.g. blast. And I think I can rule out typos since they always appear as a whole and I always use the abbreviations only.
Mathias Fleury (Feb 07 2025 at 06:09):no no no
Mathias Fleury (Feb 07 2025 at 06:09):the important thing is not that it is proven by blast
Mathias Fleury (Feb 07 2025 at 06:09):the important thing is that the abbreviation get folded in immediatly
Mathias Fleury (Feb 07 2025 at 06:09):and that apply (rule refl) is able to prove it
Mathias Fleury (Feb 07 2025 at 06:10):You need stuff on the left and the right to be identical
Mathias Fleury (Feb 07 2025 at 06:10):if they are not identical, folding will not work
Mathias Fleury (Feb 07 2025 at 06:16):that includes associativity of operators
Yiran Duan (Feb 07 2025 at 08:56):Mathias Fleury said:
and that
apply (rule refl)is able to prove it
Yes, I confirmed that one singleapply (rule refl) can directly prove it
Mathias Fleury (Feb 07 2025 at 15:22):then it is really strangle that it is not folding
Mathias Fleury (Feb 07 2025 at 15:23):can you show the abbreviation and the term you have?
Yiran Duan (Feb 07 2025 at 15:42):Sure, and I just realized that the issue won't occur if I define the abbreviation outside of the locale -- is there anything I should know about locale and abbreviation?
image.png
Mathias Fleury (Feb 07 2025 at 16:14): Mathias Fleury (Feb 07 2025 at 16:17):basically, there are issues that can arise with locales and abbreviation (there are more posts on the mailing list, but the archives are gone sadly)
Yiran Duan (Feb 07 2025 at 17:39):Mathias Fleury said:
basically, there are issues that can arise with locales and abbreviation (there are more posts on the mailing list, but the archives are gone sadly)
I see, thank you very much!
Last updated: Mar 09 2025 at 12:28 UTC