Feature request: Tutorials for basic proofs

[littlebenlittle]

Hello, I just learned about this project and Globular. It's really exciting to see a proof assistant for HoTT!

It would be valuable to see some example proofs for those of us who are coming from a set theory background and still learning HoTT. For example defining the addition of natural numbers and proving associativity.

I'd be glad to contribute to the writing, but I'd need some guidance on the theory.

[jamievicary]

Hi Ben thanks for your message! It's great that you like the project.

This proof assistant is a proof assistant for finitely-generated infinity-categories (or infinity-groupoids). It is therefore related to HoTT, since that HoTT is an "internal language" for the (infinity,1)-category of infinity-groupoids. However, the mechanisms that the two systems yield are quite different. In homotopy.io, the only allowed constructions are composition of generators, using the composition structure in the infinity-category (or infinity-groupoid), and homotopy construction, while HoTT allows in principle much more general constructions.

Taking your example of the natural numbers, that is not equivalent to a finitely-generated infinity-groupoid, since it has an infinite number of objects. As a result, it can't be expressed in homotopy.io.

To illustrate what can be done in homotopy.io, we are very much overdue making examples and tutorials available, and hope to get that done this summer. However for now you can look at the examples subdirectory of the repo.

[littlebenlittle]

Thanks, I think that makes some sense. I will need to do some reading about infinity-groupoids to better understand what does and does not fit that definition.

[kram1032]

@jamievicary you can absolutely define (finite) natural numbers in terms of Peano axioms and "0" and "Suc". It's tedious but possible.

For instance, this is what "1" might look like

And it's as simple as this to define additon:

"Add" (in green) simply consumes "Suc" one by one and puts it above until it hits a "0" etc.

I did a much more complicated and complete version of this in Globular, defining Rationals via two copies of whole numbers which in turns were built from two copies of natural numbers plus a function to normalize them.

The part where I got stuck on was how to reduce rationals to the simplest fraction, and doing even very simple fractions just takes a lot of wire manipulation, but it can all be done.

Not sure that's what @littlebenlittle had in mind, but that approach works since you have a finite set of primities (0, Suc, Add, Multiply)

[kram1032]

Peano Arithmetic.zip

I didn't prove anything yet but here is an implementation of basic Peano Arithmetic featuing addition and multiplication. I think to prove that those two are commutative, associative, and distributive, you'd have to show how various cells involving a 0 or a succ on each input are the same thing. Might require allowing some things (i.e. add 0 L and add 0 R) to be invertible

EDIT: Ok I think I see a limitation that makes a proof of commutativity or associativity tricky/unsatisfactory/impossible depending on what exactly you want:

I can sort of prove, that 0 + x = x + 0 and that Suc x + y = Suc (x + y) = x + Suc y, but that requires explicitly marking stuff as inverse where you might not want this. And I also can't prove the thing I really want, namely that

=

=

which would be proper full "point free" commutativity, because I have no way to do proper induction. Commutativity at best can be proven for each element type (0 and suc) individually, and it can be explicitly declared to hold, but I can't use the two separate pieces for each case to conclude that it works regardless of the case, which makes this property far more annoying to use than if I had the point-free version: It'd only work if I move a 0 or Suc into the right spot, rather than entirely locally as the declared version might.

And a similar problem ends up happening for associativity. What I'd like to prove in that case is that

=

which is again easy to declare but not exactly to prove in a satisfactory way.

And to even get the limited proofs of commutativity and associativity to work, I have to promote a few things to being invertible: The reduction rules of Add and Multiply need to be inverted and then you need to apply the mirror image of the now inverted rule to conclude your proof.

The unit proofs are much simpler and I could do those no problem. I have separate versions for the left and the right unit, rather than proving one of the two sides inductively.

[littlebenlittle]

Thanks, @kram1032 , the definition of zero and suc was as far as I got in my attempt! And your statement of associativity looks very similar to what I've been doing by hand, very informally. I will play around with this some more now that I'm more confident that what I want to do is possible.

[littlebenlittle]

Okay, on closer inspection I think the problems you mention are related to an issue I have been running into with my paper-and-pencil depictions of dependent type theory. Namely I have no good way to represent induction diagrammatically. I have to declare induction as a sort of external judgment where a universally quantified proposition over a type is inhabited by a tuple of proofs for each constructor for that type. It's a very awkward notation.

This makes me wonder if induction is a "natural" part of type theory.

[kram1032]

Yeah, it's really just a matter of, given a bunch of rules that cover all available cases (which is a kind of "pointed" way to do things, as, in the way natural numbers are constructed here, I need to have the relevant vertices Suc/Zero in the context of a rule), I'd have to be able to conclude that I can use the "point free" version of the rule (no longer having a Suc/Zero in the context)

However, with the current feature set, that clearly can't work: There is no way to declare stuff like "these are all there are" - I could just simply add another cell at any time, which doesn't work with commutativity or associativity, which would immediately invalidate the "point free" version.

To "solve" this, I'd have to be able to say "there is only ever these two kinds of vertex, so if I prove something for each of them, I prove it in general", but I bet the fully general version of that (across any conceivable construction of cells) is really tricky.

It'd roughly have to be, that, given a fixed set of "input" cells and some "operational" cell, if all "inputs" to the operation end up with a common sub cell after the transformation, then that implies the "operational" cell can be directly transformed into this sub cell without even looking at the "inputs".

I wonder if there is a better way to phrase that. But I think that'd effectively be what induction ought to be for arbitrary combinations of cells.

Note, that it is possible to define Fix, the fixed point operator, aka the Y-combinator as found in combinator calculus (using this same sort of vertices on a wire method to do so) You could use that for an induction principle, defining Peano Arithmetic in a combinator calculus instead. You can also define the very neat interaction combinators just fine.

Here is the Y-combinator:

And I think Fix can be used for induction, right? But I don't think that can be used to resolve the issue of proving stuff in a "point-free" manner....