Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized

On 10/28/2012 11:58 PM, Christian Sternagel wrote:


The most important question: What is your actual application anyway?

This was your second to the last question. You say it's the most important, so I move it up here, since I get wordy below.

The application is implementing certain mathematical textbooks in Isabelle, until I get to a level to where I use Isabelle to implement original research.

The style is educational, textbook writing. Discussion, example, theorem, proof, exercise, repeat. The original research part will be the hardest part to achieve, especially because it will be so time consuming to build up to that level. I at least try to end up having made an educational contribution.

"Hypothetical application" would be a better phrase to use. Applications require work, and I don't get paid for this. Financial incentive is one of the best motivators for working, where there would be two halves to "financial incentive", the reward of income for producing, and the fear of the loss of income for not producing. I have neither to motivate me.

My point here is that you are investing a lot of time to reinvent the wheel (moreover a somewhat square wheel that people won't put on their own cars; sorry for that ;)).

The wheel has largely been invented, but the wheel has been optimized for those who invented the wheel, and for those who have made significant technical contributions towards getting the wheel rolling.

Let us call this group of people Professional Software Developers (PGD). Given limited resources, we can say that the choices made so far by the PGD in optimizing the wheel have been the best choices made, seeing that the PGD are currently the primary users.

Myself, I'm not a PGD, so the wheel is not completely optimized for my needs. As to users, at times, I prioritize myself as the most important user.

My suggestion (just my personal opinion): Keep the actual THY-file as clean and simple as possible.

Well, it's not possible to tap into the power of LaTeX, or something similar, and have a primary source code file that's super clean.

You can achieve clean, but then there's cryptic, where, in my opinion, "cryptic" would currently describe almost all of the Isabelle/HOL distribution source, and the source on the I'm not complaining here. I'm just talking.

However, as I said, I'm out to cater to the market. For you, in the future I will easily be able to give you a THY which is nothing but theorem code, proof code, theorem code, proof code, with some of my comments in the proofs. Will it turn out that you're annoyed by my comments? Not a problem. I'll strip them out and give it to you as cryptic as you want, or someone like you.

It's best not to annoy people who help me out.

For a proper presentation of theories there is already Isabelle's document preparation system which works very well for LaTeX. No need to cook up your own variant. (What people often do when they want to publish some Isabelle formalization is to start another theory that imports the actual formalization and write their paper/article in this new theory, referencing facts from the previous formalization. Of course it depends on the audience, what the best solution is. E.g., for mathematicians I would mostly hide Isabelle related stuff and instead of presenting the sourcecode of the actual formalization, just reference facts - using Isabelle's antiquotations - and give textual overviews of the formalized proofs which convey the main ideas.)

Last year I worked for a month on trying to switch over to Isabelle document processing. It didn't work out. I didn't figure out a way to put all THY Isar code in a verbatim environment. I don't explain why here why I want to do that.

It's my intent to make mathematicians my primary audience, but on your point of hiding things, my conclusion is the opposite of yours here. (With all this, opinion heavily comes into play, and my opinions are subject change, so feel to disregard anything I say here.)

Actually, what I say here is based on my own preferences, where I've been greatly influenced by the culture of mathematicians.

Proofs are everything, and as a symbol of rigor, a certain amount of detailed proofs are expected, and they're expected to be written in such a way that they can be read, where "be read" will vary with the audience, such as from 1st year university level to Ph.D.

If I'm hiding the details of all the proofs, then why am I even presenting the math by means of Isabelle? Why not just do things the traditional way? You may say, "Because if you prove something in Isabelle, it shows them it's legitimate for sure." But no. It'll prove nothing to them. What is not presented to mathematicians as literature with proofs that they can read, they will not be interested in.

Paul Erdos,, had no interest in the proof of the Four Color Theorem:

Concerning your markups in order to process THY files with scripts. In your example THY file I do not see what additional possibility your markups give, since they always accompany existing commands like "section", "subsection", "definition", ... which could as easily be recognized my scripts.

When scrolling through a long document, for the major textual items, I want to answer 4 questions fast: What is it? What's it going to tell me? Where does it start? Where does it end?

With the Latex theorem environment, you can create your "Definition", "Theorem", "Postulate", etc, and the environment formatting helps separate things. Unlike with a Latex theorem environment, In the midst of lots of other Isar keywords, a Isar keyword like "theorem" doesn't stand out that well, and it doesn't always describe how it's being used.

(Yes, "theorem" could be used for a theorem, but where are keywords like "example", "exercise", "remark", "postulate". And you wouldn't want all those keywords in Isar. I made a very weak attempt to ask Makarius to allow us to define our own outer-syntax keywords in Isar. I decided that would be a bad idea. It's the limited number of keywords that standardize the language.)

Consider my COUNTERX. My COUNTERX is a conjecture for which I've found a counterexample. The keyword "theorem" doesn't accurately describe how I'm using "theorem". So suppose I say, "Okay, I have that counterexample above, and I need to scroll up and look at it again." Also suppose I have 8 theorems up above. Well, the keyword "theorem" does nothing to help me quickly locate my counterexample.

Suppose I have 4 counterexamples. The Isar keywords alone don't help me distinguish between them. Even a named theorem doesn't always tell me quickly what a theorem does. With the following, I get 4 pieces of information in the first two lines:

COUNTERX (Shows P is false with input z and y.)
theorem false_p:
"a big long hard to read formula that would take me a long time to know what it's about"
  --"Nitpick counterexamples that make it false"

The capital bold COUNTERX helps me skip a whole lot of other stuff fast, like definitions, axioms, theorems, lemmas, etc.

The short description gives me a quick summary of what to expect.

Descriptive theorem names are desirable, but not if they're 10 words long, so I don't want:

   theorem shows_P_is_false_with_input_z_and_y.

That's hard to read and would be even worse to reference in some other command.

All this is personal. If you work different, then you'll consider my tweaking a waste of time.

Maybe there is already existing infrastructure which could achieve the same goal more easily.

Sometimes, though, I just do what I've been doing, after making some initial attempt to make a change that didn't work out.

I know that there's a lot of power in Isabelle's document processing, but I consider it to be less risky to continue down my own non-standard route.

Thanks again for that proof, and documenting the low-level quantification that's occurring.




On 10/28/2012 05:46 PM, Gottfried Barrow wrote:

Now on to your complaint about my creating noise and clutter in my THY.

Working on trying to better reduce noise and clutter is half of what I
got out of sending off this email. The other half is learning about the
usefulness of locales to do some preliminary proofs without globally
injecting all the overhead into the THY.

Back to noise and clutter, the challenge is to find a way to mark up
THYs in a way that is reasonably readable, and which can also be
processed with scripts to generate other THY and TEX files to give
people options on how they want to absorb the information.

For mathematical writing, I think there are four main components,

1) Section headings
2) Text/discussion
3) Statement of theorems, definitions, axioms, etc.
4) Proofs

A big part of LaTeX is the newtheorem environment:

I'm trying to duplicate a decent imitation of the newtheorem environment
in the THY file, without creating too much clutter and noise, and not
fall prey to the "gaudy web page syndrome".

It's not obvious how to use a limited set of tools to get something
better than the traditional way of doing things.

Sometimes you don't get something better. There was Xerox. And there was
Apple. It's the story of Apple taking new ideas and refining the new
ideas in significant ways, and doing it with hardware limitations.

I attach my newest attempt to edit my THY so that I can convert my cheap
newtheorem imitations into the real thing with a script, among other
processing. The source code of a marked up language isn't meant for
public consumption, but if the public can consume the source code,
that's a good thing, because then it means you can probably read your
own source code.

Christian, thanks for the help.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.