Step theorem display and HTML typesetting

[Raph Levien]

A few updates (pushed to ghilbert-test.appspot.com as well as to the git repo).

First, I've switched entirely over to HTML typesetting, which allows (exp A B) to be typeset as A^B. A nice example is http://ghilbert-test.appspot.com/showthm/expexp (which also shows off the new showthm display).

Second, I've added a prototype of an interactive "step" display for theorems. Go to http://ghilbert-test.appspot.com/showthm/expexp?style=step for example, then use the left and right arrow keys. Each step updates the stack. It's very sparse in terms of UI, but should be good enough to prove out the concept. I'm thinking of adding some more to it:

* Maybe displaying the stack steps consumed (as hypotheses) by a step as well as the new step added. (I'm thinking light red and light green backgrounds, in analogy to diff coloring)

* Display some information about the proof step as well. At a minimum, the shortened description string (as in the listthms display), but maybe a panel that contains the full comment (not that we have many proofs with full comments), the hyps, and conclusion.

My main thinking behind the step display is to make it more intuitive, especially for new users, exactly what happens in a proof step. I've also been enjoying using it to understand a lot of the new theorems that Adam has been proving.

I'm looking into the possibility of storing the proofs in a git repository (with the loose objects and packs as blobs in the App Engine datastore). This is something of an exploration for now (and I just have a local branch), but I'm encouraged so far. The idea of having sha1 hashes of immutable versions solves a lot of problems with caching. The existing architecture flat out will not scale to handling a translated version of set.mm (which is something I want to do soon), and even with the current repo is slow-ish. Caching expensive stuff, like lists of all theorems in a .gh file, while only doing the incremental work necessary, is the win. There are other ways to do it, of course, but I want to see if the git approach is workable.

Raph

[frederic.line]

Hi Raph,

it is very interesting. It definitely adds the dynamic that is absent in metamath.
And the new infix/postfix notation addresses the problem of the ghilbert
prefix notation that is not human friendly at all
(even if I understand it is what a machine can prefer).

--
FL

Une messagerie gratuite, garantie à vie et des services en plus, ça vous tente ?
Je crée ma boîte mail www.laposte.net

[Raph Levien]

Thanks, I'm glad you find it interesting.

Proper typesetting, as the main way users view proofs, has long been the goal, and I've had prototypes working for a while (check out this screenshot from 2006: http://wiki.planetmath.org/cgi-bin/wiki.pl/Ghilbert_app_screenshot). But I think this is the first time someone on the web has just been able to click on a link and see the proof.

The goal is not 100% complete yet, because you're still seeing s-expression results in the mandatory hypotheses (ie bindings of variables that appear in the conclusion but none of the actual hypotheses). I think it's okay for now, but going forward there are a couple of things that could be done. One reasonable thing would be to parse typeset math into s-expressions, so the user could be working entirely with typeset math. Another, kinda more radical, is to get rid of mandhyps, as they can be inferred (down to the names of dummy variables, anyway) through unification of the entire proof. We've had discussions about this before and I wouldn't be surprised if a prototype happens.

Parsing typeset math has a few more implications. I've also given some thought to a theorem prover (although the first version would be based on brute force search rather than anything smart, so would only be good for short snippets of proof). That would work best by taking a want-to-prove, for which the best UI would be typeset math. Of course, even without that you could make the same observation for the hypotheses and conclusion of the theorem.

Another observation is that, for it to work fully, the text input would need to graduate from a textarea to a contentEditable, as I believe the former can't handle stuff like exponentiation. (I'm also interested in implementing stuff like highlighting to give better interactive response). However, contentEditable also seems a lot less robust, for example I've had mixed success at best with Android browsers. So I'm not sure what the best thing to do is here, and will defer it a bit, at least until I've got a lot more of the basic functionality working.

Take care,

Raph

[fl]

Second, I've added a prototype of an interactive "step" display for theorems. Go to http://ghilbert-test.appspot.com/showthm/expexp?style=step for example, then use the left and right arrow keys. Each step updates the stack. It's very sparse in terms of UI, but should be good enough to prove out the concept. I'm thinking of adding some more to it:

I definitely really like this feature. I really regret metamath has not such a viewer. It really helps read a proof. I wonder
if it is difficult to code?


 

* Maybe displaying the stack steps consumed (as hypotheses) by a step as well as the new step added. (I'm thinking light red and light green backgrounds, in analogy to diff coloring)

* Display some information about the proof step as well. At a minimum, the shortened description string (as in the listthms display), but maybe a panel that contains the full comment (not that we have many proofs with full comments), the hyps, and conclusion.

Yes that sounds good features to add.
 

My main thinking behind the step display is to make it more intuitive, especially for new users, exactly what happens in a proof step.

It can help  expert users read the proofs as well. It is often difficult to read a proof. This interface is a nice idea.

--
FL

[Marnix Klooster]

Hi Raph,

That really looks nice.  Especially the interactivity is helpful.  And from some experimenting, it would indeed also be helpful to also show the steps consumed.  (Diff coloring is nice, also think about color blindness, perhaps additionally indent the red consumed steps?

This reminds me of a different (non-interactive) approach to rendering Metamath/Ghilbert proofs that I've (on paper) experimented with in the past: rendering a proof as a "structured calculational proof".  Basically, this is the proof format designed by Dijkstra/Scholten (see, e.g., EWD1300) extended to allow subproofs (http://users.abo.fi/jwright/schoolmath/).

I think one could automatically (helped by some annotations) generate something like this: https://stackedit.io/viewer#!provider=gist&gistId=11459583&filename=Ghilbert%20expexp:%20structured%20calculational%20proof

(For other examples and discussion, see http://wiki.planetmath.org/cgi-bin/wiki.pl/metamathCalculationalProofs.)

Comments?  Would that be useful?  Would anyone want to spend time in implementing something like this, for Ghilbert or Metamath?

Groetjes,
 <><

Marnix

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
Marnix Klooster
marnix.klooster@gmail.com

[fl]

 

Comments?  Would that be useful? 

 

I think it can help read the proofs. After all you normally read the proof dynamically. You begin at the end.

and then you want to see what are the hypotheses you need to prove (and the theorems that will

be applied to them). Next you apply the referenced theorem to the last hypothese on the stack and

see what the stack become and so on. And obviously, as it has been done by Raph, you need to

see where you are in the proof exactly. So both views are needed the evolution of the stack (and the

theorem that will be applied to each hypothese) and your position in the overall proof.

 

That way I think you can grasp the proof easily.

 

(The steps of the proof that are of a syntaxic nature are not needed obviously.)

 

--

FL

[Paul Merrell]

I think there's a way to do what you what with the current UI. I tried rewriting the expexp theorem to get closer to what you're looking for. See if you like this any better.

I actually wrote it two different ways. The first emphasizes the inductive step:

http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/expexp

http://ghilbert-app.appspot.com/peano/peano_thms.gh/expexp

The second may be closer to the original

http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/expexp2

http://ghilbert-app.appspot.com/peano/peano_thms.gh/expexp2

I left the old one here http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/expexpOld

I've also updated the UI for showing the theorems and the code together. I've attached a screenshot. I've checked in the code, but it's not live on appspot.

Paul

--

[fl]

I left the old one here http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/expexpOld

It's very, very beautiful.I'm very impressed. I need several days however to explore the proof in details

and compare it with its original version (I don't have internet at home).

However one first remark. I think the original design has its own value and should kept alive.

-- 

FL

[Raph Levien]

I'm a big fan of Dijkstra's calculational proofs, and feel they have advantages over the "natural deduction" style that seems so much more popular in automated theorem proving land. In particular, I like proving equivalences when they are equivalent, rather than two separate implications.

I'd love to see more work in nicer automatic presentation of Ghilbert / Metamath proofs. Unfortunately, I'm so busy with my Android work these days that I have barely any time for Ghilbert, so someone to implement this probably won't be me, at least for a little while anyway.

Raph

--

[Paul Merrell]

I haven't looked much into calculational proofs. I don't really understand what they buy us that isn't already in the existing UI for Ghilbert. I wrote two proofs that follow the proofs in Dijkstra's paper:

http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/calculational0

http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/calculational1

He talks in the paper about removing redundant statements, but we're already doing that. If the same expression repeats itself on the left it's hidden. I'm not sure what is missing from the current design.

This example does actually highlight an important problem with the current system and maybe this what you're referring to. The two theorems actually prove different things. calculational0 proves the conditional:

     xy = y ∧ yz = z → xz = z

whereas calculational1 proves that from the two hypotheses:

    xy = y

    yz = z

we can conclude that

    xz = z

These are in fact different. It is trivial to prove calculational1 from calculational0 using modus ponens, but it is impossible to prove calculational0 from calculational1. So calculational0 is a stronger theorem, but it's less concise as Dijkstra says and the proofs are larger and more difficult to write this way. And they also make other proofs longer whenever they're used. This problem occurs all over Metamath and Ghilbert. We have two versions of many of the proofs. Often we attach an "i" at the end of the name for the "inference" version meaning the version like calculational1 with hypotheses.

I've thought a lot about this problem and I think there's a solution that wouldn't be hard to implement. Suppose that we proved a theorem with two hypotheses:

    ph -> xy = y

    ph -> yz = z

and the conclusion

    ph -> xz = z

This is the same as calculation1 except we've added an arbitrary wff ph as a conditional. This theorem is as strong as calculational0 and calculational1. To prove calculational1, replace ph with a true statement. To prove calculational0, replace ph with xy = y ∧ yz = z. The hypotheses become: 

    xy = y ∧ yz = z -> xy = y

    xy = y ∧ yz = z -> yz = z

which are always true and so we are left with the conclusion

    xy = y ∧ yz = z → xz = z

which is calculation0. In this new scheme, you would have the conditional "ph ->" in front of every statement in the proof, but we can hide this. We could create a special wff variable that is always hidden when it appears in front. (We'd probably call it something other than "ph"). We would then have the best of both worlds, the proofs would be as powerful as the condition in calculational0 and they would be as concise as calculational1. Furthermore, if you can prove the theorem without the "ph ->" part, you can prove it with it. It adds no complexity to the task of writing the proof.

Paul

[Adam Bliss]

On May 5, 2014 1:59 PM, "Paul Merrell" <pa...@merrells.org> wrote:

> This example does actually highlight an important problem with the current system and maybe this what you're referring to. The two theorems actually prove different things. calculational0 proves the conditional:
>
>      xy = y ∧ yz = z → xz = z
>
> whereas calculational1 proves that from the two hypotheses:
>
>     xy = y
>     yz = z
>
> we can conclude that
>
>     xz = z
>
> These are in fact different. It is trivial to prove calculational1 from calculational0 using modus ponens, but it is impossible to prove calculational0 from calculational1.

Actually, I'm not sure about that. Check out this page:

http://us.metamath.org/mpegif/mmdeduction.html

(I had to read it many many times before it started to make sense to me.)

[fl]

http://us.metamath.org/mpegif/mmdeduction.html

(I had to read it many many times before it started to make sense to me.)

Deduction theorem Adam !  You don't make enough proofs !

-- 

FL

[fl]

I'm a big fan of Dijkstra's calculational proofs

The problem is not calculational proofs (that, in my opinion are moderatly interesting) 

but the revival of an interface that you had created for

ghilbert and which should be completed because it is a very nice interface that can help us

read the proofs more easily.

-- 

FL