teorth / qed Goto Github PK

Sometimes there are just too many intermediate items around and they are cluttering the screen.

Maybe an option to remove (as in, "forget") existing items can be added, like dragging an item to the recycling bin. Of course, this might cause key items to be removed, but then it's a conscious option, and it's always possible to immediate undo/restart the proof anyway so it isn't that much of a big deal.

• Items in the environment window can be removed. Also preferrable to disallow removing initial given terms
• Formula can be removed, but those involving operators can only be removed after predicates and operators window is unlocked (so as to prevent making a proof unsolvable). Alternatively, disallow removing initial give formulas is also possible
• Terms can be removed as long as there are no references of them across all windows

I can already see Existential Instantiation being put on the top of the deductions list when a THERE EXIST item in an environment is selected.

There are many other things that should go on top though. Lots of deductions, especially in the formula window, applies to all kinds of terms and they clutter the deductions list very quickly if the term is big enough. Meanwhile I'm already struggling to find which item TRUE/NOT FALSE is at every single time.

Suggestion:

• Acceptable: manually order term-specific deductions before generic deductions
• Better: automatically reorder them when presenting available deductions
• Best: put them into two different divs in the deduction window, separated vertically. Though then the hotkey assignation would have to be revised

Syllogism matching rules are not implemented yet as mentioned in Ex22.8 description, but matching rules for every other law related to THERE EXISTS/FOR ALL (aka the entire Chapter 18 and 22) are not implemented either. This makes for some big inconvenience later on, e.g Ex22.6(b) cannot be used on Ex23.2.

Currently we have to manually create NOT FALSE from FALSE just to put it into an environment. Maybe an option to put NOT FALSE into an environment with just FALSE can be added separately as a convenience?

It should be 2.10.6

It's more helpful to navigate between exercises by going forward/backward instead of just warping into the first/last unsolved exercise. Warping into the first unsolved exercise becomes unhelpful to improving workflow if there is a dangling unsolved exercise behind, as pressing n no longer warps to the next exercise to which I've just solved (which is what I would usually want), but always that dangling exercise.

Suggested hotkeys: Ctrl+Left/Right

e.g Ex 9.5(a) and (b), Monotonicity of AND/OR: while (A AND C) IMPLIES (B AND C) is good, often I also want a version that deduces (C AND A) IMPLIES (C AND B). Otherwise I'd have to find a way to either invoke a AND is commutative or (A AND B) IFF (B AND A), which is inconvenient and actually hard to do as it's very hard to apply deductions to inner pieces under this system (e.g trying to deduce ((NOT (A IMPLIES B)) OR A) IMPLIES ((NOT ((NOT A) OR B)) OR A) is just a huge pain.)

More examples:

• Ex 8.5: A IMPLIES (A AND B); why not also A IMPLIES (B AND A)?
• Ex 10.1(b-e): This should've been weakened to just plain IMPLIES: Why I can only make such deductions from an IFF, but not IMPLIES, considering the former is just the two-way version of the latter?
• Ex 11.1, Ex 12.1(a), Ex 12.3(a), Excluded middle: (NOT A) AND A is just as valid as A AND (NOT A), I think. No need to restrict the order. (The same goes to excluded middle, with AND replaced by OR)
• Ex 12.4(a-b)
• Chapter 13: I'm okay with them not offering the variants actually since they're almost never used after this chapter anyway

Hey Terence,

I'm still halfway through working out the exercises on the old url, is there a way to migrate over to the new page without losing progress?

If you load the page, you'll notice that a bunch of content "flashes" before going away.

I'm guessing this is because the content starts out displayed, and then the JS hides it when first executing. It would be better if it starts out hidden to prevent the flashing.

One easier thing that I think would improve the structure and maintainability of the code would be to store the HTML "notes" and "proof" for each exercise as HTML.

Currently, these HTML strings are stored as JS string literals (in docs/js/main.js), which isn't great for storing "data" and makes it a bit harder to edit and view the HTML. For example:

One idea is to store this information in the form of hidden (i.e. not seen when browsing) "data" divs in the main html file. The structure for each exercise could be something like--

<div id="exercise-3">
<div class="notes">...</div>
<div class="proof">...</div>
</div>

Then a load_exercise_data(exercise, id) JS function could be defined that populates an Exercise object from the HTML document, and this called from within main.js for each exercise. Over time, more of the exercise "data" could be transferred to a more structured form (e.g. the "unlocks" and "unlockedBy" information), until perhaps all of each exercise can be populated from data.

On my blog at https://terrytao.wordpress.com/2018/08/18/qed-version-2-0-an-interactive-text-in-first-order-logic/#comment-504372 a commenter expressed interest in localising the software to other languages. I was wondering what would be a good way to do this. Right now the English text portions of the code are split between the javascript portion of the code and the HTML portion. I could see localising the javascript portion by replacing all text strings with variables and then loading a language-specific .js file that sets each variable to the translation of that string in the given language. Not sure how to proceed on the HTML side though.

EDIT: I guess one could place the text portions of the HTML in a separate language-specific file also. But then how would one change languages when viewing the web page?

Since Exercise.completionMsg isn't so much related to a particular exercise (and is only used once), the Exercise class could be simplified slightly by removing Exercise.completionMsg. Instead, the message could be shown when the number of solved exercises equals one. This is also how completedAllExercises() is already handled (and also makes sense from the perspective that this is a UX issue around how to interact with the user when solving exercises).

Another thing that could be done with this is to move the message text to a div in the HTML, following the pattern of moving more of the text from Javascript (code) to the HTML (textual content).

I was thinking about how to simplify main.js further, and the next thing that occurred to me (using the criterion of easiest, biggest win) is to move the base enumeration of laws to index.html. For the below to work as I'm describing, can all of the Law objects be instantiated before the first Exercise objects are created?

If so, a section could be added to the data container element as follows:

<div id="dataContainer">
<div id="lawsContainer">
<div class="law" id="LawConjunction1">
    <A HREF="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</A>
</div>
...
</div> <!-- End lawsContainer -->
...
</div> <!-- End dataContainer -->

Then, prior to creating the Exercise objects, main.js could have a routine that iterates over the law elements in the HTML and instantiates a Law object for each one.

After that, the JS could loop over an array of triples like the following to set the givens and conclusion on each law:

[
    ["LawConjunction1", [A, B], AND(A,B)],
    ...,
]

What's nice about this approach is that the HTML declaratively does the bulk of the work (which means less code, which is a good thing), and the JS is minimally responsible for only the part that has to be done in the JS (because of how the givens and conclusion are defined using JS functions).

If this works, something similar can be done for the sections and Exercise objects within. (Currently, the reverse is happening for the Exercise objects, with the JS procedurally enumerating the Exercise objects, and the HTML decorating those objects with the additional info. But the idea would be to reverse those roles along the lines described above for the Law objects.)

Has anyone discussed turning this into an iOS app?

The code is free open source so I guess if we want to do that we can just get started?

Thanks very much

e.g I have this:

If I invoke Indiscernability of identicals from a = 1 to (a * b) = (1 * b), I should be able to deduce both (1 * b) = (1 * b) and (a * b) = (a * b) (since 1 is just a term like a and b). However, only the former is available:

I'm pretty sure that if the main page is renamed from QED.html to index.html, then it will be accessible using the simpler and more easily publicized URL https://teorth.github.io/QED/ (because of how GitHub Pages is configured).

If this is done, it will require updating some links in the blog, etc. However, a simple HTML redirect page could also be added for people who already have a bookmarks set, etc.

It seems that the only to reset an exercise (due exercise content changes) is to either modify the local storage manually, or restart the whole game. It'd be good to have a button to just reset the selected exercise.

When you have solved many exercises and go back to the non-shortest ones and try to solve them with fewer steps, the "rules occur in the text at or after the current exercise" trouble a lot.

I suggest adding a setting of not showing these rules.

Or does there exist such a setting but I didn't notice it?

For example: click on "A", click "RESTART EXERCISE", ctrl-click "A", 'From formula "A", formula "A"' will be in the "Available deductions".

DOUBLE DEDUCTION THEOREM Is unlocked by solving 6.2, and 7.1 shortest proof uses DDT, but exercise 7.1 is not dependent on 6.2 for unlock.

Therefore, the shortest solution is impossible for players who jump from 6.1 to 7.1, and the UI gives no indication of why.

Either DDT should be unlocked (silently) by 6.1, or 7.1 should be unlocked by 6.2 instead of 6.1(a)

<div class="exercise" id="EXERCISE-7.1" data-unlocked-by="6.1(a)" data-unlocks="Push PushAlt">
        </div>
        <ol class="proof">
            <li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
            <li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em>, <em>B</em>]. <i>[PUSH (alternate form)]</i></span></li>
            <li><span>From <em>A</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>A</em>). <i>[DOUBLE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
            <li><span>QED!</span></li>

This HTML validator can be useful for finding HTML typos in index.html, etc:
https://validator.w3.org/

This issue can be used for resolving the various issues that the validator finds. The checkboxes below can be used for recording what the validator finds and what remaining things need to be resolved.

• (warning) Add lang="en"
• (error) An ID must not contain whitespace.
• (error) Bad href value: Illegal character in path segment

(I just added a few initial checkbox items after using the validator's "direct input" feature.)

Currently these things will not produce duplicates when being created:

• free/bound variables created by New free/bound variable
• environments (if a conclusion belongs to an environment that already exists, it will go into the existing one)

However, these things will produce duplicates:

• formulas
• terms constructed by predicates/operator window
• conclusions (moreover, doing the same conclusion will incur another step lost)

Ideally, each of the above should not have duplicates. Doing the same conclusion should be a no-op, and arguably doing a step that reaches a conclusion that already exists should also be a no-op?

Predicates takes at least one term and produces a formula. Operators takes at least one term and produces another term.

When the amount of them increases (like the new exercises in Chapter 24), it's not easy to tell which of the items in the predicates/operators window are predicates and which are operators. It'd be nice to separate them into two lists.

This issue is to finish simplifying Exercise creation in main.js.

The steps I suggest are--

1. Finish the exerciseData mapping in main.js, which has a structure identical to the lawsData mapping:

   QED/docs/js/main.js

   Lines 100 to 103 in 699d583

   	// A mapping from exercise shortName to the pair [givens, conclusion].
   	var exerciseData = {
   	"1.1": [[A, B], AND(AND(B,A),B)],
   	"1.2": [[A], AND(A,A)],

2. Add divs of the following form to index.html: <div class="section" id="section-1">Conjunction introduction</div>. These section divs should be placed between the appropriate exercise divs inside the exercise-container div, so that the section headers and exercises are in the same order that they currently appear in main.js:
   

   QED/docs/index.html

   Lines 123 to 126 in 699d583

   	<div id="exerciseContainer">
   	<div class="exercise" id="EXERCISE-1.1" data-unlocks="LawConjunction1">
   	<div class="name"></div>
   	<div class="notes">

3. Add a new data-law="<lawShortName>" attribute for the two Exercise objects that use a prior law when being constructed (namely exercises 18.1 and 18.2(b)):
   

   QED/docs/js/main.js

   Lines 331 to 335 in 699d583

   	new Exercise("18.1", universalRenamingBoundVar);
   	exerciseFromData("18.2(a)", [A, toTerm(X)], forAll(A,X));
   	new Exercise("18.2(b)", universalSpecification2);

4. Change main.js and the exerciseList.forEach() loop to iterate instead over the children of the exercise-container div, similar to how the law-container div is now being iterated over:
   

   QED/docs/js/main.js

   Lines 70 to 74 in 699d583

   	var lawElements = getElement("lawContainer").children
   	for (var i = 0; i < lawElements.length; i++) {
   	var div = lawElements[i];
   	var id = div.id;

   
   If the child has class "section," call newSection(). And if the child has class "exercise," then call exerciseFromData() or new Exercise(), depending on whether the data-law attribute is set.

Reaching exercise 11.1 (through solving exercise 10.1(a)) and clicking A from the formula window does not give NOT(A) as one of the options.

Tested in Chrome 69 and reproduced in Edge 25.

If I open QED webpage using emacs eww browser, it automatically spits out the solutions of all the exercises. It's not that pretty looking though, but it's far more easier to edit it than to solve all the exercises.

Currently the notification window is very useless because it just dumps all the solve status of the exercises. New notifications are also added at the back, so it's guaranteed to be not noticed. Most importantly, they don't actually notify anything. It's more like a "what happened recently" list.

Suggestions:

• Rename it to something else (like "log"?)
• New entries should be added to the front, so they'd actually be visible
• Perhaps should not dump the status of all solved exercises during page load since that's mostly useless

Exercise 24.8 can be proven within 19 lines using cancellation law [after showing (x * (α * 1)) = (x * α), we can directly apply cancellation law].

If there are only rules that occurred at or after the current exercise and you pressed 'c', "no available deductions" is not showed.

To address an issue raised in the blog, I wanted to suggest an easy way to start adding tests that doesn't require installing or learning to use any tooling (e.g. of the kind that professional software developers normally use).

The purpose would be to address the following comment in the "QED version 2.0: an interactive text in first-order logic" blog post:

But writing this text (particularly the first-order logic sections) has brought me close to the limit of my programming ability, as the number of bugs introduced with each new feature implemented has begun to grow at an alarming rate.

The idea is to add a test.html file which, when viewed locally, loads and runs a file called test.js. The test.js file can contain tests of functions in the other JS files (e.g. functions which are more bug-prone or otherwise difficult to get right). To start out, the tests can be simple, hand-coded assertions that raise or display an error on failure. Helper test functions could be added to facilitate making assertions, and test inputs and corresponding expected outputs could be stored in arrays to make the tests more compact.

If a test framework is later added, the hand-coded tests could be adapted to fit into whatever framework is used.