CPP '21

Stream: general

[Rob Lewis]

The call for papers for CPP '21 (Certified Programs and Proofs) is out! https://popl21.sigplan.org/home/CPP-2021#Call-for-Papers
We hope some of the Lean Zulip crowd will consider submitting.

[Rob Lewis]

Note that the abstract deadline is September 16, earlier than in past years.

[Kevin Buzzard]

Would they consider a paper about schemes?

[Reid Barton]

Does it contain programs and/or proofs? :upside_down:

[Rob Lewis]

Reid Barton said:

Does it contain programs and/or proofs? :upside_down:

And are they certified? If so, submit!

[Rob Lewis]

Three Lean papers at CPP '21 in January! Congrats

• @Johan Commelin (https://arxiv.org/abs/2010.02595)
• @Jannis Limperg (https://limperg.de/paper/cpp2021-induction/draft.pdf)
• @Koundinya Vajjha (https://arxiv.org/abs/1911.00385)

And @Jasmin Blanchette (https://matryoshka-project.github.io/pubs/satur_isa_paper.pdf) and @Jacques Carette (https://arxiv.org/abs/2005.07059), not using Lean but still part of the crowd here :smile:

[Yakov Pechersky]

The overview of the niceties and difficulties of metaprogramming in the induction tactic paper is extremely informative!

[Koundinya Vajjha]

Another one accepted is https://arxiv.org/abs/2009.11403
This is in Coq. It should be possible to port this to Lean if mathlib has the Banach Fixed Point theorem. I haven't looked at mathlib in a while, but how far away are we from Fixed point theorems?

[Reid Barton]

Is docs#contracting_with.exists_fixed_point what you need?

[Koundinya Vajjha]

Oh wow, that's great!

[Reid Barton]

there's also a ' version

[Johan Commelin]

@Jannis Limperg Your paper is really nice to read! Thanks for writing it. One remark (that I've made earlier this week in an unrelated context):

They are turned into regular expressions

I think you mean "ordinary expressions", and not regexes.

[Patrick Massot]

I just found some time to read @Jannis Limperg 's introduction. I'm surprised because the difficulties mentioned with inductionare not at all what I expected. To me the issue with induction is failing to infer the motive. A very long time ago I tried to port math-comp bigop library. It was impossible for me to replicate the nice proofs there because we donn't have SSReflect elim tactic which does induction that actually infer the motive. The introduction to Jannis's paper doesn't seem to refer to this issue, and search the paper for SSReflect doesn't return any hit whereas Coq is mentioned a lot. To me it sounds like assessing Lean using only the core library without looking at what is in mathlib. What's the story here?

[Jasmin Blanchette]

The intro makes it clear what the story is here: The tactic was motivated by the (C.S.) course at the VU, where we'd run into a number of issues in previous years. The current intro doesn't mention all issues (e.g. induction treats curried predicates much better than uncurried, but there are good reasons for (semi-)uncurried). A lot of the focus is on inductive predicates, which is more a C.S. preoccupation than a mathematical one.

I'd be curious to know what elim (which I've used a little bit) does that the Lean induction doesn't do in terms of motive inferrence.

[Kevin Buzzard]

For me, the difficulties with induction are that it insists on using the constructors of the type and even avoids notation. Induction was one reason the natural number game didn't exist in 2018 but instead appeared in 2019. Students had problems even doing basic natural number stuff with induction because you make notation has_zero nat and then apply induction on n and you're looking at nat.zero instead of 0 and all the rewrites fail and all the beginners gets lost. It wasn't until I understood more about type theory and notation that I was capable of hacking the induction command to fix these issues.

[Jasmin Blanchette]

Wouldn't applying induction with an explicit rule solve that problem (apart from the problem that you have to specify the rule every time)?

[Kevin Buzzard]

Probably. I found a solution (tagging various refl lemmas as being important and trying to rewrite them after induction had taken place, behind the user's back) and got it to work. I'm not claiming that I know what I'm doing now, let along what I was doing in mid-2019 when I was half my current Lean age :-)

[Jannis Limperg]

Thank you Johan for the correction and Yakov for the kind words! I'm very happy that the paper was useful to more than zero people.

Patrick: as Jasmin says, nu-induction deals mostly with the issues we ran into with the course, which are more typical of programming language or logic formalisations. I wasn't even aware that there are issues with induction in the context of the mathy parts of mathlib (except for the ugly names). If motive inference is a problem, it might not be too hard to clone the heuristic that SSReflect uses, but I don't know what that heuristic is. As it stands, nu-induction uses Lean's builtin heuristic, so it's no better or worse than standard induction in this regard.

Kevin: a general solution to your problem might be to decouple the default induction scheme for a type from the definition of that type. One could use a meta type class that associates a type with an induction scheme, falling back to the auto-generated induction scheme if no instance is found. That's surely overkill for just the natural number game, but it might be interesting if there are more such situations in mathlib.

[Patrick Massot]

I could try to find example from that bigop library if you are willing to work on this.

[Jasmin Blanchette]

It could be useful also as "future work" in the final version of the paper, if nothing else. That might inspire others. :) E.g. future MSc students at the VU.

[Rob Lewis]

CPP starts on Sunday, and prerecorded talks are posted for most of the papers: https://popl21.sigplan.org/home/CPP-2021?#program

[Rob Lewis]

The organization is ... complicated, so there are going to be short talks too. My short talk about Witt vectors is here. (Johan's long talk is linked on the schedule, also here)

[Rob Lewis]

CPP is starting in a few min, with a talk by Tobias Nipkow on teaching with proof assistants. https://www.youtube.com/watch?v=PAxUO84tUE8&ab_channel=CertifiedProgramsandProofs

[Rob Lewis]

Schedule: https://popl21.sigplan.org/home/CPP-2021?#program

[Patrick Massot]

Jannis' talk was very nice!

[Jannis Limperg]

Thanks! Glad you liked it. Links in case anyone else is interested (this is about the design and implementation of the induction' tactic): short presentation, long presentation, paper.