website 196

Stream: PR reviews

[Kyle Miller]

#196 is an update to the simplification documentation.

[Kyle Miller]

I'm not really sure what the lifecycle of a PR is for the website -- so I figured I'd mention that this PR exists here.

[Kyle Miller]

Incidentally, I found editing this documentation to have a high barrier to entry (there's a docs/extras/simp.md in mathlib, but it's a redirect, so then I had to find the right repo, and after editing it I found I didn't have permission to push a branch, so I had to fork the website and make a PR using my fork's branch). There must be a reason it's not, but it would be nice if all mathlib documentation were in the mathlib repo.

[Bryan Gin-ge Chen]

It looks good to me, but I've been hoping an expert like @Mario Carneiro might take a quick look at it.

[Kyle Miller]

I tried digging up what the lift_eq and use_axioms configuration options do, reading through the core C++ code as best I could.

lift_eq seems to have something to do with generating proofs of reflexive relations from proofs of equalities, though I couldn't come up with an example.

use_axioms seems to allow simp to use funext and propext (for example, to rewrite under binders).

I also wrote that canonize_proofs lets simp replace proofs with a canonical defeq one, since that's what the source code said. I have no idea when or why you'd do this. Maybe this is from the before-times when proof irrelevance wasn't a thing.

[Mario Carneiro]

simp uses propext when simp lemmas are provided in the form A <-> B, because internally it only knows how to handle equality rewriting

[Mario Carneiro]

Kyle Miller said:

I also wrote that canonize_proofs lets simp replace proofs with a canonical defeq one, since that's what the source code said. I have no idea when or why you'd do this. Maybe this is from the before-times when proof irrelevance wasn't a thing.

No, this is not before time stuff. Proofs are defeq but not syntactically equal, and simp cares about syntactic equality, so it does make a difference. Note that there are quire a few simp lemmas that use variables in place of proof arguments on the LHS for added generality even when the argument can be given a proof

[Mario Carneiro]

I'm not entirely sure how this is implemented, but my guess is that it keeps a list of all proof terms encountered and whenever two proof terms have the same type it replaces one with the other

[Mario Carneiro]

I don't have any additional wisdom regarding lift_eq, unfortunately. I suspect it might have something to do with generalizing congr and simp to work on other relations, which never really happened

[Kyle Miller]

Mario Carneiro said:

I'm not entirely sure how this is implemented, but my guess is that it keeps a list of all proof terms encountered and whenever two proof terms have the same type it replaces one with the other

I'd gotten as far as finding that there was a map for that (it's also used for instances), but I didn't dig into what was responsible for maintaining it.

I had no idea that simp didn't know about proof irrelevance; that's interesting. I'm now wondering if I've introduced any simp lemmas that weren't proof-generic enough...

[Mario Carneiro]

it knows about proof irrelevance indirectly, through congr, which handles arguments of subsingleton types specially (including propositions)

[Kyle Miller]

Are you talking about the "congruence lemmas" mentioned in simplify.cpp, or is congr used somewhere in simp?

[Mario Carneiro]

The tactic called congr uses the same underlying machinery that simp uses to rewrite in subterms, namely some C++ code that will generate congruence lemmas for arbitrary definitions

[Mario Carneiro]

simp does not call congr directly in lean

[Mario Carneiro]

in fact, simp came first, and I asked for the congruence lemma generator to be exposed as a standalone tactic

[Kyle Miller]

I assume Mario's not not satisfied with the PR, having given a couple corrections.

[Mario Carneiro]

That's correct. It would be nice to figure out lift_eq and get rid of the (?), but I don't have the time to investigate this myself, and the changes themselves look good

[Kyle Miller]

It'd also be nice to have some explanation of what the role of congruence lemmas is with simp, but simp.md is already trying to do too much.

There's a theory of documentation that there are broadly four types, and that it's useful to be clear what you're targeting. simp.md is mostly an explanation (for theoretical knowledge while studying), but by the end it becomes a reference (for theoretical knowledge while working). Ideally the reference part would be a separate document that's integrated into tactic#simp (with tactic#simp being the first part of a longer reference document, like the beginning of a Mathematica reference page). It's better having this information written down than not having it at all, but adding too much else to simp.md seems to be out of scope for what it aims to be.

Long term I'd like to reorganize the documentation to make it easy to have all these kinds of articles, all interlinked, but it's not something I can put any time into for at least another couple of months.

[Kyle Miller]

@Bryan Gin-ge Chen Do you think it's ready to be merged now?

[Bryan Gin-ge Chen]

It's merged now, thanks so much for working on this!

edit: the new page is now live

[Kyle Miller]

Looks like the markdown processor for the website doesn't italicize *`simp` lemmas* like "simp lemmas". (And Zulip-flavored markdown has no escaping, so I can't reproduce what it looks like here.)

It seems that the code { padding: 1px 3px } causes the first line of every code block to be indented by 3 pixels in my browsers (Chrome and Firefox on linux).

[Kevin Buzzard]

Thanks so much for doing this! The original version of that document was written by me and I never really knew what I was talking about, I just needed to have something to show the undergraduates who thought that simp would close an arbitrary goal as long as it was simple!