Extend the user guide, and link to it from the README

[david-a-wheeler]

This extends the user guide to walk through the simple example ( 2 + 2 ) = 4, as well as significantly expanding the functionality it covers.

[expln]

This is a lot of work! Thanks David! I reviewed and left few comments. Many of them are simple typos. However, some of them are touching more complex things related to my vision of how this guide may be used and understood by newcomers. And sorry for incorrect order of comments. This is the first time I am doing a review on GitHub. I have not figured out that I have to first start reviewing, then add comments and finish reviewing at the end. So probably you received a lot of email notifications instead of a single one.

[david-a-wheeler]

I'll post soon an update with the fixes.

[david-a-wheeler]

Here's an update, I think I addressed all your recommendations.

I also changed how I proved 2+2=4 a little bit. I still expand 4=3+1, then 3+1=(2+1)+1. However, the change is that I immediately "clean up" by showing that "4=(2+1)+1". This is probably a better general practice when proving forwards, and it makes the explanation clearer.

[expln]

Great! Thank you!

The new sequence of proof steps especially with detailed explanations of why we are doing something is much more clear for me now. Introduction of duplication action demonstrates one more feature and simultaneously removes one "select/unselect qed". Moving bottom-up proof to the end makes an impression of gradual introduction of new features which in general should make reading of this example more "memorable" (as for me).

I am not sure how you are going to proceed with updating of this guide. But now it looks complete in terms of introduction and the first example. I would appreciate it if you could fix new comments (mostly typos) and I then would complete the PR, and then you could create a new PR for further changes. This will allow me to review new changes more conveniently.

Thanks a lot!

[david-a-wheeler]

I am not sure how you are going to proceed with updating of this guide.

I have some thoughts for next steps after this PR is merged. Here is my current thinking:

Make it clear that this document is a "guide" that contains both a "user's guide/tutorial" and a "reference guide" (which walks through the UI and explains things in detail).

In the document itself, the first major section will be the user's guide which walks through a few examples, using 2+2=4 as the template. I think 2+2=4 should be the first one; it has no variables or disjoints, and involves knowledge that a grade schooler would understand. I intentionally didn't include partial selections in 2p2e4 so it doesn't introduce too many new concepts.

I'd like to add reccot to the set of examples, maybe the second or third example. Hopefully we can "steal" the text you've already written.

Currently there's a section for "more examples" at the end of the document, but I now think that all the examples should be at the beginning. That way, a new user can just sit down with the document, go through the worked examples (preferably by doing them), and understand how to use the tool. Once the tool has had some changes (as you're planning), I'm thinking about making a video from the 2p2e4 example.

The rest of the document is already the reference guide. There are a few sections not filled in ("TODO") that need filling in. In some cases they're TODO because I don't know the answers. In particular, I'm not sure what some of the proving bottom-up options are exactly about. Feel free to fill in any TODOs, and I can comment or suggest further improvements.

[expln]

Ok. Thanks David. I merged the PR. I will read and reply to your comment a bit later.

[expln]

I think 2+2=4 should be the first one

I agree, it seems to be an excellent first example.

Hopefully we can "steal" the text you've already written.

Not sure what text you mean in the context of reccot example. All my two videos about reccot were with no sound. But if you mean the sequence of steps shown in the video, then yes, please do :)

Feel free to fill in any TODOs, and I can comment or suggest further improvements.

Sure, will do!