27
$\begingroup$

In some of my works I need to prove some results within the internal logic of categories with not much structures (like pretoposes or even just categories with finite limits). The kind of things I want to prove typically involve manipulating inductive type (like a natural number object, a type of binary tree, some W-types etc...) and prove some of their properties in these relatively weak categories.

Let me give some examples of the sort of results I'm interested in:

  • If C is a cartesian category (or category with finite limits) with a parametrized natural number objects $N$ then $N \times N \simeq N$.

  • If C is a cartesian category with a (parametrized) natural number objects $N$, then $N$ is also a parametrized list object for $N$, and a parametrized finite tree objects.

  • If C is a pre-topos with parametrized list objects then essentially any kind of finitary free constructions (like free groups, free monoids, free left exact categories etc...) can be performed.

  • Which of these free construction can already be performed in a cartesian category/ a category with finite limits/an extensive category ?

  • If C is a a pretopos in which some (non finite) objects are exponentiable, and for which the corresponding W-types exists, then certain free infinitary constructions exists.

etc... those are only examples, most of them are already well known results, but they are very typical of the kind of things I'm trying to do. Note that I want to work with "internal" proof, and not proving results externally directly in terms of such categories.

I believe that this sort of things is typically a good place to try to use a proof assistant as the proof have to be spelled out in a very high level of details anyway and one can easily makes mistake.

So I'm looking for a proof assistant that would be appropriate for this.

I already started experimenting in Coq. My current strategy is to just be careful about what I'm doing: for example, only use induction principle for propositions without quantifier, or only those authorized by the specific framework I'm working in... And of course not use anythings coming from a library, and only use very explicit tactics to avoid hiding possible problems. So I'm not really using the proof assistant as a definitive witness of validity of a proof, but only as somethings that makes every single step of a proof explicit enough so that I can tell immediately if it makes sense or not in the framework I'm interested in.

This already not too bad, but I was hopping to find a more precise/formal way to do this.

  • Is there other proof assistant which have more flexible logical background ?

  • From my experience (but I'm not very familiar with the precise logical framework that Coq uses, so I can't makes what follows a formal statement, but if someone can confirm it it would be very helpful) everything that I can define in coq can be interpreted in a 'Stack' or 'Sheaves' semantics over the category I'm working in. So the only thing that I need to be careful, is to not apply an induction principle to construct functions into something that is not an object of my category. So would there be a way in Coq, or in any other proof assistant, to say that I have a nice class of sets (which would be the representables), stable under some operations (corresponding to the structure I'm putting on my category) and that when I define inductive operations or use inductions it has to be restricted to things taking values in a set in this class. But I would still like to be able to use the nice machinery of "match" "induction" "fixpoint" that Coq offers. Maybe a way to check afterward what kind of induction does a given proof uses ?

  • Any other suggestions on how to do this sort of things ?

PS: I was unsure this question was suitable for MO or not. I had the impression it was "mathematical enough" but I do have too admit that a good answer could be something technical about the inner working of some proof assistant. So If you think there is a better place to ask this question, please tell me.

$\endgroup$
  • 5
    $\begingroup$ This is a very good question! $\endgroup$ – David Roberts Mar 8 '18 at 3:15
  • 1
    $\begingroup$ Have you considered using Agda[wiki.portal.chalmers.se/agda/pmwiki.php] -- it allows unicode mixfix identifiers thereby rendering one's formal proofs as not much more work than a LaTeX rendition ;-) An impressive number of categorial results have been proven as used by Wolfram Kahl; e.g., see his RATH-Agda repo: relmics.mcmaster.ca/RATH-Agda/RATH-Agda-2.2.pdf $\endgroup$ – Musa Al-hassy Mar 8 '18 at 13:08
  • $\begingroup$ I have not. But I will look at it. Thanks for the suggestion $\endgroup$ – Simon Henry Mar 8 '18 at 13:11
  • 1
    $\begingroup$ @MusaAl-hassy In some cases, formal proofs in Agda are easier than in Coq, but in other cases the reverse is true, and in my experience anything reasonably complicated is much more work in both cases than it would be to write it in English. I don't think the difference has much to do with mixfix either; Coq's Notation commands also allow mixfix in a different way, and the real difference is that Coq allows tactics while Agda requires you to write out all terms explicitly. $\endgroup$ – Mike Shulman Mar 8 '18 at 17:30
13
$\begingroup$

One possibility that's worth thinking about is to use a "meta-proof-assistant" like Twelf, which implements a meta-theoretic logical framework inside of which you can specify any "object language" you like. It's better-adapted to proving meta-theoretic properties about the object-language, but it can also be used to prove theorems in the object language, although it doesn't have nice syntactic sugar like match and fixpoint or support for tactics.

It might also be possible to implement the type theories you're interested in inside of Isabelle or something like it, which is supposed to be a "generic proof assistant", but I'm not very familiar with that.

Regarding Coq, I don't know of an "after the fact" way to check what kind of induction a proof uses. But if you're willing to call induction principles explicitly rather than using match/fix, you could use a "private inductive type" hack similar to the way that we implement HITs in HoTT. That is, postulate your family of "representable" types and its closure conditions, then define your inductive type as a Private Inductive in a module, prove a version of the induction principle that requires the target to be representable, and then export only that restricted induction principle.

$\endgroup$
  • $\begingroup$ Thank you very much for the suggestion. that will definitely take me some time, but I'll look at them. The first two sound very interesting. For the last one I thought about trying to do something like it, I'm not very well aware of the possibilities that coq provides yet : do you believe that with the feature of "notation" and the creation of tactic available in coq, one can reproduce satisfying analogue of the match/fixpoint/induction from hand made induction principle ? $\endgroup$ – Simon Henry Mar 8 '18 at 20:37
  • $\begingroup$ Well, I find the induction principle perfectly satisfying. (-:O What is it you like about match/fixpoint/induction that an induction principle doesn't have? $\endgroup$ – Mike Shulman Mar 8 '18 at 21:35
  • $\begingroup$ (FWIW, I think using an induction principle in Coq is going to be much easier than using Twelf.) $\endgroup$ – Mike Shulman Mar 8 '18 at 21:36
  • $\begingroup$ Ok, I guess its just because I havn't tried yet then ! I had the impression that using the fixpoint/match syntax instead of spelling out explicitely the expression using the induction principle was more intuitive and readable (and also maybe the induction tactics, but I guess that in the end it does exactly the same as "apply Ind/rec") So maybe I should just try. $\endgroup$ – Simon Henry Mar 8 '18 at 21:41
  • $\begingroup$ Also do you know if I'm correct when I say that everything that coq can define/prove can be interpreted in something in the spirit of your stack semantics (let say I'm working either in a category with finite limits and looking at stacks for the discrete topology; or in a pretopos with the coherent topology) and the the induction principles are indeed the only things that should be restricted. Or is there other logical principles that Coq accept and that might be problematics ? $\endgroup$ – Simon Henry Mar 8 '18 at 22:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.